Option.pbind.proof_1
theorem Option.pbind.proof_1 : ∀ {α : Type u_1} (a : α), some a = some a
This theorem, `Option.pbind.proof_1`, asserts that for all types `α` and any element `a` of type `α`, an option containing `a` is equal to itself. In other words, any `some a` is equal to `some a`. This statement is essentially a formulation of the reflexivity property of equality in the context of option types in Lean 4.
More concisely: For all types `α` and elements `a` of type `α`, the option `some a` is equal to `some a`. In Lean 4 syntax: `(Option.pbind _ (some a) (some a)).get = a`.
|
Option.pmap.proof_1
theorem Option.pmap.proof_1 : ∀ {α : Type u_1} {p : α → Prop} (a : α), (∀ a_1 ∈ some a, p a_1) → p a
This theorem states that for any type `α` and for any predicate `p` over `α`, if `p` holds for all elements `a_1` contained in the option `some a`, then it also holds for the element `a` itself. In other words, if a predicate applies to all members of an option, then it also applies to any individual member of that option.
More concisely: If a predicate `p` holds for all elements in an option `some a`, then `p` holds for the contained element `a`.
|
Option.some_inj
theorem Option.some_inj : ∀ {α : Type u_1} {a b : α}, some a = some b ↔ a = b
This theorem, `Option.some_inj`, asserts that for all types `α` and for any two elements `a` and `b` of the type `α`, the `Option.some` function applied to `a` equals the `Option.some` function applied to `b` if and only if `a` equals `b`. In other words, it states the injectivity of the `Option.some` function: distinct inputs produce distinct outputs.
More concisely: For all types `α` and elements `a, b` of `α`, `Option.some a = Option.some b` if and only if `a = b`.
|
Option.mem_def
theorem Option.mem_def : ∀ {α : Type u_1} {a : α} {b : Option α}, a ∈ b ↔ b = some a
This theorem states that for any type `α` and any elements `a` of `α` and `b` of `Option α`, `a` is an element of `b` if and only if `b` is equal to `some a`. In other words, a value is contained in an Option value if and only if the Option value is `some` of that value. This is a fundamental property in Lean 4 pertaining to the concept of Option types, which are used to handle possible absence of a value.
More concisely: For any type `α` and `a ∈ α`, `Option.some a = b` if and only if `a ∈ b` for `b : Option α`.
|