Part.map_bind
theorem Part.map_bind :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : α → Part β) (x : Part α) (g : β → γ),
Part.map g (x.bind f) = x.bind fun y => Part.map g (f y)
The theorem `Part.map_bind` is about the interaction between the `map` and `bind` operations on `Part` types in Lean 4. It states that for all types `α`, `β`, `γ`, for any function `f` from `α` to `Part β`, a `Part` of `α` named `x`, and a function `g` from `β` to `γ`, mapping `g` over the result of binding `x` with `f` (i.e., `Part.map g (Part.bind x f)`) is equal to binding `x` with the function that maps `g` over `f` of `y` (i.e., `Part.bind x (λ y, Part.map g (f y))`). In essence, this theorem ensures that the `map` and `bind` operations on `Part` types are compatible in a way that mirrors the monadic laws.
More concisely: For any types α, β, γ, functions f from α to Part β and g from β to γ, Part.map g (Part.bind x f) equals Part.bind x (λ y, Part.map g (f y)).
|
Mathlib.Data.Part._auxLemma.14
theorem Mathlib.Data.Part._auxLemma.14 :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) {o : Part α} {b : β}, (b ∈ Part.map f o) = ∃ a ∈ o, f a = b
This theorem states that for any types `α` and `β`, a function `f` from `α` to `β`, a partial function `o` from `α`, and a value `b` of type `β`, `b` belongs to the result of mapping `f` over `o` (expressed as `b ∈ Part.map f o`) if and only if there exists a value `a` in `o` such that `f` applied to `a` equals `b`. This theorem essentially describes the behavior of the `map` operation on partial functions in terms of element membership.
More concisely: For any types `α`, `β`, function `f` from `α` to `β`, partial function `o` from `α`, and value `b` of type `β`, `b` is in the image of `f` under `o` (`b ∈ Part.map f o`) if and only if there exists an `a` in the domain of `o` such that `f(a) = b`.
|
Part.assert.proof_1
theorem Part.assert.proof_1 : ∀ {α : Type u_1} (p : Prop) (f : p → Part α), (∃ (h : p), (f h).Dom) → p
The theorem `Part.assert.proof_1` states that for any type `α`, any proposition `p`, and any function `f` from `p` to `Part α`, if there exists a proof `h` of `p` such that `(f h).Dom` is true, then `p` is true. In other words, if there is a proof of `p` for which `f` maps to a computationally meaningful value, then `p` must be true.
More concisely: If there exists a proof `h` of proposition `p` such that the domain of the function `f(h)` from `p` to `Part α` is true, then proposition `p` is true.
|
Mathlib.Data.Part._auxLemma.6
theorem Mathlib.Data.Part._auxLemma.6 : ∀ {α : Type u_1} {a b : α}, (b ∈ Part.some a) = (b = a)
This theorem states that for any type `α` and any two elements `a` and `b` of `α`, `b` is in the `Part.some` of `a` if and only if `b` is equal to `a`. In other words, the `Part.some` function creates a singleton set with `a` as the only member, and `b` is in this set only when `b` equals `a`.
More concisely: For any type `α` and elements `a, b` of `α`, `b` is in the singleton set `{a}`. i.e. `b = a`, if and only if `b ∈ {a}`.
|
Part.eq_none_iff'
theorem Part.eq_none_iff' : ∀ {α : Type u_1} {o : Part α}, o = Part.none ↔ ¬o.Dom
The theorem `Part.eq_none_iff'` states that for any type `α` and any partial function `o` of type `Part α`, `o` is equivalent to `Part.none` if and only if the domain of `o` is not true. Here, `Part.none` is a partial function that has a `False` domain and an empty function. In other words, a partial function is the same as `Part.none` precisely when its domain is not true.
More concisely: A partial function `o` of type `Part α` is equal to `Part.none` if and only if the domain of `o` is false.
|
Part.assert.proof_2
theorem Part.assert.proof_2 : ∀ {α : Type u_1} (p : Prop) (f : p → Part α) (ha : ∃ (h : p), (f h).Dom), (f ⋯).Dom := by
sorry
This theorem, `Part.assert.proof_2`, states that for any type `α`, any proposition `p`, and any function `f` from `p` to a partial function of `α`, if there exists a proof `h` of `p` such that the domain of `f(h)` is true, then the domain of the function `f` is also true. In other words, if there is some proof of the proposition for which the function `f` is defined, then the function `f` is defined in general.
More concisely: If a partial function `f` from a proposition `p` to type `α` has a defined value at some proof `h` of `p`, then the domain of `f` includes the proposition `p`.
|
Part.eq_none_iff
theorem Part.eq_none_iff : ∀ {α : Type u_1} {o : Part α}, o = Part.none ↔ ∀ (a : α), a ∉ o
This theorem, `Part.eq_none_iff`, states that for any type `α` and any part `o` of that type `α`, `o` is equal to `Part.none` (the `Part` value with a `False` domain and an empty function) if and only if for all elements `a` of type `α`, `a` is not in `o`. In simpler terms, a part is the 'none' part if no elements of the underlying type are contained in it.
More concisely: For any type `α` and part `o` of `α`, `o = Part.none` if and only if `o` is empty.
|
Part.bind_assoc
theorem Part.bind_assoc :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : Part α) (g : α → Part β) (k : β → Part γ),
(f.bind g).bind k = f.bind fun x => (g x).bind k
The theorem `Part.bind_assoc` states that for any types `α`, `β`, and `γ`, and any partial functions `f : Part α`, `g : α → Part β`, and `k : β → Part γ`, the operation `Part.bind` is associative. In other words, first binding `f` and `g`, and then binding the result with `k`, is the same as first binding `f` with the result of binding `g` and `k`. This mirrors the associative property in algebra where the way in which operations are grouped does not change the result (i.e., `(a * b) * c = a * (b * c)`).
More concisely: For any partial functions `f : Part α → Part β`, `g : α → Part β`, and `k : Part β → Part γ` in Lean 4, the composition `(Part.bind _ _) (f _) (Part.bind _ _ g)` is equal to `(Part.bind _ _ (Part.bind _ _ g)) f`.
|
Part.eta
theorem Part.eta : ∀ {α : Type u_1} (o : Part α), { Dom := o.Dom, get := fun h => o.get h } = o
This theorem, referred to as the `Part.eta` theorem, states that for any partial function `o` of type `α`, the function that takes a proof `h` of `o.Dom` and returns `o.get h` is equal to `o` itself. Essentially, it means that if we deconstruct a partial function into its domain and a function from that domain to its codomain, and then reconstruct it, we get the original partial function. This is an instance of the η-conversion property in lambda calculus.
More concisely: For any partial function `o` in Lean, `o.get (h : o.Dom) = o _` where `_` is the implicit argument.
|
Part.bind_some
theorem Part.bind_some : ∀ {α : Type u_1} {β : Type u_2} (a : α) (f : α → Part β), (Part.some a).bind f = f a := by
sorry
The theorem `Part.bind_some` states that for any two types `α` and `β`, an element `a` of type `α`, and a function `f` from `α` to `Part β`, binding the function `f` to the `Part.some a` (which is a `Part` type object with a `True` domain and a function returning `a`) is equivalent to applying the function `f` to `a`. In other words, when we bind `Part.some a` with any function `f`, it behaves just like applying `f` directly to `a`. This theorem is about the behavior of the `bind` operation in the `Part` monad.
More concisely: For any types α and β, function f from α to Part β, and element a of α, the application of f to Part.some a is equivalent to binding Part.some a with f.
|
Mathlib.Data.Part._auxLemma.5
theorem Mathlib.Data.Part._auxLemma.5 : ∀ {α : Type u_1} (a : α), (Part.some a).1 = True
This theorem states that for any type `α` and an element `a` of type `α`, the domain of the `Part.some a` function is `True`. In other words, the defined part function `Part.some a` has a domain that is always `True` for any `a` of any type `α`.
More concisely: For any type `α` and element `a` of type `α`, the domain of the function `Part.some a` is unconditionally `True`.
|
Part.some_injective
theorem Part.some_injective : ∀ {α : Type u_1}, Function.Injective Part.some
The theorem `Part.some_injective` states that for any type `α`, the function `Part.some` is injective. In other words, if we have two values of type `α`, say `a₁` and `a₂`, and if `Part.some a₁` equals `Part.some a₂`, then it must be the case that `a₁` equals `a₂`. This injectivity property means that `Part.some` function does not map different inputs to the same output.
More concisely: For any type `α`, the function `Part.some : α option → α` is an injection.
|
Part.bind_some_eq_map
theorem Part.bind_some_eq_map :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : Part α), x.bind (Part.some ∘ f) = Part.map f x
This theorem, `Part.bind_some_eq_map`, states that for any types `α` and `β`, and any function `f` from `α` to `β`, and for any partial value `x` of type `α`, binding `x` to a function that applies `f` and then wraps the result in a `Part` with a `True` domain (done by `Part.some ∘ f`) is equivalent to just mapping `f` over `x` directly. In essence, the theorem establishes a link between the `bind` and `map` operations on partial values, where binding with a function that simply wraps the result is the same as mapping that function.
More concisely: For any types `α` and `β`, and any function `f: α → β`, the application of `Part.bind` with the function `x => Part.some ∘ f` to a partial value `x: α` is equal to directly applying `f` to `x`.
|
Part.map_id'
theorem Part.map_id' : ∀ {α : Type u_1} {f : α → α}, (∀ (x : α), f x = x) → ∀ (o : Part α), Part.map f o = o
The theorem `Part.map_id'` states that for any type `α`, and for any function `f : α → α` such that `f` is the identity function (i.e., for all `x` of type `α`, `f(x) = x`), the map operation applied to `f` and any partial function `o : Part α` is equal to `o` itself. In other words, mapping an identity function over a partial function leaves the original partial function unchanged.
More concisely: For any type `α` and identity function `f : α → α`, the map operation `Part.map f o` over a partial function `o : Part α` equals `o` itself.
|
Part.ext'
theorem Part.ext' :
∀ {α : Type u_1} {o p : Part α}, (o.Dom ↔ p.Dom) → (∀ (h₁ : o.Dom) (h₂ : p.Dom), o.get h₁ = p.get h₂) → o = p := by
sorry
This theorem, `Part.ext'`, expresses an extensionality property for partial functions in Lean 4. Specifically, it asserts that for any two partial functions `o` and `p` of the same type `α`, if their domains are equivalent (i.e., `o.Dom` if and only if `p.Dom`) and for every element in their domains, the function values are equal (i.e., `o.get h₁` equals `p.get h₂`), then `o` must be equal to `p`.
More concisely: If two partial functions `o` and `p` from type `α` have equivalent domains and agree on their common domain elements (i.e., `o (h ∈ o.dom) = p (h)` for all `h ∈ o.dom`), then `o` equals `p`.
|
Part.mem_unique
theorem Part.mem_unique : ∀ {α : Type u_1} {a b : α} {o : Part α}, a ∈ o → b ∈ o → a = b
This theorem, `Part.mem_unique`, states that for any type `α`, and any two elements `a` and `b` of that type, if both `a` and `b` are elements of the same partial function `o` (of type `Part α`), then `a` and `b` must be equal. In other words, it asserts that a partial function can have at most one value for any given input.
More concisely: For any type `α` and partial function `o` of type `Part α`, if `a` and `b` are in the domain of `o` and `o a = o b`, then `a = b`.
|
Part.get_mem
theorem Part.get_mem : ∀ {α : Type u_1} {o : Part α} (h : o.Dom), o.get h ∈ o
This theorem, `Part.get_mem`, states that for any type of `α` and any partial function `o` of type `α`, if `h` is a proof that the domain of `o` is not empty (i.e., `o.Dom`), then the application of `o.get` to `h` is an element of `o`. In other words, any value that we can extract from a partial function using `get` is assured to be an element of that partial function.
More concisely: For any partial function `o` on type `α` with non-empty domain, `o.get (h : o.Dom) ∈ o`.
|
Part.map_some
theorem Part.map_some :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), Part.map f (Part.some a) = Part.some (f a)
The theorem `Part.map_some` states that for all types `α` and `β`, and for any function `f` from `α` to `β` and any element `a` of type `α`, the operation of mapping `f` over a `Part` that is `some a` (which means a `Part` whose domain is `True` and the function returns value `a`) is equivalent to the `Part` that is `some (f a)`. In simpler terms, applying a function to the value inside the `Part` and then creating a `Part` out of it is the same as first creating a `Part` out of the value and then applying the function to it. This theorem is a formal statement of the property that the map operation of the `Part` type respects the unit of the `Part` monad (which is `Part.some`).
More concisely: For all types α and β, and for any function f from α to β, the mapping of f over a Part.some a is equivalent to Part.some (f a).
|
Part.bind_none
theorem Part.bind_none : ∀ {α : Type u_1} {β : Type u_2} (f : α → Part β), Part.none.bind f = Part.none
The theorem `Part.bind_none` states that for any function `f` from a type `α` to a partial type `β`, binding `Part.none` (representing a "null" or "empty" partial value) with function `f` results in `Part.none`. This can be understood as saying that when we try to apply `f` to an undefined or non-existent value (represented by `Part.none`), the result is again undefined or non-existent. In mathematical terms, it asserts that partial function binding with an undefined value leads to an undefined result, irrespective of the function used in the binding process.
More concisely: For any partial function `f` from type `α` to partial type `β`, `bind (Part.none) f = Part.none`.
|
Mathlib.Data.Part._auxLemma.19
theorem Mathlib.Data.Part._auxLemma.19 :
∀ {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β} {b : β}, (b ∈ f.bind g) = ∃ a ∈ f, b ∈ g a
The theorem `Mathlib.Data.Part._auxLemma.19` states that for any two types `α` and `β`, a partial function `f` from `Part α`, a function `g` from `α` to `Part β`, and an element `b` of type `β`, the element `b` is in the result of binding `f` and `g` (i.e., `b ∈ Part.bind f g`) if and only if there exists an element `a` in `f` such that `b` is in `g a`. In other words, the theorem is defining the conditions under which a value `b` is a member of the result of the `bind` operation on `f` and `g`.
More concisely: For any partial functions `f` from `α` to `Part β` and `g` from `α` to `β`, and any `b` in `β`, `b` is in the result of binding `f` and `g` (`b ∈ Part.bind f g`) if and only if there exists an `a` in `α` such that `b` is in `g a`.
|
Part.mem_assert_iff
theorem Part.mem_assert_iff :
∀ {α : Type u_1} {p : Prop} {f : p → Part α} {a : α}, a ∈ Part.assert p f ↔ ∃ (h : p), a ∈ f h
The theorem `Part.mem_assert_iff` states that for any type `α`, proposition `p`, function `f` from `p` to `Part α`, and element `a` of type `α`, `a` is an element of `Part.assert p f` if and only if there exists a proof `h` of the proposition `p` such that `a` is an element of `f h`. In other words, `a` is in the partial function produced by `Part.assert` given `p` and `f` precisely when `a` is in the domain of the `f` applied to some proof of `p`.
More concisely: For any type `α`, proposition `p`, function `f` from `p` to the powerset of `α`, and element `a` of type `α`, `a` belongs to `Part.assert p f` if and only if there exists a proof `h` of `p` such that `a` is in `f(h)`.
|
Part.mem_some
theorem Part.mem_some : ∀ {α : Type u_1} (a : α), a ∈ Part.some a
The theorem `Part.mem_some` states that for all types `α` and any element `a` of type `α`, `a` is an element of `Part.some a`. In other words, any element `a` belongs to the partial function represented by `Part.some a`, which is defined to have a `True` domain and always returns `a`.
More concisely: For any type `α` and element `a` of type `α`, `a` is a member of the image of the constant partial function `Part.some a`.
|
Part.some_get
theorem Part.some_get : ∀ {α : Type u_1} {a : Part α} (ha : a.Dom), Part.some (a.get ha) = a
The theorem `Part.some_get` states that for any type `α`, and any partial function `a` of type `Part α` with a domain (denoted by `a.Dom`), applying the function `Part.some` to the result of calling `a.get` with the domain `ha` returns the original partial function `a`. This means that wrapping a function's result with `Part.some` and then retrieving it gives back the original function. Essentially, it's saying that `Part.some` and `a.get` are inverses of each other for this particular setup.
More concisely: For any partial function `a` of type `Part α` with domain `ha`, `Part.some (a.get ha) = a`.
|
Part.map_none
theorem Part.map_none : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Part.map f Part.none = Part.none
This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β`, mapping `f` over the `none` value in the `Part` type (which has a `False` domain and an empty function) yields the `none` value in the `Part` type. In other words, applying any function with the `Part.map` operation to an empty partial function results in another empty partial function.
More concisely: For any types `α` and `β` and function `f` from `α` to `β`, the application of `f` to a `Part` with empty domain results in another `Part` with empty domain.
|
Part.ext
theorem Part.ext : ∀ {α : Type u_1} {o p : Part α}, (∀ (a : α), a ∈ o ↔ a ∈ p) → o = p
This theorem, `Part.ext`, states that for any type `α` and any two partial functions `o` and `p` of type `Part α`, if for every `α`, `α` belongs to `o` if and only if it belongs to `p`, then `o` and `p` are equivalent. In other words, two partial functions are the same if they have the same elements.
More concisely: If two partial functions have the same domains and map each element in their domains to the same value, then they are equal.
|
Part.dom_iff_mem
theorem Part.dom_iff_mem : ∀ {α : Type u_1} {o : Part α}, o.Dom ↔ ∃ y, y ∈ o
This theorem, `Part.dom_iff_mem`, states that for any given partial function `o` of an arbitrary type `α`, the domain of `o` (`o.Dom`) exists if and only if there exists an element `y` such that `y` is an element of `o`. In other words, a partial function has a domain if it has at least one element.
More concisely: A partial function `o` over type `α` has a domain if and only if there exists an element `y` in `α` such that `o y` is defined.
|
Mathlib.Data.Part._auxLemma.4
theorem Mathlib.Data.Part._auxLemma.4 : ∀ {α : Type u_1} (a : α), (a ∈ Part.none) = False
This theorem states that for any type `α` and any element `a` of that type, `a` is not an element of `Part.none`. In other words, `Part.none`, which is a `Part` with a `False` domain and an empty function, contains no elements irrespective of the type `α`.
More concisely: For all types `α` and elements `a` of type `α`, `a` is not an element of the empty `Part` `Part.none` with domain `False`.
|
Part.bind_map
theorem Part.bind_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : α → β) (x : Part α) (g : β → Part γ),
(Part.map f x).bind g = x.bind fun y => g (f y)
The theorem `Part.bind_map` describes the interchangeability of "bind" and "map" operations on `Part` objects, which hold optional values. For any types `α`, `β`, and `γ`, a function `f` from `α` to `β`, a `Part` object `x` of type `α`, and a function `g` from `β` to a `Part` object of type `γ`, binding the result of mapping `f` over `x` with `g` is the same as binding `x` with the function that sends `y` to `g` applied to `f(y)`. This can be seen as a form of function composition associativity in the context of partial computations.
More concisely: For any functions `f: α → β` and `g: β → Part γ`, the application of `bind` and `map` operations on a `Part α` value `x` in the order `x >>= g . f` is equivalent to `bind (f x) g`.
|
Part.eq_some_iff
theorem Part.eq_some_iff : ∀ {α : Type u_1} {a : α} {o : Part α}, o = Part.some a ↔ a ∈ o
The theorem `Part.eq_some_iff` asserts that for any type `α`, any element `a` of type `α`, and any partial function `o` of type `Part α`, `o` is equal to the partial function `Part.some a` if and only if `a` is in the domain of `o`. In other words, a partial function is equivalent to `Part.some a` (a function with a `True` domain that always returns `a`) if and only if `a` is an element of the domain of the function. This theorem establishes the bidirectional relationship between the identity of a partial function and the presence of a specific element within its domain.
More concisely: For any partial function `o` of type `Part α` and element `a` of type `α`, `o = Part.some a` if and only if `a` is in the domain of `o`.
|