compl_sup_distrib
theorem compl_sup_distrib : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a b : α), (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
This theorem, `compl_sup_distrib`, states that for any type `α` that has a structure of Heyting Algebra, and for any two elements `a` and `b` of that type, the complement of the supremum (or join) of `a` and `b`, denoted as `(a ⊔ b)ᶜ`, is equal to the infimum (or meet) of the complements of `a` and `b`, denoted as `aᶜ ⊓ bᶜ`. In simpler terms, it means that the negation of the logical 'or' of two propositions is equivalent to the logical 'and' of their negations. This is a formulation of De Morgan's law in the context of Heyting algebra.
More concisely: In a Heyting algebra, the complement of the join (supremum) of two elements is equal to the meet (infimum) of their complements. (De Morgan's law)
|
Disjoint.sup_sdiff_cancel_right
theorem Disjoint.sup_sdiff_cancel_right :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → (a ⊔ b) \ b = a
This theorem states that for any generalized Coheyting algebra, if two elements `a` and `b` are disjoint (that is, any element that is less than or equal to both `a` and `b` is also less than or equal to the bottom element), then the result of the operation of taking the supremum (or join) of `a` and `b` and then subtracting `b` (denoted as `(a ⊔ b) \ b`) is equal to `a`. Essentially, in the context of a generalized Coheyting algebra, if `a` and `b` are disjoint, subtracting `b` from the union of `a` and `b` leaves `a` untouched.
More concisely: In a generalized Cohesion algebra, if `a` and `b` are disjoint, then `(a ⊔ b) \ b = a`.
|
sup_sdiff_right_self
theorem sup_sdiff_right_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, (a ⊔ b) \ b = a \ b
This theorem, named `sup_sdiff_right_self`, states that for any type `α` that forms a Generalized Coheyting Algebra (which is a certain type of algebraic structure), and for any two elements `a` and `b` of this type, the supremum (join) of `a` and `b`, subtracted by `b` (in the Coheyting algebra sense), is equal to `a` subtracted by `b`. This can be expressed mathematically as $(a \lor b) \setminus b = a \setminus b$, where $\lor$ denotes the supremum operation, and $\setminus$ denotes the subtraction operation in the context of a Generalized Coheyting Algebra.
More concisely: In a Generalized Coalgebra, the supremum of two elements minus one of them equals the subtraction of the same elements. That is, $(a \lor b) \setminus b = a \setminus b$.
|
BiheytingAlgebra.sdiff_le_iff
theorem BiheytingAlgebra.sdiff_le_iff :
∀ {α : Type u_4} [self : BiheytingAlgebra α] (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c
This theorem states that for all elements `a`, `b`, and `c` of a type `α` which has a Biheyting algebra structure, the residual (or relative pseudocomplement) of `a` with respect to `b` is less than or equal to `c` if and only if `a` is less than or equal to the join (supremum) of `b` and `c`. In other words, it establishes a relationship between the partial ordering in the algebra and the algebraic operations of relative pseudocomplement and join.
More concisely: For all elements `a`, `b`, and `c` in a Biheyting algebra, `a ⩽ b ∨ c` if and only if `a ⩽ b ⊔ c`, where `⩽` denotes the partial order, `∨` is the join (supremum), and `⊔` is the relative pseudocomplement.
|
sdiff_top
theorem sdiff_top : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), a \ ⊤ = ⊥
This theorem states that for any element `a` of a given type `α` in a Coheyting Algebra, the set difference of `a` and the top element `⊤` is always the bottom element `⊥`. In other words, when we subtract the largest possible element from any element in a Coheyting Algebra, we always get the smallest possible element.
More concisely: In a Cohecting Algebra, for all elements `a` in `α`, the set difference `a \ ⊤` equals the bottom element `⊥`.
|
le_compl_comm
theorem le_compl_comm : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ ↔ b ≤ aᶜ
This is a theorem in the context of Heyting Algebras, which are a kind of algebraic structure used in logic and computer science. The theorem states that for any two elements (`a` and `b`) of some Heyting Algebra, `a` is less than or equal to the complement of `b` if and only if `b` is less than or equal to the complement of `a`. This is a kind of 'commutativity' property for the order relation and the complement operation in a Heyting Algebra.
More concisely: In a Heyting Algebra, elements `a` and `b` have the same order relation to their complements, that is, `a ≤ ¬b` if and only if `b ≤ ¬a`.
|
sdiff_bot
theorem sdiff_bot : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a : α}, a \ ⊥ = a
This theorem, `sdiff_bot`, states that for any type `α` that forms a Generalized Coheyting Algebra, the set difference of any element `a` and the bottom element (denoted as ⊥) is equal to `a` itself. In the context of set theory, this is akin to saying that subtracting the empty set from any set results in the original set.
More concisely: For any type `α` forming a Generalized Cohen algebra in Lean 4, `a \ ⊥ = a` for all `a : α`.
|
compl_top
theorem compl_top : ∀ {α : Type u_2} [inst : HeytingAlgebra α], ⊤ᶜ = ⊥
This theorem states that for any type `α` that is a Heyting algebra, the pseudocomplement `⊤ᶜ` of the top element `⊤` is equal to the bottom element `⊥`. In other words, in the context of a Heyting algebra, the "inverse" or "opposite" of the top element is the bottom element.
More concisely: In a Heyting algebra, the pseudocomplement of the top element is equal to the bottom element.
|
sup_sdiff_self
theorem sup_sdiff_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊔ b \ a = a ⊔ b := by
sorry
This theorem states that for all types `α` that form a Generalized Coheyting Algebra, given any two elements `a` and `b` of `α`, the supremum (or the least upper bound) of `a` and the difference of `b` and `a` is equivalent to the supremum of `a` and `b`. In mathematical terms, we have `a ∨ (b \ a) = a ∨ b` for all elements `a` and `b` in the algebra.
More concisely: For all types `α` that form a lattice and for all elements `a, b` in `α`, the supremum of `a` and the difference `b - a` is equal to the supremum of `a` and `b`.
|
hnot_le_iff_codisjoint_left
theorem hnot_le_iff_codisjoint_left : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, ￢a ≤ b ↔ Codisjoint b a
This theorem states that for any type `α` that forms a Coheyting algebra, and any two elements `a` and `b` of that type, `a` is not less than or equal to `b` if and only if `b` and `a` are codisjoint. In the context of a lattice, two elements `a` and `b` are said to be codisjoint if, for any element `x` such that `a` and `b` are both less than or equal to `x`, the top element of the lattice is less than or equal to `x`. The theorem establishes a correspondence between the non-existence of a partial order relationship (not less than or equal) between two elements and their codisjointness in the lattice structure of a Coheyting algebra.
More concisely: In a Coheting algebra, elements are codisjoint if and only if they have no partial order relationship.
|
sup_sdiff_left_self
theorem sup_sdiff_left_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, (a ⊔ b) \ a = b \ a
This theorem, `sup_sdiff_left_self`, applies to a generalized co-heyting algebra of any type `α`. It states that for any two elements `a` and `b` of this algebra, the supremum (or join) of `a` and `b` subtracted by `a` (often written in mathematical notation as `(a ⊔ b) \ a`) is equal to `b` subtracted by `a` (`b \ a`). This theorem captures one of the fundamental properties of generalized co-heyting algebras.
More concisely: In a generalized co-Heyting algebra, the join of two elements and their difference are equal: (a ⊔ b) \ a = b \ a.
|
himp_himp
theorem himp_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇨ c = a ⊓ b ⇨ c
This theorem states that for any type `α` that forms a Generalized Heyting Algebra, and for any three elements `a`, `b`, and `c` of this type, the Heyting implication of `a` to the Heyting implication of `b` to `c` equals the Heyting implication of `a` infimum `b` to `c`. Here, `⇨` is the Heyting implication, and `⊓` is the infimum (also known as the 'greatest lower bound' or 'meet').
More concisely: For any type `α` forming a Generalized Heyting Algebra and any elements `a`, `b`, and `c` of `α`, `a ⇨ (b ⇨ c)` equals `(a ⊓ b) ⇨ c`.
|
inf_compl_self
theorem inf_compl_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), a ⊓ aᶜ = ⊥
This theorem states that for any type `α` that forms a Heyting algebra, the infimum (or greatest lower bound) of any element `a` and its complement `aᶜ` is the bottom element (`⊥`). In simple terms, the intersection of any element and its complement in a Heyting algebra is always the smallest element in the algebra.
More concisely: In a Heyting algebra, the infimum of any element and its complement is the bottom element.
|
hnot_inf_distrib
theorem hnot_inf_distrib : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a b : α), ￢(a ⊓ b) = ￢a ⊔ ￢b
This theorem states that for any type `α` that forms a co-Heyting algebra, the complement (denoted by `￢`) of the infimum (denoted by `⊓`, also often referred to as the 'meet' or 'greatest lower bound') of any two elements `a` and `b` of that type is equal to the supremum (denoted by `⊔`, also often referred to as the 'join' or 'least upper bound') of their individual complements. In mathematical notation, this can be written as `￢(a ⊓ b) = ￢a ⊔ ￢b`. This is an important property in the theory of co-Heyting algebras.
More concisely: In a co-Heyting algebra, the complement of the infimum of two elements is equal to the supremum of their individual complements: `￢(a ⊓ b) = ￢a ⊔ ￢b`.
|
compl_bot
theorem compl_bot : ∀ {α : Type u_2} [inst : HeytingAlgebra α], ⊥ᶜ = ⊤
This theorem states that for all types `α` that form a Heyting algebra, the complement of the bottom element, denoted as `⊥` (such equivalent to false in boolean algebra), is equal to the top element, denoted as `⊤` (such equivalent to true in boolean algebra). This is analogous to the law in classical logic where the negation of false is true.
More concisely: In a Heyting algebra, the complement of the bottom element is equal to the top element.
|
sdiff_le
theorem sdiff_le : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ a
This theorem states that for any type `α` which has a structure of a Generalized Coheyting Algebra, and for any two elements `a` and `b` of this type, the difference of `a` and `b` (`a \ b`) is always less than or equal to `a`. In mathematical terms, this can be denoted as $a \setminus b \leq a$.
More concisely: For any Generalized Cohen algebra `α`, and for all `a, b` in `α`, `a \ b ≤ a`.
|
compl_le_compl
theorem compl_le_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ b → bᶜ ≤ aᶜ
This theorem states that for any given type `α` that is a Heyting algebra, and any two elements `a` and `b` of this type, if `a` is less than or equal to `b`, then the pseudocomplement of `b` is less than or equal to the pseudocomplement of `a`. In other words, the order is reversed when taking pseudocomplements in a Heyting algebra.
More concisely: In a Heyting algebra, for all elements `a` and `b`, if `a ≤ b` then the pseudocomplement of `b` is less than or equal to the pseudocomplement of `a` (denoted as `⊥b ≤ ⊥a`).
|
le_himp
theorem le_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b ⇨ a
This theorem, `le_himp`, states that for any type `α` that forms a Generalized Heyting Algebra, for any elements `a` and `b` of that type, if `a` is less than or equal to `b`, this implies `a`. In mathematical terms, given a Generalized Heyting Algebra, this theorem is about the order-theoretic relation (≤) between its elements and the implication operation (⇨). It essentially says that if an element is less than or equal to another, it can be implied by that relation.
More concisely: In a Generalized Heyting Algebra, for all elements `a` and `b`, if `a` is less than or equal to `b`, then `a` implies `b`.
|
sdiff_eq_bot_iff
theorem sdiff_eq_bot_iff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b = ⊥ ↔ a ≤ b := by
sorry
This theorem states that for any type `α` that forms a generalized coheyting algebra, and for any two elements `a` and `b` of type `α`, the difference (`a \ b`) is equivalent to the bottom element (`⊥`) if and only if `a` is less than or equal to `b`. In other words, in a generalized coheyting algebra, an element `a` is less than or equal to another element `b` precisely when the difference of `a` and `b` is the bottom element.
More concisely: In a generalized cohesheaf algebra, two elements `a` and `b` are equivalent to the bottom element if and only if `a` is less than or equal to `b` in terms of their difference.
|
Codisjoint.himp_eq_right
theorem Codisjoint.himp_eq_right :
∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → b ⇨ a = a
This theorem states that for any Generalized Heyting Algebra, if two elements 'a' and 'b' are codisjoint, then the Heyting implication of 'b' by 'a', denoted as 'b ⇨ a', is equal to 'a'. In the context of Heyting algebras, 'b ⇨ a' is the largest element 'c' such that 'b ∧ c ≤ a'. Here, 'codisjoint' means that for any element 'x' in the algebra, if 'a' and 'b' are less than or equal to 'x', then the top element of the algebra is less than or equal to 'x'.
More concisely: In a Generalized Heyting Algebra, if elements 'a' and 'b' are codisjoint, then 'b ⇨ a' equals 'a'. Alternatively, the largest element 'c' satisfying 'b ∧ c ≤ a' is 'a' for codisjoint 'a' and 'b'.
|
Disjoint.le_compl_right
theorem Disjoint.le_compl_right : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, Disjoint a b → a ≤ bᶜ := by
sorry
This theorem, named `Disjoint.le_compl_right`, states that for any Heyting algebra `α` and any elements `a` and `b` of that algebra, if `a` and `b` are disjoint (meaning their infimum is the bottom element of the lattice), then `a` is less than or equal to the complement of `b`. In other words, the theorem provides an alias for the reverse direction of another theorem `le_compl_iff_disjoint_right`, establishing a connection between the concept of disjoint elements in a lattice and the order relation in the context of Heyting algebras.
More concisely: In a Heyting algebra, if two elements are disjoint, then one is less than or equal to the complement of the other.
|
sup_sdiff_self_right
theorem sup_sdiff_self_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊔ b \ a = a ⊔ b
This theorem, named `sup_sdiff_self_right`, states that for any type `α` that forms a Generalized Coheyting Algebra, for any two elements `a` and `b` of that type, the supremum (join) of `a` and the set difference of `b` and `a` is equal to the supremum of `a` and `b`. In the context of a Generalized Coheyting Algebra, the set difference operation is interpreted as a kind of 'relative complement': `b \ a` represents the part of `b` that is not in `a`. Thus, the theorem essentially states that 'adding' this 'relative complement' to `a` via the supremum operation does not change the supremum of `a` and `b`.
More concisely: In a Generalized Coheting Algebra, the supremum of an element and the set difference of another element from it is equal to the supremum of the two elements.
|
compl_compl_compl
theorem compl_compl_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), aᶜᶜᶜ = aᶜ
This theorem states that for any type `α` that forms a Heyting algebra (a structure that includes operations for 'and', 'or', and an implication operation), the triple complement of an element `a` in `α` (denoted as `aᶜᶜᶜ`) is equal to the single complement of `a` (denoted as `aᶜ`). This is analogous to how in boolean algebra, double negation returns the original value, but in a Heyting algebra, triple negation returns the single negation.
More concisely: In a Heyting algebra, the triple negation of an element equals the single negation. That is, `aᶜᶜᶜ = aᶜ` for any `a` in the algebra.
|
sdiff_idem
theorem sdiff_idem : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, (a \ b) \ b = a \ b
This theorem states that for any type `α` that forms a `GeneralizedCoheytingAlgebra`, and for any two elements `a` and `b` of `α`, the operation of subtracting `b` from `a` two times in a row is equivalent to just subtracting `b` from `a` once. In other words, `(a \ b) \ b = a \ b`. This is a property of the subtraction operation in a `GeneralizedCoheytingAlgebra`.
More concisely: In a Generalized Cohen algebra, for all elements `a` and `b`, the repeated subtraction `(a \ b) \ b` equals the single subtraction `a \ b`.
|
hnot_hnot_le
theorem hnot_hnot_le : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α}, ￢￢a ≤ a
This theorem, `hnot_hnot_le`, states that for all types `α` in a Coheyting algebra, the double negation of any element `a` of type `α` is less than or equal to `a` itself. In more mathematical terms, given any Coheyting algebra and any element `a` in that algebra, the inequality `￢￢a ≤ a` holds.
More concisely: In a Coheyting algebra, the double negation of any element is less than or equal to the element itself. (i.e. ⊥⊥a ≤ a for all a : α)
|
bot_sdiff
theorem bot_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a : α}, ⊥ \ a = ⊥
The theorem `bot_sdiff` states that for any type `α` that is a Generalized Coheyting Algebra, and for any element `a` of `α`, the pseudo-difference (denoted `\`) of the bottom element (denoted `⊥`) and `a` is equal to `⊥`. In simpler terms, subtracting any element from the smallest element of a Generalized Coheyting Algebra results in the smallest element.
More concisely: For any Generalized Coalgebra `α` and its bottom element `⊥`, we have `⊥ \ a = ⊥` for all `a` in `α`.
|
Codisjoint.hnot_le_left
theorem Codisjoint.hnot_le_left : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, Codisjoint b a → ￢a ≤ b := by
sorry
The theorem `Codisjoint.hnot_le_left` states that for any type `α` which forms a Coheyting algebra and for any elements `a` and `b` of this type, if `b` and `a` are codisjoint (which means that for any element `x` in the algebra, if `a` and `b` are less than or equal to `x`, then the top element of the algebra is less than or equal to `x`), then it is not the case that `a` is less than or equal to `b`. This is essentially saying that codisjointness implies that `a` cannot be less than or equal to `b`.
More concisely: In a cohesion algebra, if elements $a$ and $b$ are codisjoint, then $a$ is not less than or equal to $b$.
|
Disjoint.sup_sdiff_cancel_left
theorem Disjoint.sup_sdiff_cancel_left :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → (a ⊔ b) \ a = b
The theorem `Disjoint.sup_sdiff_cancel_left` states that for any type `α` that forms a Generalized Coheyting Algebra and for any elements `a` and `b` of that type, if `a` and `b` are disjoint (meaning that the greatest lower bound of `a` and `b` is the least possible element), then the result of subtracting `a` from the least upper bound of `a` and `b` yields `b`. This parallels the behavior of set subtraction in the context of disjoint sets.
More concisely: For any type `α` forming a Generalized Cohen algebra and disjoint elements `a` and `b` of `α`, the least upper bound of `a` and `b` minus `a` equals `b`.
|
sdiff_sup_self
theorem sdiff_sup_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), b \ a ⊔ a = b ⊔ a := by
sorry
This theorem states that for any type `α` that forms a Generalized Coheyting Algebra, and any two elements `a` and `b` of that type, the supremum (join operation, denoted by `⊔`) of `b` subtracted by `a` (`b \ a`) and `a` itself is equal to the supremum of `b` and `a`. In other words, removing `a` from `b` and then taking the supremum with `a` just brings us back to the supremum of `b` and `a`. This is a property specific to the structures in logic and mathematics known as Generalized Coheyting Algebras.
More concisely: For any type `α` forming a Generalized Cohesion Algebra and any `a, b` in `α`, `(b \ a) ⊔ a = b ⊔ a`.
|
top_sdiff'
theorem top_sdiff' : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), ⊤ \ a = ￢a
This theorem states that for any type `α` that forms a Coheyting Algebra, the set difference (represented by the `\` symbol) of the top element `⊤` and any element `a` from the algebra is equal to the negation (`￢a`) of `a`. In other words, when you remove `a` from the 'whole' (`⊤`), what you get is the 'not' of `a` in a Coheyting Algebra.
More concisely: In a coatomistic lattice (Coheting Algebra), the set difference between the top element and any element is equal to the negation of that element. Hence, ⊤ \ a = ￢a.
|
disjoint_compl_left
theorem disjoint_compl_left : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, Disjoint aᶜ a
The theorem `disjoint_compl_left` states that for any type `α` that forms a Heyting algebra, and any element `a` of this type, `a` and its complement `aᶜ` are disjoint. This means that for any other element `x` of `α`, if `x` is less than or equal to both `a` and `aᶜ`, then `x` is less than or equal to the bottom element of the Heyting algebra. The bottom element is the smallest element of the algebra, often denoted as `⊥`. This theorem is a generalization of the concept of disjoint sets in set theory, where two sets are disjoint if their intersection is the empty set.
More concisely: For any Heyting algebra type `α` and element `a`, if `a` and its complement `aᶜ` are elements of `α`, then they are disjoint, meaning that their meet is the bottom element `⊥` of the Heyting algebra.
|
HeytingAlgebra.himp_bot
theorem HeytingAlgebra.himp_bot : ∀ {α : Type u_4} [self : HeytingAlgebra α] (a : α), a ⇨ ⊥ = aᶜ
This theorem states that for any Heyting algebra and any element `a` of this algebra, `a ⇨ ⊥` is equal to the complement of `a`. In other words, the Heyting implication operation of `a` towards the bottom element of the algebra gives you the complement of `a`. This theorem establishes an important property of Heyting algebras and is related to the concept of adjoint functors where `a ⇨` is a right adjoint to `a ⊓`.
More concisely: In any Heyting algebra, the implication of an element `a` with the bottom element `⊥` equals its complement. That is, `a ⇨ ⊥ = ⓐ(a)`.
|
sup_sdiff_cancel_right
theorem sup_sdiff_cancel_right :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ b → a ⊔ b \ a = b
This theorem, `sup_sdiff_cancel_right`, states that for all types `α` given that `α` is a Generalized Coheyting Algebra, for any elements `a` and `b` of type `α`, if `a` is less than or equal to `b`, then the supremum of `a` and the set difference of `b` and `a` is equal to `b`. In mathematical terms, if $a \leq b$ then $a \cup (b \setminus a) = b$. This theorem is essentially capturing the property that in a Generalized Coheyting Algebra, adding back the difference of a set with a subset gives the original set.
More concisely: In a Generalized Coheting Algebra, for all elements `a` and `b`, if `a` is less than or equal to `b`, then `a ∪ (b \backslash a) = b`.
|
sdiff_sup_cancel
theorem sdiff_sup_cancel : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b ≤ a → a \ b ⊔ b = a
The theorem `sdiff_sup_cancel` states that for any type `α` that is a Generalized CoHeyting Algebra, and any two elements `a` and `b` of this type such that `b` is less than or equal to `a`, the supremum (or join operation) of the difference of `a` and `b` (denoted as `a \ b`) and `b` itself equals `a`. In other words, if you subtract `b` from `a` and then take the supremum of the result with `b`, you get back `a`. This resembles the property of canceling terms in real number arithmetic, but within the context of a generalized CoHeyting algebra.
More concisely: For any Generalized CoHeyting Algebra type `α` and elements `a` and `b` with `b ≤ a`, the supremum of `a \ b` and `b` equals `a`.
|
sdiff_le_comm
theorem sdiff_le_comm : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a \ c ≤ b := by
sorry
This theorem states that for any three elements `a`, `b`, and `c` of a type `α` that is a Generalized Coheyting Algebra, the statement "the set difference of `a` and `b` is less than or equal to `c`" is equivalent to the statement "the set difference of `a` and `c` is less than or equal to `b`". Here, the less than or equal operation is defined in the context of the Generalized Coheyting Algebra structure.
More concisely: In a Generalized Coalgebra, the set difference `a \ b` is equivalent to `a \ c` if and only if `b` is less than or equal to `c` in the order defined by the Coalgebra structure.
|
le_sdiff_sup
theorem le_sdiff_sup : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ b
This theorem states that for any type `α` that forms a Generalized Coheyting Algebra and any two elements `a` and `b` of this type, `a` is less than or equal to the supremum of `a` subtract `b` and `b`. In other words, in such an algebra, any element `a` is always less than or equal to the join of the difference of `a` and `b` with `b` itself. In the language of set theory, if we think of `\` as set difference and `⊔` as union, this is saying that any set `a` is always a subset of the union of `a` without `b` and `b`.
More concisely: For any type `α` forming a Generalized Codense lattice and any `a, b` in `α`, `a ≤ a⊕ b`, where `⊕` denotes the join operation and `⊓` the meet operation, hence `a⊕ b` is the supremum of `a` and `b`, such that `a ⊓ (−b) = a − b`.
|
GeneralizedCoheytingAlgebra.sdiff_le_iff
theorem GeneralizedCoheytingAlgebra.sdiff_le_iff :
∀ {α : Type u_4} [self : GeneralizedCoheytingAlgebra α] (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c
This theorem is stating a property about a generalized Coheyting algebra. Specifically, it is asserting that for all elements `a`, `b`, and `c` of a type `α` that forms a generalized Coheyting algebra, the slash operation `\` on `a` and `b` is less than or equal to `c` if and only if `a` is less than or equal to the join operation `⊔` of `b` and `c`. This is effectively stating that the slash operation `\` is the right adjoint to the join operation `⊔`.
More concisely: For all elements `a, b, c` in a generalized Coheyting algebra, `a \ b ≤ c` if and only if `a ≤ b ⊔ c`.
|
disjoint_compl_right
theorem disjoint_compl_right : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, Disjoint a aᶜ
This theorem states that for any type `α` that forms a Heyting Algebra, any element `a` of that type is disjoint with its complement `aᶜ`. In other words, for every element `x` that is less than or equal to `a` and less than or equal to `aᶜ`, `x` must also be less than or equal to the bottom element of the algebra. In the context of lattice theory, the bottom element is often represented as `⊥`, and this theorem essentially says that the meet (greatest lower bound) of `a` and `aᶜ` is `⊥`, generalizing the concept of disjoint sets.
More concisely: In a Heyting Algebra, for all elements `a`, `a` and `a`'s complement `aᶜ` have an empty meet, that is, there does not exist any element that is less than or equal to both `a` and `a`'s complement.
|
sdiff_sdiff_sdiff_le_sdiff
theorem sdiff_sdiff_sdiff_le_sdiff :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ (a \ c) ≤ c \ b
This theorem states that for any generalized coheyting algebra (a certain kind of algebraic structure), for any elements `a`, `b`, and `c` in that structure, the set difference of `a` and `b`, further subtracted by the set difference of `a` and `c`, is always less than or equal to the set difference of `c` and `b`. In symbolic form, this is $(a \setminus b) \setminus (a \setminus c) \leq c \setminus b$. This theorem is a general property that holds in all generalized coheyting algebras.
More concisely: In any generalized cohesheaf topos, for all elements a, b, and c, the subset difference a \ b \ included in the subset difference c \ b holds, that is, (a \ b) \ subseteq (c \ b). (Note: I assumed you meant subset difference instead of set difference as the symbol \ is often used for subset difference in Lean.)
|
codisjoint_hnot_right
theorem codisjoint_hnot_right : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α}, Codisjoint a (￢a)
The theorem `codisjoint_hnot_right` states that for any type `α` that forms a Coheyting algebra, any element `a` of this type is codisjoint from its complement `￢a`. In other words, for any element `a` and its complement `￢a` in the Coheyting algebra `α`, any element `x` in `α` that is greater than or equal to both `a` and `￢a` must be the top element `⊤` of `α`.
More concisely: In a Coheting algebra, for all elements `a` and their complements `¬a`, any element `x` greater than or equal to both `a` and `¬a` is the top element `⊤`.
|
sup_sdiff
theorem sup_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a ⊔ b) \ c = a \ c ⊔ b \ c
This theorem states that for any type α that has been declared an instance of a Generalized Coheyting Algebra, the supremum (also known as the join or least upper bound, denoted by ⊔) of two elements `a` and `b` subtracted by another element `c` (denoted by \) is equal to the supremum of `a` subtracted by `c` and `b` subtracted by `c`. In other words, the difference operation distributes over the supremum or join operation in a Generalized Coheyting Algebra.
More concisely: In a Generalized Coheting Algebra, the supremum of (a - c) and (b - c) equals (a \ b) for any elements a, b, and c.
|
himp_self
theorem himp_self : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a : α}, a ⇨ a = ⊤
This theorem states that for all types 'α' in a generalized Heyting algebra, the implication of any element 'a' by itself is equal to the top element. In other words, in any such algebra, asserting that 'a' implies 'a' is always a tautology.
More concisely: In a generalized Heyting algebra, for all types 'α' and elements 'a' in 'α', a implies a is equal to the top element.
|
IsCompl.compl_eq
theorem IsCompl.compl_eq : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, IsCompl a b → aᶜ = b
This theorem states that for any type `α` that forms a Heyting algebra, and any two elements `a` and `b` of that type, if `a` and `b` are complements of each other (as described by the `IsCompl` property), then the pseudocomplement of `a` (`aᶜ`) is equal to `b`. A Heyting algebra is a type of algebra used in mathematical logic and computer science, and the pseudocomplement is a generalized form of the concept of "not" for these types of algebras.
More concisely: In a Heyting algebra, if two elements `a` and `b` are complements of each other (i.e., `a` and `b` satisfy `a ∧ b = �bot` and `a ∨ b = ⊤`), then `aᶜ = b`.
|
himp_inf_le
theorem himp_inf_le : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, (a ⇨ b) ⊓ a ≤ b
This is a theorem from the domain of generalized Heyting algebras. It states that for any type `α` that has a structure of a generalized Heyting algebra, and for any two elements `a` and `b` of this type, the meet (infimum) of the implication from `a` to `b` and `a` itself is always less than or equal to `b`. In terms of logic, this theorem describes a property of the implication operation in intuitionistic logic, which is the logic underlying Heyting algebras.
More concisely: In any generalized Heyting algebra, for all elements `a` and `b`, the implication `a => b` implies `a <= b`.
|
le_compl_of_le_compl
theorem le_compl_of_le_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ → b ≤ aᶜ
This theorem, `le_compl_of_le_compl`, is an alias for the forward direction of `le_compl_comm`. It states that for any type `α` that forms a Heyting Algebra, if a given element `a` is less than or equal to the complement of another element `b`, then `b` is less than or equal to the complement of `a`. In terms of lattice theory, if an element is below the complement of another, then the second is below the complement of the first.
More concisely: If `α` is a Heyting Algebra and `a ≤ b`, then `b ≤ ��heap a`, where `��heap` denotes the complement operator.
|
himp_eq_top_iff
theorem himp_eq_top_iff : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇨ b = ⊤ ↔ a ≤ b
This is the **deduction theorem** in the framework of a Generalized Heyting Algebra model for intuitionistic logic. For any two elements `a` and `b` in any type `α` that forms a Generalized Heyting Algebra, the implication from `a` to `b` holds if and only if `a` is less than or equal to `b`. Here the implication is represented as `a ⇨ b`, and `⊤` represents the top element or the truth value in the algebraic structure; the statement `a ⇨ b = ⊤` is asserting that the implication from `a` to `b` is true.
More concisely: In a Generalized Heyting Algebra, an implication from element `a` to `b` holds if and only if `a` is below `b` in the lattice structure.
|
himp_inf_distrib
theorem himp_inf_distrib :
∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)
This theorem, `himp_inf_distrib`, states that for any type `α`, which forms a Generalized Heyting Algebra, and for any elements `a`, `b`, and `c` of that type, the operation `a` implies `(b` and `c)` is equal to `(a` implies `b)` and `(a` implies `c)`. In mathematical terms, it shows that implication distributes over the infimum (logical AND) operation in a Generalized Heyting Algebra.
More concisely: In a Generalized Heyting Algebra, the implication operation distributes over the infimum (logical AND) operation: `a implies (b and c) <-> (a implies b) and (a implies c)`.
|
compl_sup
theorem compl_sup : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
This theorem states that for any Heyting algebra (a kind of lattice-based mathematical structure) and for any two elements `a` and `b` of that algebra, the complement of the supremum (join, or least upper bound) of `a` and `b` is equal to the infimum (meet, or greatest lower bound) of the complements of `a` and `b`. Symbolically, this can be written as: `(a ∪ b)' = a' ∩ b'`.
More concisely: For any Heyting algebra, the complement of the join (supremum) of two elements is equal to the meet (infimum) of their complements: `(a ∪ b)' = a' ∩ b'`.
|
himp_bot
theorem himp_bot : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), a ⇨ ⊥ = aᶜ
This theorem, `himp_bot`, states that for any type `α` that forms a Heyting algebra, the Heyting implication of any element `a` towards the bottom element (representing "false" or "zero" in the algebra) is equal to the logical complement (or negation) of `a`. In terms of logic, it essentially states that "if `a` implies `false`, then `a` must be false", hence `a` is not true, or `a`'s complement.
More concisely: For any element `a` in a Heyting algebra, `a → ⊥ = ⊢(a)`, where `⊥` denotes the bottom element, `⊢` is the logical complement, and `→` denotes Heyting implication.
|
inf_compl_eq_bot
theorem inf_compl_eq_bot : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, a ⊓ aᶜ = ⊥
This theorem states that for any type `α` that forms a Heyting algebra, the infimum (greatest lower bound) of any element `a` and its complement `aᶜ` is equal to the bottom element `⊥` of the algebra. In other words, in any Heyting algebra, any element and its complement have no common elements, represented by the bottom element of the algebra.
More concisely: In any Heyting algebra, the infimum of an element and its complement is the bottom element.
|
Codisjoint.hnot_le_right
theorem Codisjoint.hnot_le_right : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, Codisjoint a b → ￢a ≤ b := by
sorry
In the context of a Coheyting Algebra `α`, the theorem `Codisjoint.hnot_le_right` states that for any elements `a` and `b` of `α`, if `a` and `b` are codisjoint, then it is not the case that `a` is less than or equal to `b`. In other words, `a` being codisjoint with `b` implies that `a` cannot be less than or equal to `b`. Here, two elements are said to be codisjoint if the supremum (greatest lower bound) of any element greater than or equal to both `a` and `b` is the top element of the lattice.
More concisely: In a Cohesion Algebra, if elements $a$ and $b$ are codisjoint, then $a$ is not less than or equal to $b$. (Two elements $a$ and $b$ are codisjoint if their supremum is the top element of the lattice.)
|
sdiff_inf
theorem sdiff_inf : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ (b ⊓ c) = a \ b ⊔ a \ c
This theorem, `sdiff_inf`, states that for all types `α` in a Generalized Coheyting Algebra, and for any three elements `a`, `b`, `c` of this type, the set difference of `a` and the infimum (greatest lower bound) of `b` and `c` is equal to the supremum (least upper bound) of the set difference of `a` and `b` and the set difference of `a` and `c`. In terms of set theory, it expresses that removing elements `b` and `c` from `a` simultaneously is equivalent to removing `b` from `a` and `c` from `a` separately, and then taking the union of the two results.
More concisely: For all types `α` in a Generalized Cohen algebra and all elements `a`, `b`, `c` of `α`, `a \ (inf b c) = sup (a \ b) (a \ c)`.
|
le_sup_sdiff
theorem le_sup_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ b ⊔ a \ b
This theorem states that for any type `α` that forms a Generalized Coheyting Algebra, and for any elements `a` and `b` of type `α`, `a` is less than or equal to the sup (supremum) of `b` and the set difference `a \ b`. In mathematical terms, this can be written as: ∀ a, b ∈ α, a ≤ sup(b, a \ b).
More concisely: For any Generalized Cocompleteness Algebra type `α` and elements `a, b` in `α`, `a` is less than or equal to the supremum of `b` and the set difference `a \ b`. Mathematically expressed: `∀ a, b ∈ α, a ≤ sup(b, a \ b)`.
|
Disjoint.sdiff_eq_left
theorem Disjoint.sdiff_eq_left :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → a \ b = a
This theorem states that for any generalized coheyting algebra `α` and any two elements `a` and `b` of `α`, if `a` and `b` are disjoint (in other words, their greatest lower bound (infimum) is the bottom element `⊥` of `α`), then the difference of `a` and `b` (denoted `a \ b`), is equal to `a`. In mathematical terms, if `a` and `b` are disjoint in the lattice sense, then removing `b` from `a` leaves `a` unchanged.
More concisely: If `α` is a generalized coheta algebra and `a` and `b` in `α` are disjoint, then `a \ b = a`.
|
le_himp_iff
theorem le_himp_iff : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ a ⊓ b ≤ c := by
sorry
This theorem states that for all types `α` that have a structure of a Generalized Heyting Algebra, and for any `a`, `b`, and `c` of type `α`, `a` is less than or equal to the Heyting implication of `b` and `c` if and only if the infimum (greatest lower bound) of `a` and `b` is less than or equal to `c`.
More concisely: For any type `α` with a Generalized Heyting Algebra structure and any elements `a`, `b`, and `c` of type `α`, `a ≤ i(b, c)` if and only if `inf(a, b) ≤ c`, where `i` denotes Heyting implication and `inf` denotes the infimum.
|
Codisjoint.himp_le_of_right_le
theorem Codisjoint.himp_le_of_right_le :
∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, Codisjoint a c → b ≤ a → c ⇨ b ≤ a
This theorem states that, given any three elements `a`, `b`, and `c` of a Generalized Heyting Algebra (which is a type of algebra that generalizes the concepts of an order and a lattice), if `a` and `c` are codisjoint (meaning that their supremum is the top element of the lattice) and `b` is less than or equal to `a`, then the "implication" of `c` and `b` (represented by `c ⇨ b`) is less than or equal to `a`. In other words, if `a` and `c` do not overlap and `b` is contained within `a`, then `b` cannot extend beyond `a` when "implied by" `c`. This theorem is a less general version of the `himp_le` theorem in the context of Boolean algebras.
More concisely: In a Generalized Heyting Algebra, if elements `a`, `b`, and `c` satisfy `a` and `c` are codisjoint and `b ≤ a`, then `c ⇨ b ≤ a`.
|
GeneralizedHeytingAlgebra.le_himp_iff
theorem GeneralizedHeytingAlgebra.le_himp_iff :
∀ {α : Type u_4} [self : GeneralizedHeytingAlgebra α] (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c
This theorem, named `GeneralizedHeytingAlgebra.le_himp_iff`, states that, in a Generalized Heyting Algebra, the operation `a ⇨` is right adjoint to `a ⊓`. This means that for any elements `a`, `b`, and `c` of the algebra, `a` is less than or equal to `b ⇨ c` if and only if `a ⊓ b` is less than or equal to `c`. In other words, the operation `a ⇨` captures the essence of implication (or residuation) in the logic system represented by the Generalized Heyting Algebra.
More concisely: In a Generalized Heyting Algebra, for all elements `a`, `b`, and `c`, `a ≤ b ⇨ c` if and only if `a ⊓ b ≤ c`.
|
sdiff_le_sdiff_left
theorem sdiff_le_sdiff_left :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ b → c \ b ≤ c \ a
This theorem defines a property of generalized coheyting algebras. In particular, it states that for any given type `α` that forms a generalized coheyting algebra, if `a` is less than or equal to `b`, then the difference of `c` and `b` is less than or equal to the difference of `c` and `a`. Here, '\ ' denotes the operation of set-difference in the algebra.
More concisely: For any type `α` forming a generalized cohetning algebra in Lean 4 and any elements `a ≤ b` in `α`, we have `b \ a ≤ c \ a` for any `c` in `α`.
|
le_compl_iff_disjoint_right
theorem le_compl_iff_disjoint_right : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ ↔ Disjoint a b := by
sorry
The theorem `le_compl_iff_disjoint_right` states that for any Heyting algebra `α` and elements `a` and `b` of that algebra, `a` is less than or equal to the complement of `b` if and only if `a` and `b` are disjoint. Here, 'disjoint' means that any element `x` of the algebra that is less than or equal to both `a` and `b` is actually less than or equal to the bottom element of the algebra. This extends the definition of disjointness to wider classes of ordered structures, beyond just sets.
More concisely: In a Heyting algebra, elements $a$ and $b$ are disjoint if and only if $a \leq \neg b$, where $\neg$ denotes the complement operator.
|
sdiff_sdiff_comm
theorem sdiff_sdiff_comm :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ c = (a \ c) \ b
This theorem states that for any type `α` that forms a Generalized Coheyting Algebra, and for any three elements `a`, `b`, and `c` of type `α`, the operation of subtracting `b` from `a` and then subtracting `c` from the result is equal to the operation of subtracting `c` from `a` and then subtracting `b` from the result. This can be written in mathematical notation as `(a - b) - c = (a - c) - b`.
More concisely: For any type `α` that is a Generalized Cohen algebra and for all `a, b, c` in `α`, `(a - b) - c = (a - c) - b`.
|
Mathlib.Order.Heyting.Basic._auxLemma.1
theorem Mathlib.Order.Heyting.Basic._auxLemma.1 :
∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, (a ≤ b ⇨ c) = (a ⊓ b ≤ c)
This theorem is from the Mathlib library in the Order/Heyting/Basic module. It states that for all types `α` that are instances of `GeneralizedHeytingAlgebra`, and for all elements `a`, `b`, and `c` of this type, the proposition `a ≤ b ⇨ c` is equivalent to `a ⊓ b ≤ c`. In other words, the implication from `a` being less than or equal to `b` to `c` is the same as the infimum (greatest lower bound) of `a` and `b` being less than or equal to `c` in a Generalized Heyting algebra.
More concisely: In a Generalized Heyting algebra, for all elements `a`, `b`, and `c`, the implication `a ≤ b` implies `a ⊓ b ≤ c` is equivalent to `a ≤ c` given `c ≤ b`.
|
sup_sdiff_self_left
theorem sup_sdiff_self_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), b \ a ⊔ a = b ⊔ a := by
sorry
This theorem, `sup_sdiff_self_left`, is an alias of `sdiff_sup_self`. It states that for any given type `α` which is an instance of a `GeneralizedCoheytingAlgebra`, and any two elements `a` and `b` of this type, the supremum (join) of the symmetric difference of `b` and `a` with `a` is equal to the supremum of `b` and `a`. In mathematical notation, this can be written as $(b \setminus a) \cup a = b \cup a$.
More concisely: For any type `α` being a `GeneralizedCoheytingAlgebra` and any elements `a, b` of `α`, the supremum of `(b \setminus a)` and `a` equals the supremum of `b` and `a`. In Lean 4, this is represented by the theorem alias `sup_sdiff_self_left` or `sdiff_sup_self`.
|
hnot_anti
theorem hnot_anti : ∀ {α : Type u_2} [inst : CoheytingAlgebra α], Antitone hnot
The theorem `hnot_anti` states that for every type `α` that forms a co-Heyting algebra, the Heyting algebra negation function `hnot` is antitone. In other words, if `α` is a type that forms a co-Heyting algebra (a lattice with certain additional properties), and `a` and `b` are elements of `α` such that `a ≤ b`, then `hnot(b) ≤ hnot(a)`.
More concisely: For every co-Heyting algebra type `α`, the Heyting algebra negation function `hnot` is monotonic, that is, `hnot(a) ≤ hnot(b)` whenever `a ≤ b`.
|
sdiff_le_sdiff_right
theorem sdiff_le_sdiff_right :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ b → a \ c ≤ b \ c
This theorem states that for any type `α` that forms a generalized coheyting algebra, given three elements `a`, `b`, and `c` of that type, if `a` is less than or equal to `b`, then the pseudo-difference of `a` and `c` (`a \ c`) is less than or equal to the pseudo-difference of `b` and `c` (`b \ c`). This theorem can be viewed as a property of order preservation in the context of generalized coheyting algebras.
More concisely: In a generalized coheting algebra, if `a ≤ b` then `a \ c ≤ b \ c` for all elements `a, b, c` of the type.
|
codisjoint_hnot_left
theorem codisjoint_hnot_left : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α}, Codisjoint (￢a) a
The theorem `codisjoint_hnot_left` states that for any type `α` that is a co-heyting algebra, and for any element `a` of this type, the element `a` and its negation `￢a` are codisjoint. In the context of lattice theory, two elements are codisjoint if their supremum (or join) is the top element of the lattice. In other words, no matter what element `x` we choose in `α`, if both `a` and `￢a` are less than or equal to `x`, then the top element of the lattice `⊤` must also be less than or equal to `x`.
More concisely: For any co-heyting algebra type `α` and its elements `a` and `¬a`, if `a` and `¬a` are less than or equal to any element `x` in `α`, then their supremum (join) equals the top element `⊤` in `α`.
|
BiheytingAlgebra.top_sdiff
theorem BiheytingAlgebra.top_sdiff : ∀ {α : Type u_4} [self : BiheytingAlgebra α] (a : α), ⊤ \ a = ￢a
The theorem `BiheytingAlgebra.top_sdiff` states that in any Biheyting Algebra (a kind of algebraic structure used in intuitionistic logic), for any element `a` of the algebra, the pseudo-difference of the top element (⊤) and `a` is equivalent to the negation of `a`. In mathematical terms, this can be expressed as `⊤ \ a = ￢a`. This theorem is universal for all types `α` that form a Biheyting Algebra.
More concisely: In any Biheyting Algebra, the pseudo-difference of the top element and any algebra element is equivalent to the negation of that element.
|
sdiff_le_iff
theorem sdiff_le_iff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a ≤ b ⊔ c := by
sorry
This theorem, `sdiff_le_iff`, states that for any type `α` that is a `GeneralizedCoheytingAlgebra`, and for any elements `a`, `b`, and `c` of type `α`, the statement "the set difference of `a` and `b` is less than or equal to `c`" is equivalent to the statement "`a` is less than or equal to the join of `b` and `c`". In the context of a Generalized Coheyting Algebra, the join operation (`⊔`) is similar to the union operation in set theory, and the set difference operation (`\`) removes elements of the second set from the first.
More concisely: For any `α` being a `GeneralizedCoheytingAlgebra` and any elements `a`, `b`, and `c` of type `α`, `a \ b ≤ c` if and only if `a ≤ b ⊔ c`.
|
CoheytingAlgebra.top_sdiff
theorem CoheytingAlgebra.top_sdiff : ∀ {α : Type u_4} [self : CoheytingAlgebra α] (a : α), ⊤ \ a = ￢a
This theorem, `CoheytingAlgebra.top_sdiff`, states that for any type `α` that has a Coheyting algebra structure, the set difference of the top element `⊤` and any element `a` of `α` equals the negation of `a`, denoted as `￢a`. In mathematical terms, this theorem is stating that in a Coheyting algebra, "⊤ minus a" is equivalent to "not a".
More concisely: In a Coheyting algebra, the set difference of the top element and any element is equal to the negation of that element. That is, ⊤ \-- a = ¬a.
|
le_compl_compl
theorem le_compl_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, a ≤ aᶜᶜ
This theorem states that for all types `α` that form a Heyting algebra, and for any element `a` of that type, `a` is less than or equal to its double complement (`aᶜᶜ`). In the context of Heyting algebras, the double complement of an element can be interpreted as the "approximation" of that element within the logic system; this theorem asserts that the original element is never greater than this approximation.
More concisely: For all types `α` in a Heyting algebra and for all elements `a` in `α`, `a ≤ aᶜᶜ` holds.
|
sdiff_sdiff
theorem sdiff_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), (a \ b) \ c = a \ (b ⊔ c)
This theorem states that for any type `α` that forms a Generalized Coheyting Algebra (a certain type of algebraic structure), for any three elements `a`, `b`, `c` of that type, the difference of `a` and `b`, and then the difference of the result with `c`, is equal to the difference of `a` and the join (or union) of `b` and `c`. In mathematical terms, `(a \ b) \ c = a \ (b ⊔ c)`. Note that `\` represents the operation of taking the 'residual' or 'difference' in the context of Generalized Coheyting Algebras, and `⊔` represents the join operation.
More concisely: In a Generalized Coheting Algebra, the difference of an element with the join of two other elements is equal to the sequential difference of that element with each of the other two.
|
sdiff_self
theorem sdiff_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a : α}, a \ a = ⊥
This theorem states that for any type `α` which forms a Generalized Coheyting Algebra, the set difference of any element `a` with itself is always the bottom element, represented by `⊥`. In the context of a Generalized Coheyting Algebra, the bottom element typically represents the "empty" or "zero" element. Therefore, the theorem essentially says that subtracting any element from itself results in an "empty" or "zero" element in the algebraic structure.
More concisely: In a Generalized Coheting Algebra, for all types `α` and elements `a` of type `α`, `a \ a = ⊥`.
|
compl_anti
theorem compl_anti : ∀ {α : Type u_2} [inst : HeytingAlgebra α], Antitone compl
The theorem `compl_anti` states that for any type `α` that is a Heyting algebra, the complement function (`compl`) is antitone. This means that if `a` and `b` are elements of `α` and `a ≤ b`, then `compl b ≤ compl a`. In other words, the complement function reverses the order of elements in a Heyting algebra.
More concisely: For any Heyting algebra `α`, the complement function `compl` is order-reversing, i.e., `compl a ≤ compl b` whenever `a ≤ b`.
|
Disjoint.le_compl_left
theorem Disjoint.le_compl_left : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, Disjoint b a → a ≤ bᶜ
This theorem, named `Disjoint.le_compl_left`, states that for any type `α` that forms a Heyting algebra, and any two elements `a` and `b` of this type, if `b` and `a` are disjoint (meaning the greatest element `x` that is less than or equal to both `a` and `b` is the bottom element of the lattice), then `a` is less than or equal to the complement of `b`. In other words, if `b` and `a` are disjoint, then all elements of `a` are in the complement of `b`.
More concisely: If `α` is a Heyting algebra and `a` and `b` are disjoint elements of `α`, then `a ≤ komp b`, where `komp` denotes the complement operator in `α`.
|
Mathlib.Order.Heyting.Basic._auxLemma.13
theorem Mathlib.Order.Heyting.Basic._auxLemma.13 :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b ≤ c) = (a ≤ b ⊔ c)
This theorem, referred to as `Mathlib.Order.Heyting.Basic._auxLemma.13`, states that for all types `α` that form a Generalized Coheyting Algebra, and for all elements `a, b, c` of type `α`, the property that `a` subtracted from `b` is less than or equal to `c` is equivalent to the property that `a` is less than or equal to the join (`⊔`) of `b` and `c`. Using mathematical symbols, this can be written as `(a \ b ≤ c) = (a ≤ b ⊔ c)`.
More concisely: For all types `α` that form a Generalized Heyting Algebra and all elements `a, b, c` of type `α`, `a - b ≤ c` if and only if `a ≤ b ⊔ c`.
|
sdiff_inf_self_left
theorem sdiff_inf_self_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a \ (a ⊓ b) = a \ b
This theorem states that for any type `α` that has a structure of a `GeneralizedCoheytingAlgebra`, and for any two elements `a` and `b` of type `α`, the set difference of `a` and the infimum (greatest lower bound) of `a` and `b` is equal to the set difference of `a` and `b`. In mathematical notation, this is equivalent to saying: $a \setminus (a \land b) = a \setminus b$.
More concisely: For any type `α` with a `GeneralizedCoheytingAlgebra` structure and any elements `a` and `b` of type `α`, the set difference `a \ (a \aland b)` equals `a \ b`.
|
sup_himp_distrib
theorem sup_himp_distrib :
∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c)
This theorem states that in the context of a Generalized Heyting Algebra (a specific type of algebraic structure) over any type α, for any three elements a, b, and c of α, the sup-implication distribution law holds. This law indicates that the sup-implication (a join operation followed by implication) of a and b towards c is equal to the intersection of the implications from a to c and from b to c. In LaTeX, it can be written as `a ∨ b → c = (a → c) ∧ (b → c)`.
More concisely: In a Generalized Heyting Algebra, the sup-implication of a and b is equal to the intersection of their implications: a ∨ b → c = a → c ∧ b → c.
|
sdiff_inf_self_right
theorem sdiff_inf_self_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), b \ (a ⊓ b) = b \ a
This theorem states that for any type `α` that is a Generalized Coheyting Algebra, and for any two elements `a` and `b` from this type, the result of subtracting the infimum of `a` and `b` from `b` is the same as subtracting `a` from `b`. This is denoted in Lean 4 as `b \ (a ⊓ b) = b \ a`. The `\` operator denotes set difference (also known as "set subtract"), and `⊓` denotes the infimum (greatest lower bound) in the context of a Coheyting Algebra.
More concisely: In a Generalized Coheting Algebra, the set difference of an element with the infimum of that element and another element is commutative, that is, `b \ (a ⊓ b) = b \ a`.
|
sdiff_right_comm
theorem sdiff_right_comm :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), (a \ b) \ c = (a \ c) \ b
This theorem, `sdiff_right_comm`, states that for any type `α` that forms a Generalized Coheyting Algebra, and for any three elements `a`, `b`, and `c` of this type, the "set difference" operation is right-commutative. In other words, taking the set difference of `a` and `b` and then the set difference of the result with `c` yields the same result as taking the set difference of `a` and `c` and then the set difference of the result with `b`. In mathematical notation, this can be written as `(a \ b) \ c = (a \ c) \ b`.
More concisely: For any type `α` forming a Generalized Cohen algebra, the right commutativity of set difference holds: `(a \ b) \ c = (a \ c) \ b`.
|
hnot_le_iff_codisjoint_right
theorem hnot_le_iff_codisjoint_right :
∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, ￢a ≤ b ↔ Codisjoint a b
The theorem `hnot_le_iff_codisjoint_right` states that for all types `α` that form a Coheyting algebra, and for any two elements `a` and `b` of that type, `a` is not less than or equal to `b` if and only if `a` and `b` are codisjoint. Here, being codisjoint means that for all elements `x`, if `a` and `b` are both less than or equal to `x`, then the top element of the order is less than or equal to `x`. This essentially means `a` and `b` are as far apart as possible in the order, given that the supremum of `a` and `b` is the top element.
More concisely: For any type α forming a complete lattice and any elements a, b in α, a ≤ b if and only if a ∨ b = ⊤ (where ∨ is the lattice join and ⊤ is the top element) if and only if a and b are codisjoint.
|
le_compl_iff_le_compl
theorem le_compl_iff_le_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ ↔ b ≤ aᶜ
This theorem, `le_compl_iff_le_compl`, is an alias of the `le_compl_comm` theorem. It states that for any Type `α` that forms a Heyting algebra, and for any elements `a` and `b` of this type, `a` is less than or equal to the complement of `b` if and only if `b` is less than or equal to the complement of `a`. In other words, in a Heyting algebra, the order relationship between two elements is mirrored when comparing each element to the complement of the other.
More concisely: In a Heyting algebra, for all elements a and b, a <= complement(b) if and only if b <= complement(a).
|
Mathlib.Order.Heyting.Basic._auxLemma.4
theorem Mathlib.Order.Heyting.Basic._auxLemma.4 :
∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, (a ≤ b ⊓ c) = (a ≤ b ∧ a ≤ c)
This theorem, named `_auxLemma.4` in the `Mathlib.Order.Heyting.Basic` module, states that for any type `α` that is a semilattice with respect to the operation "infimum" (denoted as `⊓`), and for any elements `a`, `b`, and `c` of this type, `a` is less than or equal to the infimum of `b` and `c` if and only if `a` is less than or equal to `b` and `a` is less than or equal to `c`. In other words, `a` being less than or equal to the "minimum" of `b` and `c` is equivalent to `a` being less than or equal to both `b` and `c`.
More concisely: For any semilattic type α and elements a, b, c, a ≤ inf(b, c) if and only if a ≤ b and a ≤ c.
|
le_compl_iff_disjoint_left
theorem le_compl_iff_disjoint_left : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ ↔ Disjoint b a := by
sorry
This theorem states that for any Heyting algebra `α` and any elements `a` and `b` of `α`, `a` is less than or equal to the complement of `b` if and only if `b` and `a` are disjoint. Here, two elements are said to be disjoint if, for any element `x` that is less than or equal to both `a` and `b`, `x` is also less than or equal to the bottom element of the order. The Heyting algebra is a type of lattice that is equipped with an additional operation called relative pseudocomplement, denoted as `ᶜ`.
More concisely: For any Heyting algebra `α` and elements `a` and `b` of `α`, `a ≤ ᶜb` if and only if `a` and `b` are disjoint.
|
compl_compl_inf_distrib
theorem compl_compl_inf_distrib : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a b : α), (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ := by
sorry
This theorem states that for any type `α` that forms a Heyting algebra, and for any two elements `a` and `b` of this type, the double negation of the infimum (greatest lower bound, denoted by `⊓`) of `a` and `b` is equal to the infimum of the double negations of `a` and `b`. In mathematical terms, we can express this as `(a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ` for all `a` and `b` in `α`.
More concisely: For any type `α` that forms a Heyting algebra and any `a, b` in `α`, the double negation of their infimum equals the infimum of the double negations: `(a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ`.
|
Disjoint.le_sdiff_of_le_left
theorem Disjoint.le_sdiff_of_le_left :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, Disjoint a c → a ≤ b → a ≤ b \ c
This theorem states that in a Generalized Coheyting Algebra α, given any three elements a, b, and c such that a and c are disjoint (i.e., their infimum is the bottom element), if a is less than or equal to b, then a is less than or equal to the difference of b and c. This is a weaker version of a theorem applicable in generalized Boolean algebras, as indicated by the note to see `le_sdiff`.
More concisely: In a Generalized Lattice α, if a and c are disjoint elements with a ≤ b, then a ≤ b - c.
|
IsCompl.eq_compl
theorem IsCompl.eq_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, IsCompl a b → a = bᶜ
This theorem states that for any type `α` that forms a Heyting algebra, for any two elements `a` and `b` of this type, if `a` and `b` are complement to each other (which means `a` and `b` satisfy the properties of being complements in a Heyting algebra), then `a` is equal to the complement of `b`. The complement operation is denoted by `bᶜ` in Lean notation.
More concisely: In a Heyting algebra, if elements `a` and `b` are complements to each other, then `a = bᶜ`.
|
sdiff_sdiff_left
theorem sdiff_sdiff_left :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ c = a \ (b ⊔ c)
This theorem states that for any GeneralizedCoheytingAlgebra `α`, and for any elements `a`, `b`, and `c` of `α`, the set difference of `a` and `b` subtracted by `c` is equal to the set difference of `a` and the join of `b` and `c`. In mathematical notation, this can be written as: $ (a \setminus b) \setminus c = a \setminus (b ∪ c) $.
More concisely: For any Generalized Coalgebra `α`, the set difference `(a \setminus b) \setminus c` equals `a \setminus (b ∪ c)` for all elements `a`, `b`, and `c` of `α`.
|
himp_le_himp_left
theorem himp_le_himp_left : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b → c ⇨ a ≤ c ⇨ b
This theorem states that for any type `α` that forms a Generalized Heyting Algebra, given three elements `a`, `b`, and `c` of that type, if `a` is less than or equal to `b`, then the implication of `c` towards `a` is less than or equal to the implication of `c` towards `b`. In other words, increasing the consequent of an implication in a Heyting Algebra increases the implication itself.
More concisely: For any type `α` forming a Generalized Heyting Algebra and elements `a`, `b`, `c` of `α`, if `a ≤ b`, then `(c → a) ≤ (c → b)`.
|
hnot_hnot_hnot
theorem hnot_hnot_hnot : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), ￢￢￢a = ￢a
This theorem states that for any type `α` that forms a Coheyting Algebra, the triple negation of an element `a` of type `α` is equal to the negation of `a`. In mathematical terms, if `￢` denotes the negation operation in the Coheyting Algebra, we have `￢￢￢a = ￢a` for all `a` in `α`.
More concisely: In a Cohetting Algebra, the triple negation of an element equals the negation of that element. That is, for all `α` and `a` in `α`, `￢￢￢a = ￢a`.
|