Disjoint.le_symmDiff_sup_symmDiff_left
theorem Disjoint.le_symmDiff_sup_symmDiff_left :
∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b c : α}, Disjoint a b → c ≤ symmDiff a c ⊔ symmDiff b c
This theorem states that for any type `α` that forms a Boolean algebra, and any elements `a`, `b`, and `c` of that type, if `a` and `b` are disjoint (meaning their greatest lower bound, or infimum, is the bottom element of the lattice), then `c` is less than or equal to the supremum (or join operation) of the symmetric difference of `a` and `c` and the symmetric difference of `b` and `c`. In mathematical terms, if `a` and `b` are disjoint, then $c \leq ((a \setminus c) \cup (b \setminus c))$. Note that the symmetric difference operation `\` is represented mathematically by set subtraction, and the supremum operation `⊔` is represented by set union.
More concisely: For any Boolean algebra type `α` and disjoint elements `a`, `b` of `α`, `c` satisfies `c ≤ (a \ b) ∪ (b \ c)`.
|
symmDiff_def
theorem symmDiff_def : ∀ {α : Type u_2} [inst : Sup α] [inst_1 : SDiff α] (a b : α), symmDiff a b = a \ b ⊔ b \ a := by
sorry
This theorem states that for all types `α` that have a supremum (denoted as `Sup α`) and set difference operations (denoted as `SDiff α`), the symmetric difference `symmDiff` of any two elements `a` and `b` of type `α` is equal to the union (supremum, denoted as `⊔`) of the set difference of `a` and `b` and the set difference of `b` and `a`. In other words, `symmDiff a b` equals `(a \ b) ⊔ (b \ a)`. This corresponds to the mathematical concept of the symmetric difference of two sets, which consists of elements in either of the sets but not in their intersection.
More concisely: For any type `α` with a supremum and set difference operations, the symmetric difference of two elements `a` and `b` equals the supremum of their set difference and the set difference of their reversed order: `symmDiff a b = (a \ b) ⊔ (b \ a)`.
|
bihimp_assoc
theorem bihimp_assoc :
∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b c : α), bihimp (bihimp a b) c = bihimp a (bihimp b c)
The theorem `bihimp_assoc` states that for all types `α` equipped with a Boolean algebra structure, and for all elements `a`, `b`, `c` of type `α`, the Heyting bi-implication operation `bihimp` is associative. That is, the result of first applying `bihimp` to `a` and `b`, and then applying `bihimp` to the result and `c`, is the same as the result of first applying `bihimp` to `b` and `c`, and then applying `bihimp` to `a` and the result. In mathematical terms, this can be written as $(a \leftrightarrow b) \leftrightarrow c = a \leftrightarrow (b \leftrightarrow c)$, where $\leftrightarrow$ denotes the Heyting bi-implication.
More concisely: For all types `α` with a Boolean algebra structure and all elements `a, b, c` of type `α`, the associativity of Heyting bi-implication holds: `(a bihimp b) bihimp c = a bihimp (b bihimp c)`.
|
symmDiff_assoc
theorem symmDiff_assoc :
∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α),
symmDiff (symmDiff a b) c = symmDiff a (symmDiff b c)
The theorem `symmDiff_assoc` states that for any type `α` which is equipped with the structure of a generalized boolean algebra, the symmetric difference operation `symmDiff` is associative. In other words, for any elements `a`, `b`, and `c` from this type, the symmetric difference of `a` and `b`, when taken the symmetric difference with `c`, is the same as taking the symmetric difference of `a` with the symmetric difference of `b` and `c`. This property can be written mathematically as: `symmDiff (symmDiff a b) c = symmDiff a (symmDiff b c)`.
More concisely: For any type equipped with a generalized boolean algebra structure, the symmetric difference operation is associative: `symmDiff (a symmetricDiff b) symmetricDiff c = a symmetricDiff (b symmetricDiff c)`.
|
symmDiff_right_involutive
theorem symmDiff_right_involutive :
∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a : α), Function.Involutive fun x => symmDiff a x
The theorem `symmDiff_right_involutive` states that for all types `α` that form a `GeneralizedBooleanAlgebra`, the symmetric difference operation with a fixed element `a` is an involutive function. In other words, applying the symmetric difference operation twice with the same element `a` results in the original value. In mathematical terms, this can be expressed as `symmDiff a (symmDiff a x) = x` for all `x` in `α`. The symmetric difference operation is defined as `(A \ B) ⊔ (B \ A)`, where `\` denotes set difference and `⊔` denotes the supremum operation.
More concisely: For any type `α` that forms a `GeneralizedBooleanAlgebra`, the symmetric difference operation with a fixed element `a` is involutive, that is, `symmDiff a (symmDiff a x) = x` for all `x` in `α`.
|
symmDiff_bot
theorem symmDiff_bot : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a : α), symmDiff a ⊥ = a
The theorem `symmDiff_bot` states that for all types `α` which form a Generalized Coheyting Algebra, and for any element `a` of type `α`, the symmetric difference of `a` and the bottom element (`⊥`) is just `a` itself. In terms of set theory, the symmetric difference (denoted by `symmDiff`) between a set `a` and the empty set (`⊥`) is just the set `a` itself.
More concisely: For any type `α` that forms a Generalized Coalgebra and any element `a` of type `α`, `symmDiff a ⊥ = a`.
|
symmDiff_sup_inf
theorem symmDiff_sup_inf :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff a b ⊔ a ⊓ b = a ⊔ b
The theorem `symmDiff_sup_inf` states that for every type `α` that forms a Generalized Coheyting Algebra, and for every pair of elements `a` and `b` from `α`, the sup (union or "or") of the symmetric difference of `a` and `b` and the inf (intersection or "and") of `a` and `b` is equal to the sup of `a` and `b`. In other words, it combines the concepts of symmetric difference ("elements in `a` or `b`, but not in both"), intersection ("elements in both `a` and `b`"), and union ("elements in `a` or `b` or in both") to show a certain identity relationship that holds in this algebraic structure.
More concisely: For every type `α` forming a Generalized Lattice and every pair of elements `a, b` in `α`, the sup of the symmetric difference `a ⊎ b` and the inf of `a` and `b` equals the sup of `a` and `b`.
|
symmDiff_sdiff
theorem symmDiff_sdiff :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), symmDiff a b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
The theorem `symmDiff_sdiff` states that for any type `α` which is a Generalized Coheyting Algebra, and any three elements `a`, `b`, and `c` of this type, the symmetric difference of `a` and `b`, minus `c`, is equal to the union of `a` minus the union of `b` and `c`, and `b` minus the union of `a` and `c`. In mathematical terms, this can be written as $(A \triangle B) \setminus C = (A \setminus (B \cup C)) \cup (B \setminus (A \cup C))$, where $A$, $B$, and $C$ are elements of some Generalized Coheyting Algebra, $\triangle$ denotes symmetric difference, $\setminus$ denotes set difference, and $\cup$ denotes union.
More concisely: For any Generalized Cohesion Algebra type `α` and elements `a`, `b`, and `c` of `α`, $(a \triangle b) \setminus c = (a \setminus (b \cup c)) \cup (b \setminus (a \cup c))$.
|
symmDiff_eq_bot
theorem symmDiff_eq_bot : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, symmDiff a b = ⊥ ↔ a = b
This theorem states that for any type `α` that is an instance of a generalized coheyting algebra, and for any elements `a` and `b` of this type, the symmetric difference of `a` and `b` is equal to the bottom element of the algebra (denoted by `⊥`) if and only if `a` is equal to `b`. In other words, in such an algebraic structure, the symmetric difference of two elements being the bottom element is an indicator of the equality of these two elements.
More concisely: For any type `α` instancing a generalized co Heyting algebra and any elements `a, b` of `α`, `a ⊎ b = ⊥` if and only if `a = b`.
|
hnot_symmDiff_self
theorem hnot_symmDiff_self : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), symmDiff (￢a) a = ⊤
The theorem `hnot_symmDiff_self` states that for any type `α` that is a co-heyting algebra, the symmetric difference of the negation (`￢a`) of an element `a` and `a` itself is always the top element (`⊤`). In other words, in a co-heyting algebra, the symmetric difference of an element and its negation always yields the maximal element.
More concisely: In a co-heyting algebra, the symmetric difference of an element and its negation equals the top element.
|
symmDiff_self
theorem symmDiff_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a : α), symmDiff a a = ⊥
The theorem `symmDiff_self` states that for any type `α` that forms a Generalized Coheyting Algebra, the symmetric difference of an element `a` with itself always equals the bottom element `⊥`. In other words, given any element from the algebra, the result of performing the symmetric difference operation on it and itself is the lowest or 'null' element in the algebra. This is akin to saying the symmetric difference of a set with itself is the empty set in set theory.
More concisely: For any type `α` that is a Generalized Coalgebra, `a ⊎ a = ⊥` for all `a : α`.
|
symmDiff_eq_sup_sdiff_inf
theorem symmDiff_eq_sup_sdiff_inf :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff a b = (a ⊔ b) \ (a ⊓ b)
This theorem states that for any type `α` equipped with a structure of a generalized coheyting algebra, and for any elements `a` and `b` of that type, the symmetric difference of `a` and `b` (defined as `(a \ b) ⊔ (b \ a)`) is equal to the union of `a` and `b` minus the intersection of `a` and `b` (expressed as `(a ⊔ b) \ (a ⊓ b)`). In other words, the symmetric difference operation can also be computed by taking the union of the two elements and then removing their intersection.
More concisely: For any type `α` with a generalized coalgebra structure and elements `a` and `b` in `α`, the symmetric difference `(a \ b) ⊔ (b \ a)` equals the set difference between the union of `a` and `b` and their intersection, `(a ⊔ b) \ (a ⊓ b)`.
|
bihimp_comm
theorem bihimp_comm : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp a b = bihimp b a := by
sorry
The theorem `bihimp_comm` states that for all types `α` that form a Generalized Heyting Algebra, the Heyting bi-implication operation, denoted as `bihimp`, is commutative. In other words, for any two elements `a` and `b` of the algebra, the bi-implication of `a` and `b` is equal to the bi-implication of `b` and `a`. In terms of logic, this means that the logical equivalence between `a` and `b` is the same as the logical equivalence between `b` and `a`.
More concisely: For any type `α` forming a Generalized Heyting Algebra, the Heyting bi-implication operation `bihimp` is commutative: `a bihimp b ≡ b bihimp a`.
|
symmDiff_comm
theorem symmDiff_comm :
∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff a b = symmDiff b a
This theorem states that for any type `α` that is a Generalized Coheyting Algebra, the symmetric difference operation is commutative. In other words, given any two elements `a` and `b` of this type, the symmetric difference of `a` and `b` is the same as the symmetric difference of `b` and `a`. The symmetric difference operation being referred to here is defined as the union of the difference of `a` and `b` and the difference of `b` and `a`.
More concisely: For any type `α` that is a Generalized Coalgebra, the symmetric difference of two elements `a` and `b` is commutative, i.e., `a \\ b = b \\ a`.
|