eq_compl_iff_isCompl
theorem eq_compl_iff_isCompl : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x = yᶜ ↔ IsCompl x y
This theorem states that for any type `α` with a Boolean algebra structure, and any two elements `x` and `y` of type `α`, `x` equals the complement of `y` if and only if `x` and `y` are complements of each other. In mathematical terms, given a Boolean algebra (often represented in terms of set operations), two elements `x` and `y` are complements (i.e., their union is the whole set and their intersection is empty) if and only if `x` is equivalent to the set-theoretic complement of `y`.
More concisely: For any Boolean algebra type `α` and elements `x` and `y` of type `α`, `x` and `y` are complements if and only if `x` is the complement of `y` and vice versa.
|
BooleanAlgebra.himp_eq
theorem BooleanAlgebra.himp_eq : ∀ {α : Type u} [self : BooleanAlgebra α] (x y : α), x ⇨ y = y ⊔ xᶜ
The theorem `himp_eq` from the `BooleanAlgebra` class states that for any Boolean algebra, the implication operation `x ⇨ y` is equal to the supremum of `y` and the complement of `x` (`y ⊔ xᶜ`). It applies to every type `α` that forms a Boolean algebra, and for every pair of elements (`x`, `y`) from that type. This theorem represents one of the fundamental properties of Boolean algebras.
More concisely: In every Boolean algebra, the implication operation is equal to the supremum of one element with the complement of the other.
|
BooleanAlgebra.le_top
theorem BooleanAlgebra.le_top : ∀ {α : Type u} [self : BooleanAlgebra α] (a : α), a ≤ ⊤
This theorem states that for any Boolean algebra, let's denote it as `α`, and for any element `a` of this Boolean algebra, `a` is less than or equal to the top element, denoted by `⊤`. In other words, in any Boolean algebra, all elements are less than or equal to the greatest element (`⊤`).
More concisely: In any Boolean algebra, every element is less than or equal to the top element.
|
inf_inf_sdiff
theorem inf_inf_sdiff : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x y : α), x ⊓ y ⊓ x \ y = ⊥
The theorem `inf_inf_sdiff` states that for any type `α` that forms a Generalized Boolean Algebra, for any two elements of this type, say `x` and `y`, the greatest lower bound (infimum denoted by `⊓`) of `x` and `y` and the set difference of `x` and `y` (`x \ y`) is the bottom element (`⊥`). In simpler terms, it says that if you take the intersection of `x` and `y` and then remove all elements of `y` from `x`, you will end up with an empty set.
More concisely: For any type `α` that forms a Generalized Boolean Algebra, `x` and `y` being elements of `α`, `x ⊓ (x \ y) = ⊥`.
|
sup_compl_eq_top
theorem sup_compl_eq_top : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], x ⊔ xᶜ = ⊤
This theorem states that for any type `α` that has a Boolean algebra structure, the supremum (also known as the join or least upper bound) of any element `x` and its complement `xᶜ` is the top element `⊤`. In other words, in any Boolean algebra, the "or" operation (`⊔`) applied to an element and its negation always results in the truth value "true" or `⊤`.
More concisely: In any Boolean algebra, the supremum of an element and its complement is the top element.
|
compl_eq_bot
theorem compl_eq_bot : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], xᶜ = ⊥ ↔ x = ⊤
This theorem states that for any type `α` which forms a Boolean algebra, the complement (`xᶜ`) of an element `x` of type `α` is equal to the bottom element (`⊥`) if and only if `x` is the top element (`⊤`). In terms of set theory, this would mean that the complement of a set is the empty set if and only if the set is universal, i.e., contains all elements.
More concisely: For any Boolean algebra type `α`, the complement of an element `x` equals the bottom element `⊥` if and only if `x` is the top element `⊤`. Equivalently, in set theory, the complement of a set is the empty set if and only if the set is universal.
|
inf_sdiff_distrib_left
theorem inf_sdiff_distrib_left :
∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (a b c : α), a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
This theorem states that for any generalized Boolean algebra, the operation of finding the infimum (greatest lower bound) of `a` and `b` and then subtracting `c` is equivalent to finding the infimum of `a` and `b` first, and then subtracting the infimum of `a` and `c`. In essence, it's expressing a property of distributivity of the `sdiff` (set difference) and `inf` (infimum or greatest lower bound) operations over the elements of the algebra.
More concisely: In a generalized Boolean algebra, the operation of taking the infimum of two elements and then subtracting a third element is equivalent to first taking the infimum of the first two elements and then subtracting their infimum with the third element.
|
inf_sdiff_self_right
theorem inf_sdiff_self_right : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x ⊓ y \ x = ⊥
This theorem states that for any generalized boolean algebra (a mathematical structure that can behave like a set of subsets of a base set), the infimum (or greatest lower bound) of y and the symmetric difference of x and y is the bottom element of the algebra. In other words, the intersection of any element `y` with the set difference between `y` and `x` (i.e., elements in `y` but not in `x`) always results in the bottom element, which represents an empty set in this context. Thus, the theorem captures the intuitive notion that the intersection of a set with its complement relative to another set is always empty.
More concisely: For any generalized boolean algebra, the infimum of an element and the symmetric difference between that element and another element is the bottom element.
|
compl_involutive
theorem compl_involutive : ∀ {α : Type u} [inst : BooleanAlgebra α], Function.Involutive compl
The theorem `compl_involutive` asserts that for all types `α` equipped with a boolean algebra structure, the `compl` function (which represents the complement operation in the boolean algebra) is involutive. In other words, applying the `compl` function twice to any element of the boolean algebra results in the original element. In mathematical terms, this is saying that for all elements `x` in the boolean algebra, `compl(compl(x)) = x`.
More concisely: For all types equipped with a boolean algebra structure, the complement operation is involutive, i.e., `compl(compl(x)) = x` for all elements `x` in the boolean algebra.
|
compl_compl
theorem compl_compl : ∀ {α : Type u} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = x
This theorem states that for all types `α` that have a `BooleanAlgebra` structure, the double complement of an element `x` from `α` is equal to `x`. In mathematical terms, this corresponds to the widely applicable principle that the double negation of a proposition is the proposition itself.
More concisely: For all types `α` with a `BooleanAlgebra` structure, the double negation of an element `x` equals `x`.
|
sdiff_eq_self_iff_disjoint
theorem sdiff_eq_self_iff_disjoint :
∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y = x ↔ Disjoint y x
This theorem states that for any generalized Boolean algebra, denoted by `α`, and any two elements `x` and `y` of `α`, the statement "`x` set-minus `y` equals `x`" is equivalent to "`y` and `x` are disjoint". Here, two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element of the algebra. This notion of disjointness generalizes the concept of disjoint sets in set theory.
More concisely: For any generalized Boolean algebra `α`, elements `x` and `y` are disjoint if and only if `x \ y` equals the bottom element of `α`.
|
sdiff_unique
theorem sdiff_unique :
∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x ⊓ y ⊔ z = x → x ⊓ y ⊓ z = ⊥ → x \ y = z := by
sorry
This theorem, `sdiff_unique`, states that for any type `α` that forms a Generalized Boolean Algebra, given any elements `x`, `y`, and `z` of that type, if the join (or union) of the meet (or intersection) of `x` and `y` with `z` equals `x`, and the meet of `x`, `y`, and `z` equals the bottom element (representing the empty set), then the set difference of `x` and `y` equals `z`. In mathematical terms, this states that if $x \cap y \cup z = x$ and $x \cap y \cap z = \emptyset$, then $x - y = z$.
More concisely: If $x \cap y = \emptyset$ and $x \cup y \cup z = x$, then $x \setminus y = z$.
|
himp_eq
theorem himp_eq : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x ⇨ y = y ⊔ xᶜ
This theorem, `himp_eq`, states that for all types `α` (where `α` is an instance of a Boolean algebra), and for all elements `x` and `y` of type `α`, the operation of implication (denoted by `x ⇨ y`) is equal to the supremum (or join) of `y` and the complement of `x` (denoted by `xᶜ`). In mathematical terms, `x ⇒ y = y ∪ ¬x` for all elements `x` and `y` in any Boolean algebra.
More concisely: In any Boolean algebra, the operation of implication (x ⇨ y) is equal to the supremum (y ∪ xᶜ) for all elements x and y.
|
compl_eq_comm
theorem compl_eq_comm : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], xᶜ = y ↔ yᶜ = x
This theorem states that for any type `α` equipped with a Boolean algebra structure, and any two elements `x` and `y` of this type, the complement of `x` equals `y` if and only if the complement of `y` equals `x`. In mathematical terms, if `x` and `y` are elements of a Boolean algebra, then the complement of `x` (`xᶜ`) is equal to `y` if and only if the complement of `y` (`yᶜ`) is equal to `x`.
More concisely: For any Boolean algebra `α`, and elements `x, y` in `α`, `xᶜ = y` if and only if `yᶜ = x`.
|
compl_injective
theorem compl_injective : ∀ {α : Type u} [inst : BooleanAlgebra α], Function.Injective compl
The theorem `compl_injective` states that for all types `α` equipped with a Boolean algebra structure, the complement function `compl` is injective. In more mathematical terms, the complement function `compl`, defined on a Boolean algebra, is such that whenever `compl x = compl y` for any two elements `x` and `y` from the Boolean algebra, it implies that `x = y`. Thus, the complement function doesn't map different elements to the same value.
More concisely: For all Boolean algebras α, the complement function is injective, that is, complements of distinct elements are distinct.
|
BooleanAlgebra.sdiff_eq
theorem BooleanAlgebra.sdiff_eq : ∀ {α : Type u} [self : BooleanAlgebra α] (x y : α), x \ y = x ⊓ yᶜ
For any types `α` with a `BooleanAlgebra` structure and any elements `x` and `y` of the type `α`, the set difference `x \ y` (the set of elements in `x` but not in `y`) is equivalent to the intersection of `x` with the complement of `y` (`x ⊓ yᶜ`). In other words, removing elements of `y` from `x` is the same as finding elements that are in `x` and not in `y`.
More concisely: For any Boolean algebra `α` and elements `x, y` in `α`, `x \ y` equals `x ∩ yᶜ`.
|
isCompl_compl
theorem isCompl_compl : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], IsCompl x xᶜ
This theorem states that for all elements `x` of a type `α` in a Boolean algebra, `x` is complementary to its own complement `xᶜ`. In terms of set theory, this theorem proves that every element and its complement form a complementary pair, meaning the union of the two gives the universal set and their intersection is empty.
More concisely: In a Boolean algebra, for all elements `x`, `x` is complementary to `xᶜ`, meaning `x ∨ xᶜ = ⊤` and `x ∧ xᶜ = ⊥`.
|
sdiff_sdiff_eq_self
theorem sdiff_sdiff_eq_self : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], y ≤ x → x \ (x \ y) = y
This theorem states that for any type `α` that forms a Generalized Boolean Algebra, and for any elements `x` and `y` of that type; if `y` is less than or equal to `x`, then the symmetric difference of `x` and the symmetric difference of `x` and `y` equals `y`. In mathematical terms, this theorem can be expressed as: if `y ≤ x`, then `x \ (x \ y) = y`. The backslash (`\`) operation represents the symmetric difference in this context.
More concisely: For any type `α` forming a Generalized Boolean Algebra and elements `x` and `y` of `α` with `y ≤ x`, we have `x \ (x \ y) = y`.
|
Mathlib.Order.BooleanAlgebra._auxLemma.1
theorem Mathlib.Order.BooleanAlgebra._auxLemma.1 :
∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], (x \ y = x) = Disjoint x y
This theorem states that for any type `α` that is a generalized Boolean algebra, and for any elements `x` and `y` of `α`, the condition that `x \ y` equals `x` is equivalent to `x` and `y` being disjoint. In the context of a generalized Boolean algebra, two elements `x` and `y` are considered disjoint if for all `x` such that `x` is less than or equal to `a` and `x` is less than or equal to `b`, `x` is also less than or equal to the bottom element `⊥`. This is a generalization of the concept of disjoint sets, where the intersection of the sets is empty.
More concisely: In a generalized Boolean algebra, two elements are disjoint if and only if their difference equals one of them.
|
GeneralizedBooleanAlgebra.inf_inf_sdiff
theorem GeneralizedBooleanAlgebra.inf_inf_sdiff :
∀ {α : Type u} [self : GeneralizedBooleanAlgebra α] (a b : α), a ⊓ b ⊓ a \ b = ⊥
This theorem states that for any elements `a` and `b` in a Generalized Boolean Algebra, the infimum (greatest lower bound or 'and' operation) of `a` and `b`, further infimum with the set difference of `a` and `b` (equivalent to `a` and not `b`), is equal to the bottom element (the least element of the algebra, typically representing false). In other words, in the context of this algebra, `(a and b) and (a and not b)` always equates to false.
More concisely: In a Generalized Boolean Algebra, the infimum of `a` and `b` and the infimum of `a` and `a` XOR `b` (set difference) equals the bottom element.
|
sdiff_sdiff_right'
theorem sdiff_sdiff_right' :
∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x \ (y \ z) = x \ y ⊔ x ⊓ z
This theorem, `sdiff_sdiff_right'`, states that for any type `α` which forms a GeneralizedBooleanAlgebra and for any elements `x`, `y`, and `z` of that type, the set difference of `x` and the set difference of `y` and `z` is equal to the join of the set difference of `x` and `y` with the meet of `x` and `z`. In mathematical notation, this is written as $x \setminus (y \setminus z) = (x \setminus y) \sqcup (x \cap z)$. The theorem is universally quantified over `x`, `y`, and `z`, meaning it holds for all possible values of these variables.
More concisely: For any type `α` forming a GeneralizedBooleanAlgebra and any elements `x`, `y`, and `z` of that type, $x \setminus (y \setminus z) = (x \setminus y) \sqcup (x \cap z)$.
|
disjoint_sdiff_self_left
theorem disjoint_sdiff_self_left : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], Disjoint (y \ x) x
This theorem, `disjoint_sdiff_self_left`, states that for all types `α` and for all elements `x` and `y` of type `α` in a generalized boolean algebra, the 'difference' of `y` and `x` (denoted as `y \ x`) and `x` itself are disjoint. In the context of lattice theory, two elements are considered disjoint if their greatest lower bound (or infimum) is the bottom element of the lattice. In other words, for every other element `z` in the lattice, if `z` is less than or equal to both `y \ x` and `x`, then `z` must be less than or equal to the bottom element. This is a way of expressing the notion that `y \ x` and `x` have no elements in common (hence, they are 'disjoint').
More concisely: In a generalized boolean algebra, for all types `α` and elements `x` and `y` of type `α`, the sets `{z | z ≤ x ∧ z ≤ y \ x}` and `{x}` have no common elements.
|
sup_inf_sdiff
theorem sup_inf_sdiff : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x y : α), x ⊓ y ⊔ x \ y = x
This theorem states that for any type `α` that is a Generalized Boolean Algebra, given any two elements `x` and `y` of this type, the supremum (join, denoted as `⊔`) of the infimum (meet, denoted as `⊓`) of `x` and `y` and the set difference (`\`) of `x` and `y`, is equal to `x`. In plain English, it means the union of the intersection and the difference of two elements in a Generalized Boolean Algebra is equal to the first of these elements.
More concisely: In a Generalized Boolean Algebra, the supremum of the infimum of two elements and their set difference is equal to the first element. Or, more succinctly: `⊔(x ⊓ y, x \ y) = x` for all `α` and `x, y : α`.
|
compl_eq_top
theorem compl_eq_top : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], xᶜ = ⊤ ↔ x = ⊥
This theorem states that for all types `α` (where `α` is a Boolean algebra), the complement (`xᶜ`) of a given element `x` from `α` is equal to the top element (`⊤`) if and only if `x` is the bottom element (`⊥`). In other words, in any Boolean algebra, an element and its complement occupy opposite extremes of the algebra; if an element is the least element (`⊥`), its complement is the greatest element (`⊤`), and vice versa.
More concisely: In a Boolean algebra, the complement of an element is equal to the top element if and only if that element is the bottom element.
|
sdiff_sup
theorem sdiff_sup : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], y \ (x ⊔ z) = y \ x ⊓ y \ z := by
sorry
This theorem, `sdiff_sup`, states that for any type `α` that is a Generalized Boolean Algebra and any elements `x`, `y`, and `z` of that type, the set difference of `y` and the supremum of `x` and `z` (written as `y \ (x ⊔ z)`) is equivalent to the infimum of the set difference of `y` and `x` and the set difference of `y` and `z` (written as `y \ x ⊓ y \ z`). Essentially, this theorem describes a property of set differences and supremum/infimum operations in the context of a Generalized Boolean Algebra.
More concisely: For any element `y` of a Generalized Boolean Algebra and elements `x` and `z` of that type, `y \ (x ⊔ z)` is equivalent to `(y \ x) ⊓ (y \ z)`.
|
sdiff_sdiff_right
theorem sdiff_sdiff_right :
∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z
This theorem, `sdiff_sdiff_right`, states that for any type `α` that forms a Generalized Boolean Algebra, and any elements `x`, `y`, `z` of this type, the set difference of `x` and the set difference of `y` and `z` equals the join of the set difference of `x` and `y` with the meet of `x`, `y`, and `z`. In mathematical notation, this can be written as: \(x \ (y \ z) = x \ y \cup (x \cap y \cap z)\).
More concisely: For any type `α` forming a Generalized Boolean Algebra and elements `x`, `y`, `z` of `α`, `x ∖ (y ∖ z) = (x ∖ y) ⋃ (x ∩ y ∩ z)`.
|
compl_inf
theorem compl_inf : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], (x ⊓ y)ᶜ = xᶜ ⊔ yᶜ
This theorem states that for any type `α` equipped with a Boolean algebra structure, and for any two elements `x` and `y` of `α`, the complement of the infimum (or greatest lower bound) of `x` and `y` is equal to the supremum (or least upper bound) of the complements of `x` and `y`. In other words, it's saying that the De Morgan's Law holds in this Boolean algebra: not (x and y) is the same as (not x) or (not y).
More concisely: For any Boolean algebra `α`, the complement of the infimum of elements `x` and `y` equals the supremum of the complements of `x` and `y`. Equivalently, `not (x && y) <-> not x || not y`.
|
inf_sdiff_self_left
theorem inf_sdiff_self_left : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], y \ x ⊓ x = ⊥
This theorem states that for any type `α` which forms a Generalized Boolean Algebra, and any elements `x` and `y` of this type, the infimum (greatest lower bound) of the difference of `y` and `x` and `x` itself is the bottom element of the algebra. In simpler terms, it's saying if you take `x` away from `y` and then take the intersection with `x`, you end up with the least possible value in the whole set.
More concisely: For any type `α` forming a Generalized Boolean Algebra and any `x, y` in `α`, the infimum of `y - x` and `x` is the lattice bottom element.
|
compl_le_compl_iff_le
theorem compl_le_compl_iff_le : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], yᶜ ≤ xᶜ ↔ x ≤ y
This theorem, `compl_le_compl_iff_le`, states that for any given Boolean algebra, the complement of `y` (denoted as `yᶜ`) is lesser than or equal to the complement of `x` (denoted as `xᶜ`) if and only if `x` is lesser than or equal to `y`. In other words, it establishes an order-reversing correspondence between elements and their complements in a Boolean algebra.
More concisely: In a Boolean algebra, x≤y if and only if x′≤y′, where x and y are elements and x′ (respectively y′) denotes the complement of x (respectively y.
|
le_sdiff
theorem le_sdiff : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z
This theorem states that for any type `α` that is an instance of a `GeneralizedBooleanAlgebra`, and for any elements `x`, `y`, and `z` of this type, `x` is less than or equal to the difference of `y` and `z` if and only if `x` is less than or equal to `y` and `x` is disjoint with `z`. Here, `Disjoint x z` means that for any element that is less than or equal to both `x` and `z`, that element must also be less than or equal to the bottom element of the lattice. In essence, the theorem connects the partial order relation and the disjointness in the context of a generalized Boolean algebra.
More concisely: In a generalized Boolean algebra, for all elements x, y, and z, x <= y ^-.\^ z if and only if x <= y and x is disjoint with z. (Here, "^-.\^" denotes the lattice operation for difference in a generalized Boolean algebra.)
|
compl_surjective
theorem compl_surjective : ∀ {α : Type u} [inst : BooleanAlgebra α], Function.Surjective compl
The theorem `compl_surjective` states that for all types `α` that have a `BooleanAlgebra` instance, the complement function `compl` is surjective. In other words, for every element in the Boolean algebra, there exists another element such that when the complement operation is applied to the latter, we get the former. This is a property of the Boolean algebra structure, where the complement of any element always exists.
More concisely: For every element in a Boolean algebra with a given instance, there exists an element whose complement is that element.
|
compl_inj_iff
theorem compl_inj_iff : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], xᶜ = yᶜ ↔ x = y
This theorem states that for any type `α` that is a Boolean algebra, and any two elements `x` and `y` of that type, the complement of `x` is equal to the complement of `y` if and only if `x` is equal to `y`. In other words, the operation of taking the complement is injective in any Boolean algebra.
More concisely: In a Boolean algebra, the complement operation is injective, that is, for all elements x and y, x = y implies ·x = ·y, where · denotes the complement operation.
|
sdiff_compl
theorem sdiff_compl : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x \ yᶜ = x ⊓ y
This theorem states that for any type `α` that forms a Boolean algebra, and for any elements `x` and `y` of type `α`, the set difference of `x` and the complement of `y` (`x \ yᶜ`) is equal to the intersection of `x` and `y` (`x ⊓ y`). This is a property of Boolean algebra structures, which include sets and certain types of logic systems.
More concisely: In a Boolean algebra, for all elements x and y, x intersect y is equal to x minus the complement of y.
|
disjoint_sdiff_self_right
theorem disjoint_sdiff_self_right : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], Disjoint x (y \ x)
The theorem `disjoint_sdiff_self_right` states that for any type `α` that forms a Generalized Boolean Algebra, and any elements `x` and `y` of `α`, the element `x` and the difference of `y` and `x` (`y \ x`) are disjoint. In the context of this lattice-based structure, two elements being disjoint means that any element that is less than or equal to both of them is also less than or equal to the bottom element of the lattice.
More concisely: For any type `α` forming a Generalized Boolean Algebra and elements `x, y` in `α`, `x` and `y \ x` are disjoint, i.e., there is no element less than or equal to both `x` and `y \ x`.
|
BooleanAlgebra.inf_compl_le_bot
theorem BooleanAlgebra.inf_compl_le_bot : ∀ {α : Type u} [self : BooleanAlgebra α] (x : α), x ⊓ xᶜ ≤ ⊥
This theorem states that in a boolean algebra, for any element `x`, the infimum (greatest lower bound) of `x` and the complement of `x` is less than or equal to the bottom element (`⊥`). This essentially means that the intersection of an element and its complement in a boolean algebra is always the bottom element, or "empty".
More concisely: In a boolean algebra, for all elements x,the infimum of x and the complement of x is less than or equal to the bottom element.
|
sdiff_lt
theorem sdiff_lt : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], y ≤ x → y ≠ ⊥ → x \ y < x
This theorem states that for any type `α` that is a Generalized Boolean Algebra, given any two elements `x` and `y` of `α` such that `y` is less than or equal to `x` and `y` is not the bottom element, the operation `x \ y` (set difference of `x` and `y`) results in a value strictly less than `x`. Essentially, subtracting a non-zero and non-maximum element from another element reduces the value.
More concisely: For any Generalized Boolean Algebra `α` and elements `x` and `y` in `α` with `y` being less than or equal to `x` and not the bottom element, `x \ y` (the set difference of `x` and `y`) is strictly less than `x`.
|
BooleanAlgebra.top_le_sup_compl
theorem BooleanAlgebra.top_le_sup_compl : ∀ {α : Type u} [self : BooleanAlgebra α] (x : α), ⊤ ≤ x ⊔ xᶜ
This theorem states that in a Boolean algebra, for any element `x`, the supremum (least upper bound) of `x` and its complement `xᶜ` is always greater than or equal to the top element `⊤`. In other words, combining an element with its complement through the operation of supremum always results in an element that is at least as great as the greatest element in the Boolean algebra.
More concisely: In a Boolean algebra, for any element `x`, the supremum of `x` and its complement `xᶜ` is greater than or equal to the top element `⊤`.
|
BooleanAlgebra.bot_le
theorem BooleanAlgebra.bot_le : ∀ {α : Type u} [self : BooleanAlgebra α] (a : α), ⊥ ≤ a
This theorem states that in any Boolean algebra, the bottom element (denoted as `⊥`) is less than or equal to any element `a`. In other words, the bottom element is the least element in the set of all elements of the Boolean algebra. This is a fundamental property of Boolean algebras.
More concisely: In any Boolean algebra, the bottom element is lesser or equal to every element.
|
sdiff_sdiff_right_self
theorem sdiff_sdiff_right_self : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ (x \ y) = x ⊓ y
This theorem states that for all types `α` and for all elements `x` and `y` of type `α`, where `α` is a Generalized Boolean Algebra, the set difference of `x` and the set difference of `x` and `y` is equal to the intersection of `x` and `y`. In mathematical terms, it asserts that \(x \setminus (x \setminus y) = x \cap y\) for all `x` and `y` in a Generalized Boolean Algebra.
More concisely: For all types `α` representing a Generalized Boolean Algebra and all elements `x` and `y` in `α`, we have `x \ (x \ y) = x ∩ y`.
|
inf_sdiff_assoc
theorem inf_sdiff_assoc : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], (x ⊓ y) \ z = x ⊓ y \ z := by
sorry
This theorem, `inf_sdiff_assoc`, states that for any type `α` that is a Generalized Boolean Algebra, and any three elements `x`, `y`, `z` of this type, the "set difference" operation (`\`) behaves the same way whether it is applied to the intersection (`⊓`) of `x` and `y` first and then `z`, or to `x` and the set difference of `y` and `z`. In other words, it asserts that the set difference operation is associative with respect to the intersection operation.
More concisely: For any type `α` being a Generalized Boolean Algebra and elements `x`, `y`, `z` of it, `(x ⊓ y) \ z` equals `x \ (y \ z)`.
|
sdiff_eq
theorem sdiff_eq : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x \ y = x ⊓ yᶜ
This theorem, `sdiff_eq`, states that for any type `α` that has a Boolean algebra structure and for any two instances `x` and `y` of this type, the set difference of `x` and `y` (denoted as `x \ y`) is equal to the result of the 'AND' operation (denoted as `⊓`) between `x` and the complement of `y` (denoted as `yᶜ`).
More concisely: For any type `α` with a Boolean algebra structure, `x ⊓ yᶜ = x \ y`.
|
GeneralizedBooleanAlgebra.sup_inf_sdiff
theorem GeneralizedBooleanAlgebra.sup_inf_sdiff :
∀ {α : Type u} [self : GeneralizedBooleanAlgebra α] (a b : α), a ⊓ b ⊔ a \ b = a
This theorem states that for any type `α` that forms a `GeneralizedBooleanAlgebra`, and for any two elements `a` and `b` of this type, the supremum (or join) of the infimum (or meet) of `a` and `b` and the set difference of `a` and `b` equals `a`. In other words, in the context of a generalized Boolean algebra, combining `a` and `b` with both intersection and difference operations, and then taking the union of the results, will return `a`.
More concisely: In a generalized Boolean algebra, the supremum of the infimum of two elements and their set difference equals the first element.
|
Mathlib.Order.BooleanAlgebra._auxLemma.6
theorem Mathlib.Order.BooleanAlgebra._auxLemma.6 :
∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], (xᶜ = yᶜ) = (x = y)
This theorem states that for any type `α` with a defined Boolean algebra structure, and any two elements `x` and `y` of that type, the claim that the Boolean complement of `x` is equal to the Boolean complement of `y` is equivalent to the claim that `x` is equal to `y`. In other words, two elements in this context are identical if and only if their complements are identical.
More concisely: For any type `α` with a defined Boolean algebra structure, two elements `x` and `y` are equal if and only if their complements are equal.
|