EsakiaHom.ext
theorem EsakiaHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
[inst_3 : Preorder β] {f g : EsakiaHom α β}, (∀ (a : α), f a = g a) → f = g
The theorem `EsakiaHom.ext` states that for any two types `α` and `β` where `α` and `β` have a topological space and preorder structure, and for any two Esakia homomorphisms `f` and `g` from `α` to `β`, the two Esakia homomorphisms are equal if they map any `α` to the same `β`. That is, if for every element `a` of `α`, `f(a)` equals `g(a)`, then `f` equals `g`. In mathematical terms, it validates the extensionality property for Esakia homomorphisms.
More concisely: If two Esakia homomorphisms between topological preordered types map every element to the same image, then they are equal.
|
PseudoEpimorphism.ext
theorem PseudoEpimorphism.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f g : PseudoEpimorphism α β},
(∀ (a : α), f a = g a) → f = g
This theorem states that for any two pseudo-epimorphisms `f` and `g` from a type `α` to a type `β`, where both `α` and `β` have a preorder structure, if `f` and `g` are equal at every point `a` in `α`, then `f` and `g` are themselves equal. Essentially, this theorem justifies the pointwise equality of pseudo-epimorphisms.
More concisely: If `f` and `g` are two pseudo-epimorphisms from a preordered type `α` to a preordered type `β`, then `f` and `g` are equal if and only if they agree at every point in `α`.
|