sInfHomClass.map_sInf
theorem sInfHomClass.map_sInf :
∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : FunLike F α β]
[self : sInfHomClass F α β] (f : F) (s : Set α), f (sInf s) = sInf (⇑f '' s)
This theorem, `sInfHomClass.map_sInf`, states that for any types `F`, `α`, and `β`, where `α` and `β` are both `InfSet` (i.e., types with an infimum operation), if `F` is a `FunLike` (or function-like) from `α` to `β`, and is in the `sInfHomClass` (i.e., it preserves the infimum operation under the mapping), then for any function `f` of type `F` and any set `s` of type `α` the infimum of the image of `s` under `f` is equal to the image of the infimum of `s` under `f`.
In other words, given a function `f` that is a homomorphism preserving infima, the operation of taking the infimum of a set and then applying `f` is the same as first applying `f` to each element of the set and then taking the infimum of the resulting values. This is written in mathematical notation as `f(inf s) = inf {f(x) : x in s}`.
More concisely: For any `FunLike` function `F` from an `InfSet` type `α` to another `InfSet` type `β`, if `F` preserves infima (i.e., `F.map inf = inf .map F`), then `F(inf {x : α | x ∈ s}) = inf {F(x) : x ∈ s}` for any set `s` in `α`.
|
CompleteLatticeHomClass.map_sSup
theorem CompleteLatticeHomClass.map_sSup :
∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
[inst_2 : FunLike F α β] [self : CompleteLatticeHomClass F α β] (f : F) (s : Set α),
f (sSup s) = sSup (⇑f '' s)
This theorem states that for any type `F`, and any types `α` and `β` which are complete lattices, if `F` has a function-like structure from `α` to `β` and respects the structure of complete lattice homomorphisms, then for any function `f` of type `F` and any set `s` of elements of type `α`, the supremum (in the complete lattice sense, also referred to as the join) of the set `s` mapped through `f` is equal to the supremum of the image of the set `s` under the function `f`. In other words, the function `f` commutes with the operation of taking the supremum. This is a key property of morphisms between complete lattices.
More concisely: For any complete lattice homomorphism `f` from a complete lattice `α` to a complete lattice `β` and any subset `s` of `α`, the image of the supremum of `s` under `f` is equal to the supremum of the images of elements in `s` under `f`.
|
FrameHomClass.map_sSup
theorem FrameHomClass.map_sSup :
∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
[inst_2 : FunLike F α β] [self : FrameHomClass F α β] (f : F) (s : Set α), f (sSup s) = sSup (⇑f '' s)
The theorem `FrameHomClass.map_sSup` states that for any types `F`, `α`, and `β`, if `α` and `β` are both complete lattices, `F` is a function-like relation from `α` to `β`, and `F` belongs to the class `FrameHomClass` (i.e., it preserves the structure of frames, or complete lattices), then for every function `f` of type `F` and every set `s` of elements of type `α`, the application of `f` to the supremum (`sSup`) of `s` is equal to the supremum of the image of `s` under `f`. In other words, the function `f` commutes with the operation of taking suprema, or joins, in the lattice.
More concisely: For any complete lattices α and β, and any function-like relation F from α to β belonging to FrameHomClass, the application of F to the supremum of a set in α is equal to the supremum of the images of that set under F.
|
sSupHomClass.map_sSup
theorem sSupHomClass.map_sSup :
∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : FunLike F α β]
[self : sSupHomClass F α β] (f : F) (s : Set α), f (sSup s) = sSup (⇑f '' s)
This theorem states that for any type `F`, any types `α` and `β`, given that the suprema operation is defined on `α` and `β` (denoted by `SupSet α` and `SupSet β`), and that `F` is a function-like from `α` to `β` (`FunLike F α β`), and `sSupHomClass F α β` holds (meaning that `F` maps suprema to suprema), then for any function `f` of type `F` and any set `s` of type `α`, the supremum of the image of `s` under `f` is equal to the image of the supremum of `s` under `f`. In other words, the function `f` commutes with the supremum operation: taking the supremum after applying `f` is the same as applying `f` after taking the supremum.
More concisely: For any function-like `F` from type `α` to type `β` with `sSupHomClass F α β`, if `SupSet α` and `SupSet β` hold and `s` is a set of type `α`, then `Sup (map F s) = map (Sup s) F`.
|
sSupHom.map_sSup'
theorem sSupHom.map_sSup' :
∀ {α : Type u_8} {β : Type u_9} [inst : SupSet α] [inst_1 : SupSet β] (self : sSupHom α β) (s : Set α),
self.toFun (sSup s) = sSup (self.toFun '' s)
The theorem `sSupHom.map_sSup'` states that for any types `α` and `β` equipped with a supremum operation (given by `SupSet α` and `SupSet β`), and any function `self` from `α` to `β` that respects the supremum operation (i.e., an `sSupHom`), the function `self` commutes with taking supremum. In other words, if `s` is a set in `α`, the supremum of the image of `s` under `self` is the same as applying `self` to the supremum of `s`. This can be written in mathematical notation as: for all sets `s` of `α`, `self(sup s) = sup(self(s))`.
More concisely: For any types `α` and `β` with supremum operations and an `sSupHom` function `self` from `α` to `β`, `self(Sup a s) = Sup b (self `` map s)` for all sets `s` in `α`.
|
map_iSup
theorem map_iSup :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [inst : FunLike F α β] [inst_1 : SupSet α]
[inst_2 : SupSet β] [inst_3 : sSupHomClass F α β] (f : F) (g : ι → α), f (⨆ i, g i) = ⨆ i, f (g i)
The theorem `map_iSup` states that for any types `F`, `α`, `β`, and `ι`, if `F` is a function-like mapping from `α` to `β`, both `α` and `β` are SupSet (i.e., they are equipped with a supremum operation), and `F` respects the supremum operation (i.e., `F` is a sup-semilattice homomorphism), then the function `f` of type `F` distributes over the supremum of a family `(g i)` of elements in `α` indexed by `ι`. In mathematical terms, this means that for any function `f` and family `g`, we have `f (sup_i g i) = sup_i f (g i)`.
More concisely: If `F` is a sup-semilattice homomorphism from a SupSet `α` to a SupSet `β`, then `F (sup_i g i) = sup_i F (g i)`.
|
FrameHom.ext
theorem FrameHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f g : FrameHom α β},
(∀ (a : α), f a = g a) → f = g
This theorem, `FrameHom.ext`, states that for any two frame homomorphisms `f` and `g` between two complete lattices (of types `α` and `β`), if `f` and `g` are equal at every element `a` of the lattice `α`, then `f` and `g` are indeed the same frame homomorphism. In other words, two frame homomorphisms are equal if they act the same on every element of their domain.
More concisely: Two frame homomorphisms between complete lattices are equal if and only if they map every element to the same image.
|
CompleteLatticeHom.ext
theorem CompleteLatticeHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
{f g : CompleteLatticeHom α β}, (∀ (a : α), f a = g a) → f = g
This theorem states that for any two types `α` and `β`, both of which have a `CompleteLattice` structure, any two functions `f` and `g` from `α` to `β` that are `CompleteLatticeHom` (complete lattice homomorphisms), are equal if and only if they map every element of `α` to the same element in `β`. Essentially, it's saying that two complete lattice homomorphisms are identical if they behave the same way on all inputs.
More concisely: Given types `α` and `β` with `CompleteLattice` structures, two functions `f` and `g` from `α` to `β` are equal as complete lattice homomorphisms if and only if they map every element of `α` to the same image in `β`.
|
sInfHom.ext
theorem sInfHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] {f g : sInfHom α β},
(∀ (a : α), f a = g a) → f = g
This theorem states that for any two set-infimum-preserving functions `f` and `g` between two sets `α` and `β` (both of which are in the class of sets with infimum), if `f` and `g` are equal at every element of `α` (i.e., for any element `a` of `α`, `f(a)` is equal to `g(a)`), then `f` and `g` are the same function. This is a statement of function extensionality for set-infimum-preserving functions.
More concisely: If two set-infimum-preserving functions between sets with infimum agree on every element, then they are equal.
|
FrameHom.map_sSup'
theorem FrameHom.map_sSup' :
∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (self : FrameHom α β)
(s : Set α), self.toFun (sSup s) = sSup (self.toFun '' s)
This theorem states that for any two types `α` and `β`, both of which are complete lattices, and for any frame homomorphism `self` from `α` to `β`, the homomorphism commutes with the supremum (also known as join) operation. Specifically, if `s` is a set of elements in `α`, then the supremum of the images of `s` under the homomorphism is the same as the image of the supremum of `s` under the homomorphism. In mathematical terms, we can express this as `self(sup s) = sup (self(s))` for all sets `s` of elements in `α`.
More concisely: For any complete lattices α and β, and frame homomorphism self from α to β, self preserves suprema, that is, self (sup S) = sup (self S) for all sets S in α.
|
sSupHom.ext
theorem sSupHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] {f g : sSupHom α β},
(∀ (a : α), f a = g a) → f = g
This theorem, `sSupHom.ext`, states that for any two sup-semilattice homomorphisms `f` and `g` from one type `α` to another type `β` (where both `α` and `β` are sup-semilattices), if `f` and `g` agree on every element of `α` (in other words, for all `a` in `α`, `f(a)` equals `g(a)`), then `f` and `g` are proven to be equal. This demonstrates the principle of function extensionality for sup-semilattice homomorphisms.
More concisely: If two sup-semilattice homomorphisms from one sup-semilattice to another agree on every element, then they are equal.
|
CompleteLatticeHom.map_sSup'
theorem CompleteLatticeHom.map_sSup' :
∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
(self : CompleteLatticeHom α β) (s : Set α), self.toFun (sSup s) = sSup (self.toFun '' s)
The theorem `CompleteLatticeHom.map_sSup'` states that for any two complete lattices `α` and `β`, and a homomorphism between them, the homomorphism commutes with the supremum operation. More specifically, given a set `s` of elements in `α`, the supremum of `s` under the homomorphism is equal to the supremum of the image of `s` under the homomorphism, i.e., applying the homomorphism first and then taking the supremum gives the same result as taking the supremum first and then applying the homomorphism. Here, `sSup` denotes the supremum operation on a set, and `self.toFun` represents the homomorphism.
More concisely: For any complete lattices α and β and a homomorphism f: α → β, the image of the supremum of a subset s of α under f is equal to the supremum of the images of elements in s under f. In other words, f(⨆(s)) = ⨆(f(s)).
|
sInfHom.map_sInf'
theorem sInfHom.map_sInf' :
∀ {α : Type u_8} {β : Type u_9} [inst : InfSet α] [inst_1 : InfSet β] (self : sInfHom α β) (s : Set α),
self.toFun (sInf s) = sInf (self.toFun '' s)
The theorem `sInfHom.map_sInf'` states that for any types `α` and `β` equipped with an `InfSet` structure (which provides an infimum or "greatest lower bound" operation), and for any function `self` that is a supremum-preserving function (`sInfHom`) from `α` to `β`, and any set `s` of elements of type `α`, the supremum of the image of `s` under `self` is the same as the image under `self` of the supremum of `s`. In other words, the function `self` commutes with the supremum operation.
More concisely: For any supremum-preserving function `self` between infinitely-bounded types `α` and `β`, and any set `s` in `α` with an infimum, the supremum of `self` applied to `s` is equal to `self` applied to the supremum of `s`.
|