Mathlib.Data.PFun._auxLemma.6
theorem Mathlib.Data.PFun._auxLemma.6 :
∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (x : α), (x ∈ f.preimage s) = ∃ y ∈ s, y ∈ f x
The theorem `Mathlib.Data.PFun._auxLemma.6` states that for all types `α` and `β`, a partial function `f` from `α` to `β`, a set `s` of `β`, and an element `x` of `α`, the fact that `x` belongs to the preimage of `s` under `f` (i.e., `x ∈ PFun.preimage f s`) is equivalent to the existence of an element `y` in `s` such that `y` belongs to the function `f` at `x` (i.e., `∃ y ∈ s, y ∈ f x`). In simple terms, an element is in the preimage of a set under a partial function if and only if there exists an element in the original set that is mapped to by the function from the given element.
More concisely: For all types `α` and `β`, a partial function `f` from `α` to `β`, and an element `x` in `α` and a set `s` in `β`, `x` is in the preimage of `s` under `f` if and only if there exists `y` in `s` such that `f x = y`.
|
Mathlib.Data.PFun._auxLemma.10
theorem Mathlib.Data.PFun._auxLemma.10 :
∀ {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β} {b : β}, (b ∈ f.bind g) = ∃ a ∈ f, b ∈ g a
The theorem `Mathlib.Data.PFun._auxLemma.10` states that for all types `α` and `β`, a partial function `f` from `α`, a function `g` from `α` to `Part β`, and a value `b` of type `β`, `b` belongs to the bind operation of `f` and `g` if and only if there exists a value `a` belonging to `f` such that `b` belongs to `g a`. In other words, `b` is in the result of binding `f` and `g` if there is an element in `f` which when passed through `g` produces `b`.
More concisely: For all types `α` and `β`, and partial functions `f : α → Option β` and `g : α → Part β`, the value `b` belongs to `bind f g` if and only if there exists an `a` in the domain of `f` such that `b` is an element of `g a`.
|
PFun.dom_of_mem_fix
theorem PFun.dom_of_mem_fix :
∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {b : β}, b ∈ f.fix a → (f a).Dom
This theorem states that for all types `α` and `β`, and for all function `f` that takes a value of type `α` and returns a value of type `β` or `α`, and given any elements `a` of type `α` and `b` of type `β`, if `b` is in the fixed point of `f` with respect to `a`, then `a` is in the domain of `f`. This is a property related to the concept of fixed points in function theory, where a fixed point of a function is an element that is mapped to itself by the function. Here, it is stated in the context of partial functions, which are functions that may not have a defined output for every input.
More concisely: If a partial function `f` has `a` as its fixed point with respect to an argument `b`, then `a` lies in the domain of `f`.
|
Mathlib.Data.PFun._auxLemma.11
theorem Mathlib.Data.PFun._auxLemma.11 : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, ((∃ x, p x) ∧ b) = ∃ x, p x ∧ b
This theorem states that for any type `α`, any predicate `p` on `α`, and any proposition `b`, the proposition `((∃ x, p x) ∧ b)` is equivalent to `∃ x, p x ∧ b`. In simpler terms, it says that the existence of an element satisfying a certain property and another independent proposition being true, is the same as there existing an element which satisfies the property and the independent proposition is true.
More concisely: For any type `α`, predicate `p` on `α`, and proposition `b`, `∃x, p x ∧ b` is equivalent to `(∃x, p x) ∧ b`.
|
PFun.fix_stop
theorem PFun.fix_stop :
∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {b : β} {a : α}, Sum.inl b ∈ f a → b ∈ f.fix a
This theorem states that for any types `α` and `β`, and for any function `f` from `α` to a sum type of `β` and `α`, if applying `f` to `a` results in a left sum (a value of type `β`) denoted by `b`, then `b` is also an element in the fixpoint of `f` on `a`. In other words, if advancing one step from `a` leads to `b : β`, then `b` is included in the result of applying the fixpoint function of `f` on `a`.
More concisely: For any functions f from type α to the sum type β + α, if applying f to x results in a left sum value b of type β, then b is in the fixpoint of f on x.
|
PFun.coe_comp
theorem PFun.coe_comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β), ↑(g ∘ f) = (↑g).comp ↑f
This theorem, `PFun.coe_comp`, states that for any three types, α, β, and γ, and for any two functions, g, which maps from β to γ, and f, which maps from α to β, the composition of these two functions when considered as partial functions (i.e., `↑(g ∘ f)`) is equal to the composition of these two functions considered as partial functions individually (`PFun.comp ↑g ↑f`). Here, `PFun.comp` denotes the composition of partial functions as a partial function, and ↑ denotes the coercion of a function to a partial function.
More concisely: For any functions f : α -> β and g : β -> γ, the coercions of their composition g ∘ f to a partial function are equal: ↑(g ∘ f) = PFun.comp ↑g ↑f.
|
PFun.ext'
theorem PFun.ext' :
∀ {α : Type u_1} {β : Type u_2} {f g : α →. β},
(∀ (a : α), a ∈ f.Dom ↔ a ∈ g.Dom) → (∀ (a : α) (p : f.Dom a) (q : g.Dom a), f.fn a p = g.fn a q) → f = g
This theorem is called "Partial function extensionality". It states that for any two partial functions `f` and `g` from type `α` to type `β`, if the domain of `f` and `g` are the same (i.e., for every element `a` of type `α`, `a` is in the domain of `f` if and only if it is in the domain of `g`), and if for every element `a` in their common domain, the value of `f` at `a` is equal to the value of `g` at `a`, then `f` and `g` are the same partial function. This theorem thus formalizes a notion of equality for partial functions based on their definedness and their behavior on their common domain.
More concisely: If two partial functions from type `α` to type `β` have the same domain and agree on their values for all elements in their common domain, then they are equal as partial functions.
|
PFun.fix_fwd_eq
theorem PFun.fix_fwd_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a a' : α}, Sum.inr a' ∈ f a → f.fix a = f.fix a'
This theorem states that for any types `α` and `β`, and any partial function `f` from `α` to the sum type `β ⊕ α`, if advancing one step from an element `a` of `α` along `f` leads to another element `a'` of `α`, then the fixed point of `f` at `a` is the same as the fixed point of `f` at `a'`. In other words, `f.fix a = f.fix a'`.
More concisely: If `f` is a partial function from type `α` to `β ⊕ α` such that advancing one step from `a` to `a'` in `α` along `f` implies `f.fix a = f.fix a'`, then `a` and `a'` have the same fixed point in `f`.
|
PFun.ext
theorem PFun.ext : ∀ {α : Type u_1} {β : Type u_2} {f g : α →. β}, (∀ (a : α) (b : β), b ∈ f a ↔ b ∈ g a) → f = g := by
sorry
This theorem, `PFun.ext`, states that for any two partial functions `f` and `g` from a type `α` to a type `β`, if for all elements `a` from `α` and `b` from `β`, `b` is in the domain of `f a` if and only if `b` is in the domain of `g a`, then `f` and `g` are equal. In other words, two partial functions are equal if they have the same domain and produce the same results for every input in that domain.
More concisely: If two partial functions from type `α` to type `β` have the same domains and agree on their outputs for all elements in their common domain, then they are equal.
|