LatticeHomClass.map_inf
theorem LatticeHomClass.map_inf :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : FunLike F α β]
[self : LatticeHomClass F α β] (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b
The theorem `LatticeHomClass.map_inf` asserts that for all types `F`, `α`, and `β`, if `α` and `β` are lattices, `F` is a function-like from `α` to `β` and `F` is a `LatticeHomClass` morphism, then the function `f` of type `F` preserves the infimum operation. In other words, for any elements `a` and `b` of type `α`, applying `f` to the infimum (`⊓`) of `a` and `b` results in the same as taking the infimum of `f(a)` and `f(b)`. Such a function `f` is said to be a lattice homomorphism.
More concisely: For any function-like `F` between lattices `α` and `β`, if `F` is a lattice homomorphism, then `F` preserves the infimum operation: `F (a ⊓ b) = F a ⊓ F b` for all `a, b` in `α`.
|
SupHomClass.map_sup
theorem SupHomClass.map_sup :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Sup α] [inst_1 : Sup β] [inst_2 : FunLike F α β]
[self : SupHomClass F α β] (f : F) (a b : α), f (a ⊔ b) = f a ⊔ f b
This theorem states that if we have a function `f` of type `F`, which is a member of the `SupHomClass` from type `α` to type `β`, and `α` and `β` both have supremum operations (denoted by `⊔`), then `f` preserves these suprema. Specifically, for any elements `a` and `b` of type `α`, the supremum of `f(a)` and `f(b)` is equal to the function `f` applied to the supremum of `a` and `b`. In mathematical terms, we can write this as `f(a ⊔ b) = f(a) ⊔ f(b)`. This means that the function `f` commutes with the supremum operation, or in other words, applying `f` doesn't change the order of the elements when taking the supremum.
More concisely: If `f` is a function from type `α` to type `β` that belongs to `SupHomClass`, and both `α` and `β` have supremum operations, then `f(a ⊔ b) = f(a) ⊔ f(b)` for all `a, b` in `α`.
|
SupBotHom.map_bot'
theorem SupBotHom.map_bot' :
∀ {α : Type u_7} {β : Type u_8} [inst : Sup α] [inst_1 : Sup β] [inst_2 : Bot α] [inst_3 : Bot β]
(self : SupBotHom α β), self.toFun ⊥ = ⊥
The theorem `SupBotHom.map_bot'` states that for any types `α` and `β` that both have supremum (`Sup`) and bottom (`Bot`) elements, a supremum-preserving bottom homomorphism (`SupBotHom`) from `α` to `β` will map the bottom element of `α` to the bottom element of `β`. In other words, under such a homomorphism, the image of the lowest possible element in `α` is the lowest possible element in `β`.
More concisely: Given types `α` and `β` with supremum and bottom elements, and a supremum-preserving homomorphism `f` from `α` to `β`, then `f(Bot α) = Bot β`.
|
map_sdiff'
theorem map_sdiff' :
∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
[inst_2 : FunLike F α β] [inst_3 : BoundedLatticeHomClass F α β] (f : F) (a b : α), f (a \ b) = f a \ f b
The theorem `map_sdiff'` states that for any types `F`, `α`, and `β` where `α` and `β` are Boolean algebras, `F` is a function-like from `α` to `β`, and `F` is a bounded lattice homomorphism, then for any function `f` of type `F` and any elements `a` and `b` of type `α`, the result of applying `f` to the set difference of `a` and `b` is equal to the set difference of the result of applying `f` to `a` and the result of applying `f` to `b`. This special case of `map_sdiff` specifies the properties of a function in a Boolean algebra context.
More concisely: For any Boolean algebra homomorphism F from α to β, the image of the set difference between two elements a and b under F is equal to the set difference of their images: F(a ∖ b) = F(a) ∖ F(b).
|
InfHom.map_inf'
theorem InfHom.map_inf' :
∀ {α : Type u_7} {β : Type u_8} [inst : Inf α] [inst_1 : Inf β] (self : InfHom α β) (a b : α),
self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
The theorem `InfHom.map_inf'` states that for any two elements `a` and `b` of a type `α` equipped with an infimum (`Inf`), if there is an infimum-preserving function (`InfHom`) from `α` to another type `β` which also has an infimum, then applying the infimum operation to `a` and `b` before applying the function is the same as applying the function to `a` and `b` individually and then taking the infimum. In mathematical terms, for an infimum-preserving function `f`, this says that `f(a ⊓ b) = f(a) ⊓ f(b)`.
More concisely: For any infimum-preserving function `f` from an infimum-equipped type `α` to another infimum-equipped type `β`, `f(Inf(a, b)) = Inf(f(a), f(b))`, where `Inf` denotes the infimum operation and `a` and `b` are elements of `α`.
|
BoundedLatticeHom.map_top'
theorem BoundedLatticeHom.map_top' :
∀ {α : Type u_7} {β : Type u_8} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] (self : BoundedLatticeHom α β), self.toFun ⊤ = ⊤
This theorem states that for any `BoundedLatticeHom` (a homomorphism between two bounded lattices), the top element of the domain lattice gets mapped to the top element of the codomain lattice. Here, `α` and `β` denote types, which are equipped with a lattice structure and a bounded order. The function `self.toFun` represents the action of the `BoundedLatticeHom` on elements of `α`, and the theorem asserts that applying `self.toFun` to the top element of `α` (denoted by `⊤`) results in the top element of `β`. In essence, `⊤` is preserved under the lattice homomorphism.
More concisely: Given any `BoundedLatticeHom` between two bounded lattices `α` and `β`, the homomorphism maps the top element `⊤` of `α` to the top element `⊤` of `β`.
|
InfTopHomClass.map_top
theorem InfTopHomClass.map_top :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Inf α] [inst_1 : Inf β] [inst_2 : Top α] [inst_3 : Top β]
[inst_4 : FunLike F α β] [self : InfTopHomClass F α β] (f : F), f ⊤ = ⊤
The theorem `InfTopHomClass.map_top` states that for any types `F`, `α`, and `β`, if `α` and `β` both have `Inf` and `Top` instances (meaning they have a least element and a greatest element, respectively), and `F` is a function-like object from `α` to `β` with an `InfTopHomClass` instance (meaning it preserves the operations of greatest and least elements), then applying a function `f` of type `F` to the greatest element of `α` yields the greatest element of `β`. In other words, an `InfTopHomClass` morphism preserves the top (greatest) element.
More concisely: Given types `α` and `β` with greatest elements `topα` and `topβ` respectively, and a function-like object `F` from `α` to `β` preserving greatest elements, then `F topα = topβ`.
|
BoundedLatticeHom.map_bot'
theorem BoundedLatticeHom.map_bot' :
∀ {α : Type u_7} {β : Type u_8} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] (self : BoundedLatticeHom α β), self.toFun ⊥ = ⊥
This theorem states that for any `BoundedLatticeHom` (a homomorphism between bounded lattices), the bottom element of the source lattice is mapped to the bottom element of the target lattice. This holds true for all types `α` and `β` that are lattices with a bounded order. In other words, a `BoundedLatticeHom` preserves the bottom element under its function.
More concisely: For any `BoundedLatticeHom` between two bounded lattices, the homomorphism maps the bottom element of the source lattice to the bottom element of the target lattice.
|
BoundedLatticeHomClass.map_bot
theorem BoundedLatticeHomClass.map_bot :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] [inst_4 : FunLike F α β] [self : BoundedLatticeHomClass F α β] (f : F), f ⊥ = ⊥
The theorem `BoundedLatticeHomClass.map_bot` states that for any types `F`, `α`, and `β`, if `α` and `β` are lattices and bounded orders, and `F` is a function-like structure from `α` to `β` that satisfies the conditions of a `BoundedLatticeHomClass`, then any morphism `f` of type `F` preserves the bottom element of the lattice, i.e., the image of the bottom element of the lattice `α` under `f` is the bottom element of the lattice `β`.
More concisely: Given types `α` and `β` as bounded lattices, and a function-like structure `F` from `α` to `β` that is a bounded lattice homomorphism, then `F` maps the bottom element of `α` to the bottom element of `β`.
|
SupBotHomClass.map_bot
theorem SupBotHomClass.map_bot :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Sup α] [inst_1 : Sup β] [inst_2 : Bot α] [inst_3 : Bot β]
[inst_4 : FunLike F α β] [self : SupBotHomClass F α β] (f : F), f ⊥ = ⊥
The theorem `SupBotHomClass.map_bot` states that for all types `F`, `α`, and `β`, if `α` and `β` are types equipped with supremum (`Sup`) and bottom (`Bot`) elements, `F` is a function-like type from `α` to `β`, and `F` has the `SupBotHomClass` property (which typically means that it preserves suprema and bottom elements), then applying a function `f` of type `F` to the bottom element of `α` produces the bottom element of `β`. In other words, the function `f` preserves the bottom element under these conditions. The proof of this theorem is omitted in this context.
More concisely: For types `α` and `β` equipped with suprema and bottom elements, and a function-like type `F` from `α` to `β` with the `SupBotHomClass` property, the application of any such function `f` : `F` to the bottom element of `α` results in the bottom element of `β`.
|
LatticeHom.ext
theorem LatticeHom.ext :
∀ {α : Type u_3} {β : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] {f g : LatticeHom α β},
(∀ (a : α), f a = g a) → f = g
This theorem, `LatticeHom.ext`, states that for any two lattice homomorphisms `f` and `g` from a lattice `α` to a lattice `β`, if `f` and `g` map any element `a` of `α` to the same element in `β`, then `f` and `g` are the same lattice homomorphism. In other words, two lattice homomorphisms are equal if they have the same action on all elements of the domain lattice.
More concisely: If two lattice homomorphisms from a lattice to another lattice map every element to the same image, then they are equal.
|
InfHomClass.map_inf
theorem InfHomClass.map_inf :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Inf α] [inst_1 : Inf β] [inst_2 : FunLike F α β]
[self : InfHomClass F α β] (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b
The theorem `InfHomClass.map_inf` states that, for all types `F`, `α`, and `β`, if `α` and `β` have an infimum operation (denoted by `⊓`), and if type `F` has a function-like mapping from `α` to `β`, then any morphism `f` which belongs to the `InfHomClass` (meaning it preserves the infimum operation) will also preserve the infimum operation in the sense that the infimum of `f(a)` and `f(b)` is equal to `f` of the infimum of `a` and `b`. In mathematical terms, it simply says that if `f` preserves the infimum operation, then `f(a ⊓ b) = f(a) ⊓ f(b)` for every `a` and `b` in the domain of `f`.
More concisely: Given types `F`, `α`, and `β` with infima, if `α` and `β`'s infima are preserved by a function-like mapping `f` from `α` to `β` in the `InfHomClass`, then `f(a ⊓ b) = f(a) ⊓ f(b)` for all `a, b` in `α`.
|
map_compl'
theorem map_compl' :
∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
[inst_2 : FunLike F α β] [inst_3 : BoundedLatticeHomClass F α β] (f : F) (a : α), f aᶜ = (f a)ᶜ
This theorem, `map_compl'`, states a special case of `map_compl` for boolean algebras. Specifically, for any two types `α` and `β` that are boolean algebras, and for any function `f` of a type `F` that acts like a function from `α` to `β` (that is, `F` is `FunLike` from `α` to `β`), and `F` also being a bounded lattice homomorphism, the complement of the output of `f` applied to a value `a` of type `α` is the same as the result of `f` applied to the complement of `a`. In other words, if `a` is a boolean value in `α`, then applying the function `f` and then taking the complement is the same as first taking the complement of `a` and then applying the function `f`.
More concisely: For any binary functions `f` between two boolean algebras that are lattice homomorphisms, applying the complement after `f` is equivalent to applying `f` after the complement.
|
BoundedLatticeHomClass.map_top
theorem BoundedLatticeHomClass.map_top :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] [inst_4 : FunLike F α β] [self : BoundedLatticeHomClass F α β] (f : F), f ⊤ = ⊤
The theorem `BoundedLatticeHomClass.map_top` states that for all type `F`, types `α`, `β` where `α` and `β` are lattices and bounded orders, and `F` is a function-like structure from `α` to `β`. If `F` is also a bounded lattice homomorphism from `α` to `β`, then for any function `f` of type `F`, the top element of `α` (denoted by `⊤`) is mapped to the top element of `β` under the function `f`. In mathematical terms, for a function `f` in the context of the mentioned structures, we have `f(⊤) = ⊤`.
More concisely: If `F` is a bounded lattice homomorphism from a lattice `α` with bounded order to a lattice `β` with bounded order, then `F(⊤) = ⊤`, where `⊤` denotes the top element of `α` and `β`.
|
LatticeHom.map_inf'
theorem LatticeHom.map_inf' :
∀ {α : Type u_7} {β : Type u_8} [inst : Lattice α] [inst_1 : Lattice β] (self : LatticeHom α β) (a b : α),
self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
This theorem states that a `LatticeHom` (lattice homomorphism), which is a function between two lattices, preserves the infimum operation. Specifically, for any two elements `a` and `b` in a lattice `α`, the infimum (`⊓`) of `a` and `b` under the lattice homomorphism equals the infimum of the images of `a` and `b` under the same homomorphism. In other words, applying the homomorphism after taking the infimum gives the same result as taking the infimum after applying the homomorphism.
More concisely: A lattice homomorphism preserves the infimum operation, i.e., for all elements `a` and `b` in a lattice, `⊓ (f a b) = f (⊓ a b)`.
|
SupHom.map_sup'
theorem SupHom.map_sup' :
∀ {α : Type u_7} {β : Type u_8} [inst : Sup α] [inst_1 : Sup β] (self : SupHom α β) (a b : α),
self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
This theorem states that a `SupHom` (supremum homomorphism) preserves the supremum operation. Specifically, for any two elements `a` and `b` of some type `α` that has a supremum operation, and given a `SupHom` from `α` to another type `β` that also has a supremum operation, the supremum of the images of `a` and `b` under the `SupHom` is the image of the supremum of `a` and `b`. In mathematical terms, this can be written as `f(a ⊔ b) = f(a) ⊔ f(b)` where `f` is the `SupHom`.
More concisely: Given two elements `a` and `b` of a type `α` with a supremum operation, and a `SupHom` function `f` from `α` to a type `β` also with supremum operation, the image of the supremum of `a` and `b` under `f` equals the supremum of the images of `a` and `b`: `f(a ⊔ b) = f(a) ⊔ f(b)`.
|
BoundedLatticeHom.ext
theorem BoundedLatticeHom.ext :
∀ {α : Type u_3} {β : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] {f g : BoundedLatticeHom α β}, (∀ (a : α), f a = g a) → f = g
This theorem states that for any two bounded lattice homomorphisms `f` and `g` between two lattices `α` and `β`, if `f` and `g` have the same output for every element `a` in lattice `α`, then `f` and `g` are the same. Here, `α` and `β` are types that form lattices with a bounded order. A bounded lattice homomorphism is a function that preserves the lattice operations and the order.
More concisely: If two bounded lattice homomorphisms between two bounded lattices agree on all lattice elements, then they are equal.
|
InfTopHom.map_top'
theorem InfTopHom.map_top' :
∀ {α : Type u_7} {β : Type u_8} [inst : Inf α] [inst_1 : Inf β] [inst_2 : Top α] [inst_3 : Top β]
(self : InfTopHom α β), self.toFun ⊤ = ⊤
This theorem states that for any type `α` equipped with an infimum (greatest lower bound) and a top element, and any type `β` also equipped with an infimum and a top element, any `InfTopHom` (an infimum-preserving function that also preserves the top element) from `α` to `β` will map the top element of `α` to the top element of `β`. In mathematical notation, this is saying that for a function `f: α -> β` that preserves infimum and the top element, we have `f(⊤_α) = ⊤_β`.
More concisely: For any functions preserving infimum and top elements between complete lattices with greatest elements, the greatest element is mapped to the greatest element.
|
map_symmDiff'
theorem map_symmDiff' :
∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
[inst_2 : FunLike F α β] [inst_3 : BoundedLatticeHomClass F α β] (f : F) (a b : α),
f (symmDiff a b) = symmDiff (f a) (f b)
The theorem `map_symmDiff'` states that for all types `F`, `α`, and `β`, given that `α` and `β` are boolean algebras, `F` is a function-like structure from `α` to `β`, and `F` is a bounded lattice homomorphism from `α` to `β`, for any function `f` of type `F` and any elements `a` and `b` of type `α`, applying `f` to the symmetric difference of `a` and `b` is equivalent to taking the symmetric difference of the images of `a` and `b` under `f`. In other words, the function `f` preserves the operation of symmetric difference under its mapping from `α` to `β`.
More concisely: For any function-like structure `F` from boolean algebras `α` and `β`, that is a bounded lattice homomorphism, the application of `F(f)` to the symmetric difference of elements `a` and `b` in `α` is equal to the symmetric difference of `F(a)` and `F(b)` in `β`.
|