HeytingHomClass.map_bot
theorem HeytingHomClass.map_bot :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β]
[inst_2 : FunLike F α β] [self : HeytingHomClass F α β] (f : F), f ⊥ = ⊥
The theorem `HeytingHomClass.map_bot` states that, for every type `F` and every pair of types `α` and `β` that are equipped with a structure of a Heyting algebra, if `F` is a type of functions from `α` to `β`, and `F` behaves like a homomorphism between Heyting algebras, then for every function `f` of type `F`, the bottom element of `α` is mapped to the bottom element of `β`. In other words, a Heyting algebra homomorphism preserves the bottom element.
More concisely: Given types equipped with Heyting algebra structures `α` and `β`, and a Heyting algebra homomorphism `F` from `α` to `β`, for all `f` in `F`, `f��xic⊥α = ⊥β`, where `⊥` denotes the bottom element.
|
BiheytingHomClass.map_sdiff
theorem BiheytingHomClass.map_sdiff :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β]
[inst_2 : FunLike F α β] [self : BiheytingHomClass F α β] (f : F) (a b : α), f (a \ b) = f a \ f b
This theorem states that for any given types `F`, `α`, and `β`, if `α` and `β` are both BiHeyting algebras, `F` is a function-like type from `α` to `β`, and `F` is a BiHeyting homomorphism class, then for any function `f` of type `F` and any elements `a` and `b` of type `α`, the difference of `a` and `b` mapped by `f` is equal to the difference of `f` mapped by `a` and `f` mapped by `b`. In other words, a BiHeyting homomorphism preserves the difference operation.
More concisely: If `F` is a function-like type from a BiHeyting algebra `α` to another BiHeyting algebra `β`, and `F` is a BiHeyting homomorphism class, then for all `a, b ∈ α`, `F(a − b) = F(a) − F(b)`.
|
CoheytingHom.ext
theorem CoheytingHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] {f g : CoheytingHom α β},
(∀ (a : α), f a = g a) → f = g
This theorem states that for any two types `α` and `β`, where `α` and `β` are both instances of the Coheyting algebra, and for any two homomorphisms `f` and `g` from `α` to `β`, if for every element `a` in `α`, `f(a)` is equal to `g(a)`, then `f` is equal to `g`. In other words, it states the principle of function extensionality for Coheyting homomorphisms: two homomorphisms between Coheyting algebras are the same if and only if they map each element of the source algebra to the same element of the target algebra.
More concisely: Given types `α` and `β` as instances of Coheyting algebras, and homomorphisms `f` and `g` from `α` to `β`, if for all `a` in `α`, `f(a) = g(a)`, then `f = g`.
|
CoheytingHom.map_sdiff'
theorem CoheytingHom.map_sdiff' :
∀ {α : Type u_6} {β : Type u_7} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] (self : CoheytingHom α β)
(a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b
This theorem states that for any co-Heyting homomorphism, the difference operation is preserved. More specifically, given any two elements `a` and `b` from a co-Heyting algebra `α`, the difference of `a` and `b` mapped via the homomorphism is equal to the difference of `a` and `b` mapped individually via the same homomorphism. This is a property related to the algebraic structure known as a co-Heyting algebra, which is a type of lattice.
More concisely: For any co-Heyting homomorphism, the operation of taking differences is preserved, that is, (h a) - (h b) = h (a - b), where h is a co-Heyting homomorphism, and a, b are elements from a co-Heyting algebra.
|
HeytingHom.map_bot'
theorem HeytingHom.map_bot' :
∀ {α : Type u_6} {β : Type u_7} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (self : HeytingHom α β),
self.toFun ⊥ = ⊥
The theorem `HeytingHom.map_bot'` states that for any two types `α` and `β`, given that they are both Heyting algebras, any Heyting homomorphism from `α` to `β` will map the bottom element of `α` to the bottom element of `β`. In other words, a Heyting homomorphism preserves the "bottom" or "smallest" element in a Heyting algebra.
More concisely: Given two Heyting algebras `α` and `β`, any Heyting homomorphism from `α` to `β` maps the bottom element of `α` to the bottom element of `β`.
|
BiheytingHom.map_himp'
theorem BiheytingHom.map_himp' :
∀ {α : Type u_6} {β : Type u_7} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] (self : BiheytingHom α β)
(a b : α), self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
The theorem states that for all types `α` and `β` which are instances of a Bi-Heyting algebra, any bi-Heyting homomorphism (denoted by `self`) preserves the Heyting implication. More precisely, if `a` and `b` are elements of `α`, then the homomorphism of the Heyting implication of `a` and `b` (`a ⇨ b`) is equal to the Heyting implication of the homomorphisms of `a` and `b` (`self.toFun a ⇨ self.toFun b`).
More concisely: For any bi-Heyting algebra homomorphism `self`: `self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b` for all `α`-elements `a` and `b`.
|
BiheytingHom.ext
theorem BiheytingHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] {f g : BiheytingHom α β},
(∀ (a : α), f a = g a) → f = g
This theorem, `BiheytingHom.ext`, states that for any two types `α` and `β`, both equipped with a structure of a Biheyting algebra, and for any two morphisms `f` and `g` from `α` to `β` in the category of Biheyting algebras, if `f` and `g` are pointwise equal (that is, for every element `a` of `α`, we have `f a = g a`), then `f` and `g` are the same morphism. This is a statement about the uniqueness of morphisms in the category of Biheyting algebras.
More concisely: In the category of Biheyting algebras, two morphisms between two Biheyting algebra structures on types with pointwise equal mappings are equal as morphisms.
|
HeytingHom.map_himp'
theorem HeytingHom.map_himp' :
∀ {α : Type u_6} {β : Type u_7} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (self : HeytingHom α β)
(a b : α), self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
The theorem `HeytingHom.map_himp'` states that for any Heyting homomorphism (a structure-preserving function between two Heyting algebras), the homomorphism preserves the Heyting implication operation. In other words, for any elements `a` and `b` of a Heyting algebra `α`, the image under the homomorphism of the Heyting implication of `a` and `b` is equal to the Heyting implication of the images of `a` and `b`. Here, `⇨` denotes the Heyting implication operation.
More concisely: Given any Heyting homomorphism between two Heyting algebras, it preserves the Heyting implication operation, that is, for all elements `a` and `b` in the algebra, `f(a ⇨ b) = f(a) ⇨ f(b)`.
|
BiheytingHom.map_sdiff'
theorem BiheytingHom.map_sdiff' :
∀ {α : Type u_6} {β : Type u_7} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] (self : BiheytingHom α β)
(a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b
This theorem states that for any given bi-Heyting homomorphism from one bi-Heyting algebra to another, the homomorphism preserves the "set difference" operation. In other words, if you take the set difference of two elements (a and b) in the original bi-Heyting algebra, and then apply the homomorphism, it's the same as if you first applied the homomorphism to each of the two elements and then took the set difference in the second bi-Heyting algebra.
More concisely: For any bi-Heyting homomorphism between two bi-Heyting algebras, the image of the set difference of two elements is the set difference of the images of those elements.
|
HeytingHomClass.map_himp
theorem HeytingHomClass.map_himp :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β]
[inst_2 : FunLike F α β] [self : HeytingHomClass F α β] (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b
The theorem `HeytingHomClass.map_himp` asserts that for any types `F`, `α`, and `β`, if `α` and `β` are Heyting algebras, `F` is a function-like term from `α` to `β`, and there is a Heyting homomorphism from `α` to `β`, then for any such homomorphism `f` and any elements `a` and `b` of `α`, the homomorphism `f` preserves the Heyting implication. That is, applying `f` to the result of the Heyting implication operation on `a` and `b` is the same as performing the Heyting implication operation on `f a` and `f b`. In mathematical terms, for all `f`, `a`, and `b`, `f(a ⇨ b) = f(a) ⇨ f(b)`.
More concisely: Given functions `F : α -> β`, `f : α -> β` a Heyting homomorphism, for all elements `a, b` in `α`, we have `f(a سXFF b) = f(a) سXFF f(b)` in `β`, where `סXFF` denotes the Heyting implication operation.
|
BiheytingHomClass.map_himp
theorem BiheytingHomClass.map_himp :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β]
[inst_2 : FunLike F α β] [self : BiheytingHomClass F α β] (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b
The theorem `BiheytingHomClass.map_himp` states that for every types `F`, `α`, and `β`, if `α` and `β` are Bi-Heyting algebras, `F` is a function-like from `α` to `β`, and `F` is a Bi-Heyting homomorphism, then any function `f : F` preserves the Heyting implication, meaning that the Heyting implication of the images under `f` of two elements of `α` is equal to the image under `f` of the Heyting implication of the two elements. In mathematical terms, for all `a` and `b` in `α`, `f(a ⇨ b) = f(a) ⇨ f(b)`.
More concisely: For any types `α` and `β` being Bi-Heyting algebras, given a function-like `F` from `α` to `β` that is a Bi-Heyting homomorphism, it preserves the Heyting implication, i.e., `F(a ⇨ b) = F(a) ⇨ F(b)` for all `α` elements `a` and `b`.
|
CoheytingHom.map_top'
theorem CoheytingHom.map_top' :
∀ {α : Type u_6} {β : Type u_7} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] (self : CoheytingHom α β),
self.toFun ⊤ = ⊤
This theorem states that for any co-Heyting homomorphism, the image of the top element of the source co-Heyting algebra under the homomorphism is the top element of the target co-Heyting algebra. In other words, a co-Heyting homomorphism preserves the top element of a co-Heyting algebra. Here, `α` and `β` are any types that have a co-Heyting algebra structure, and `self` is any co-Heyting homomorphism from `α` to `β`.
More concisely: For any co-Heyting algebra `α` and `β`, and any co-Heyting homomorphism `self` from `α` to `β`, `self (top α) = top β`.
|
CoheytingHomClass.map_top
theorem CoheytingHomClass.map_top :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β]
[inst_2 : FunLike F α β] [self : CoheytingHomClass F α β] (f : F), f ⊤ = ⊤
The theorem `CoheytingHomClass.map_top` states that, for any types `F`, `α`, `β`, if `α` and `β` are Coheyting Algebras and there is a function-like structure (`FunLike`) from `α` to `β`, and if `F` is a co-Heyting homomorphism from `α` to `β`, then applying this homomorphism to the top element in `α` yields the top element in `β`. In other words, a co-Heyting homomorphism preserves the top element of a Coheyting Algebra.
More concisely: For co-Heyting algebras α and β, and a function-like structure between them with a co-Heyting homomorphism F, F maps the top element of α to the top element of β.
|
CoheytingHomClass.map_sdiff
theorem CoheytingHomClass.map_sdiff :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β]
[inst_2 : FunLike F α β] [self : CoheytingHomClass F α β] (f : F) (a b : α), f (a \ b) = f a \ f b
This theorem states that, for all types `F`, `α`, and `β`, where `α` and `β` are co-Heyting algebras, `F` has an injective coercion to functions from `α` to `β`, and for a homomorphism (denoted by `f`) between these two co-Heyting algebras, the homomorphism preserves the "difference" operation. In mathematical terms, this means that applying the homomorphism to the result of the difference operation (`a \ b`) in `α` is the same as performing the difference operation in `β` with the results of applying the homomorphism to `a` and `b` individually; i.e., `f (a \ b) = f a \ f b`.
More concisely: Given co-Heyting algebras `α`, `β`, and a homomorphism `f` between them, the injective coercion from type `F` to functions `α → β` satisfies `f (a \ b) = f a \ f b` for all `a` and `b` in `α`.
|
HeytingHom.ext
theorem HeytingHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] {f g : HeytingHom α β},
(∀ (a : α), f a = g a) → f = g
This theorem, `HeytingHom.ext`, states that for any two Heyting algebra homomorphisms `f` and `g` from a Heyting algebra `α` to another Heyting algebra `β`, if for all elements `a` in `α` the result of applying `f` to `a` is equal to the result of applying `g` to `a`, then `f` and `g` must be the same homomorphism. In other words, two Heyting algebra homomorphisms are equal if they produce the same output for every input from the domain Heyting algebra.
More concisely: If two Heyting algebra homomorphisms from one Heyting algebra to another agree on all elements, then they are equal.
|