CompleteDistribLattice.iInf_sup_le_sup_sInf
theorem CompleteDistribLattice.iInf_sup_le_sup_sInf :
∀ {α : Type u_1} [self : CompleteDistribLattice α] (a : α) (s : Set α), ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
The theorem `CompleteDistribLattice.iInf_sup_le_sup_sInf` states that in a complete distributive lattice of any type `α`, the supremum (`⊔`) operator distributes over the infimum (`⨅`) operator. Specifically, for any element `a` of the lattice and any set `s` of elements of the lattice, the infimum of the supremum of `a` and each element in `s` is less than or equal to the supremum of `a` and the infimum of the set `s`.
More concisely: For any complete distributive lattice and any element `a` and set `s` of its elements, `⊔` (supremum) of `a` and `⨅` (infimum) of the set `s` is less than or equal to `⊔` of `a` and `⨅` of `s`.
|
Order.Frame.inf_sSup_le_iSup_inf
theorem Order.Frame.inf_sSup_le_iSup_inf :
∀ {α : Type u_1} [self : Order.Frame α] (a : α) (s : Set α), a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
This theorem states that in any frame structure, the meet operation (`⊓`) distributes over the supremum operation (`⨆`). More formally, given any element `a` and any set `s` in the frame structure `α`, the meet of `a` and the supremum of `s` is less than or equal to the supremum of the meet of `a` and each element `b` in `s`. Here, the supremum (`sSup`) is the least upper bound, and `⊓` is the meet operation, which represents the greatest lower bound of two elements.
More concisely: In any frame structure, for all elements `a` and set `s`, the meet of `a` and the supremum of `s` is less than or equal to the supremum of the meets of `a` and each element in `s`.
|
CompleteAtomicBooleanAlgebra.le_sup_inf
theorem CompleteAtomicBooleanAlgebra.le_sup_inf :
∀ {α : Type u} [self : CompleteAtomicBooleanAlgebra α] (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
This theorem, named `le_sup_inf`, states that in the context of a `CompleteAtomicBooleanAlgebra`, for any elements `x`, `y`, and `z` of any type `α`, the infimum ('join', denoted by ⊔) of `x` and `y`, intersected ('meet', denoted by ⊓) with the infimum of `x` and `z`, is less than or equal to the infimum of `x` and the intersection of `y` and `z`. In mathematical terms, it asserts that `(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z)`. This is a property relating the operations of supremum (infimum, or 'join') and infimum (meet) in a complete atomic Boolean algebra.
More concisely: In a complete atomic Boolean algebra, the infimum of the infimum of two elements and their join, is less than or equal to the infimum of their meet and the join of the elements. In other words, `(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z)` for all elements `x`, `y`, and `z`.
|
CompleteAtomicBooleanAlgebra.top_le_sup_compl
theorem CompleteAtomicBooleanAlgebra.top_le_sup_compl :
∀ {α : Type u} [self : CompleteAtomicBooleanAlgebra α] (x : α), ⊤ ≤ x ⊔ xᶜ
This theorem states that for any type `α` that has a structure of a Complete Atomic Boolean Algebra, the supremum (or join operation denoted by `⊔`) of any element `x` in `α` and its complement (`xᶜ`) is always greater than or equal to the top element (`⊤`). In simpler terms, in any Complete Atomic Boolean Algebra, the "combined value" of an element and its opposite is at least as big as the biggest possible value in that algebra.
More concisely: In a complete atomic boolean algebra, for all elements x, x ⊔ xᶜ ≥ ⊤.
|
CompleteAtomicBooleanAlgebra.inf_sSup_le_iSup_inf
theorem CompleteAtomicBooleanAlgebra.inf_sSup_le_iSup_inf :
∀ {α : Type u} [self : CompleteAtomicBooleanAlgebra α] (a : α) (s : Set α), a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
This theorem states that in a complete atomic Boolean algebra, the infimum (greatest lower bound, denoted by `⊓`) of an element `a` and the supremum (least upper bound, denoted by `sSup`) of a set `s` is less than or equal to the supremum (over all elements `b` in the set `s`) of the infimum of `a` and `b`. This is a distributive law in the context of complete atomic Boolean algebras.
More concisely: In a complete atomic Boolean algebra, the infimum of an element with the supremum of any set containing it is less than or equal to the supremum of the infimums of that element with each set element.
|
CompleteBooleanAlgebra.sInf_le
theorem CompleteBooleanAlgebra.sInf_le :
∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (s : Set α), ∀ a ∈ s, sInf s ≤ a
This theorem states that for any set `s` in a Complete Boolean Algebra of type `α`, every element `a` within `s` is greater than or equal to the infimum of `s`. In other words, the infimum (greatest lower bound) of `s` is less than or equal to every element in `s`. It is a property that holds in any Complete Boolean Algebra, a mathematical structure that includes operations of conjunction, disjunction, and complementation, as well as a least element, a greatest element, and arbitrary infima and suprema.
More concisely: For any element `a` in a Complete Boolean Algebra `α`, we have `inf(s) ≤ a` for every set `s ⊆ α` with `a ∈ s`.
|
iSup_inf_of_monotone
theorem iSup_inf_of_monotone :
∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} [inst_1 : Preorder ι]
[inst_2 : IsDirected ι fun x x_1 => x ≤ x_1] {f g : ι → α},
Monotone f → Monotone g → ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i
The theorem `iSup_inf_of_monotone` states that for any types `α` and `ι`, where `α` forms a frame order and `ι` a preorder. If `ι` is directed with respect to the partial order `≤`, and `f` and `g` are both monotone functions from `ι` to `α`, then the supremum of the infimum of `f(i)` and `g(i)` for all `i` in `ι` is equal to the infimum of the supremum of `f(i)` and the supremum of `g(i)`. In mathematical terms, this can be written as $\bigvee_i (f(i) \land g(i)) = (\bigvee_i f(i)) \land (\bigvee_i g(i))$, where $\bigvee$ denotes the supremum (or join), $\land$ denotes the infimum (or meet), and the index `i` ranges over all elements in `ι`.
More concisely: For any frame order types `α` and preorder `ι`, if `ι` is directed and `f` and `g` are monotone functions from `ι` to `α`, then $\bigvee\_i (f(i) \land g(i)) = (\bigvee\_i f(i)) \land (\bigvee\_i g(i))$.
|
Order.Coframe.iInf_sup_le_sup_sInf
theorem Order.Coframe.iInf_sup_le_sup_sInf :
∀ {α : Type u_1} [self : Order.Coframe α] (a : α) (s : Set α), ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
This theorem states that for any type `α` that is a coframe, and for any element `a` of `α` and any set `s` of elements of `α`, the infimum (or greatest lower bound) of the supremums (or least upper bounds) `a ⊔ b` over all `b` in `s` is less than or equal to the supremum of `a` and the infimum of `s`. In simpler terms, in a coframe, the supremum operation distributes over the infimum operation.
More concisely: For any coframe type `α`, the supremum of an element `a` in `α` and the infimum of the supremums of `a` over all elements `b` in any set `s` in `α` is less than or equal to the supremum of `a` and the infimum of `s`.
|
iSup_inf_iSup
theorem iSup_inf_iSup :
∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α},
(⨆ i, f i) ⊓ ⨆ j, g j = ⨆ i, f i.1 ⊓ g i.2
This theorem states that for any two types `ι` and `ι'`, and any two functions `f` and `g` from these types to a type `α` that is equipped with a frame structure (an algebraic structure that generalizes both lattices and Heyting algebras), the supremum of the images of `f` and `g` (expressed as `(⨆ i, f i) ⊓ ⨆ j, g j`) is equal to the supremum of the infimum of the paired elements from `f` and `g` (expressed as `⨆ i, f i.1 ⊓ g i.2`). In simpler terms, it expresses a distributive property of the supremum and infimum operations in the context of certain algebraic structures.
More concisely: For any types `ι`, `ι'`, and functions `f : ι -> α` and `g : ι' -> α` to a frame-structured type `α`, the supremum of `f` and `g` equals the supremum of the pairwise infima of `f(i)` and `g(j)`.
|
iSup_inf_eq
theorem iSup_inf_eq :
∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] (f : ι → α) (a : α), (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
This theorem states that for any type `α` equipped with an order frame structure, any function `f` from some indexing set `ι` to `α`, and any element `a` of `α`, the infimum (greatest lower bound) of `a` and the supremum (least upper bound) over all `i` of `f(i)` is equal to the supremum over all `i` of the infimum of `a` and `f(i)`. It essentially says that the infimum operation commutes with the supremum operation under certain conditions.
More concisely: For any type `α` with an order frame structure, given a function `f` from an indexing set `ι` to `α` and an element `a` of `α`, the infimum of `a` with respect to the order on `α` and the supremum of the infimum of `a` and `f(i)` over all `i` in `ι` are equal.
|
inf_iSup_eq
theorem inf_iSup_eq :
∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] (a : α) (f : ι → α), a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
This theorem states that for any given type `α` equipped with a frame structure (a type of order theoretic structure), a constant `a` of type `α`, and a function `f` from an arbitrary type `ι` to `α`, the infimum (greatest lower bound) of `a` and the supremum (least upper bound) over all `i` of `f i` is equal to the supremum over all `i` of the infimum of `a` and `f i`. In other words, it exchanges the order of the infimum and supremum operations. This property is often found in mathematical structures that involve order and lattice operations, and is known as the "inf-sup distributive law".
More concisely: For any frame-structured type `α`, any element `a` of `α`, and any function `f` from an arbitrary type to `α`, the infimum of `a` and the supremum of the infima of `a` and `f i` over all `i` are equal.
|
CompleteAtomicBooleanAlgebra.sdiff_eq
theorem CompleteAtomicBooleanAlgebra.sdiff_eq :
∀ {α : Type u} [self : CompleteAtomicBooleanAlgebra α] (x y : α), x \ y = x ⊓ yᶜ
This theorem, `CompleteAtomicBooleanAlgebra.sdiff_eq`, states that for any elements `x` and `y` of a complete atomic Boolean algebra of any type `α`, the set difference operation `x \ y` is equivalent to the operation `x ⊓ yᶜ`, where `⊓` is the infimum or greatest lower bound operation and `ᶜ` denotes the complement of `y`. In other words, removing `y` from `x` is the same as finding the greatest element in `x` that is not in `y`.
More concisely: For any elements x and y in a complete atomic Boolean algebra, x \ y = x ⊓ yᶜ, where ⊓ is the infimum and yᶜ is the complement.
|
compl_iInf
theorem compl_iInf :
∀ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ι → α}, (iInf f)ᶜ = ⨆ i, (f i)ᶜ
The theorem `compl_iInf` states that for any type `α` that forms a complete Boolean algebra and a function `f` from any sort `ι` to `α`, the complement of the indexed infimum of `f` is equal to the indexed supremum of the complement of `f`. In mathematical terms, this can be written as: for all `ι` and `α` such that `α` is a complete Boolean algebra, and any function `f: ι → α`, it holds that `(iInf f)ᶜ = ⨆ i, (f i)ᶜ`. This theorem captures the duality between the supremum and infimum operations in the context of a complete Boolean algebra.
More concisely: In a complete Boolean algebra, the complement of the indexed infimum of a function equals the indexed supremum of the complements.
|
sSup_inf_eq
theorem sSup_inf_eq : ∀ {α : Type u} [inst : Order.Frame α] {s : Set α} {b : α}, sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b
This theorem, named `sSup_inf_eq`, states that for any type `α` with a frame structure (which makes it a partially ordered set with certain additional properties related to suprema and infima), for any set `s` of elements of type `α`, and for any element `b` of type `α`, the infimum of the supremum of `s` and `b` is equal to the supremum of the set of all infima of elements `a` in `s` and `b`. In mathematical notation, this can be written as: `inf(sup(s), b) = sup({inf(a, b) | a ∈ s})`.
More concisely: For any frame-structured type `α` and set `s` of elements, the infimum of the supremum of `s` and an element `b` equals the supremum of the set of infima of each element in `s` and `b`. In mathematical notation: `inf(sup(s), b) = sup({inf(a, b) | a ∈ s})`.
|
CompleteBooleanAlgebra.iInf_sup_le_sup_sInf
theorem CompleteBooleanAlgebra.iInf_sup_le_sup_sInf :
∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (a : α) (s : Set α), ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
This theorem states that in a complete Boolean algebra, the supremum operation (denoted as `⊔`) distributes over the infimum operation (denoted as `⨅`). In other words, for any element `a` and any set `s` of the same type in the context of a complete Boolean algebra, the infimum of the supremum of `a` and every element in `s` is less than or equal to the supremum of `a` and the infimum of `s`.
More concisely: In a complete Boolean algebra, for any element `a` and set `s` of the same type, the infimum of `a` and the supremum of elements in `s` is less than or equal to the supremum of `a` and the infimum of `s`. In symbols: `⨅(a : B) (s : set B) ∥a ⊔ s∥ ≤ ⊔(a : B) (s : set B) ⨅ s`, where `B` is the type of the Boolean algebra.
|
sup_iInf_eq
theorem sup_iInf_eq :
∀ {α : Type u} {ι : Sort w} [inst : Order.Coframe α] (a : α) (f : ι → α), a ⊔ ⨅ i, f i = ⨅ i, a ⊔ f i
This theorem states that, for any type `α` equipped with a coframe order structure, any value `a` of type `α`, and any function `f` mapping from a type `ι` to `α`, the supremum (or least upper bound, denoted by `⊔`) of `a` and the infimum (or greatest lower bound, denoted by `⨅ i, f i`) of the values produced by `f` over all `i` in `ι` is equal to the infimum of the supremum of `a` and each value produced by `f`. In mathematical terms, the theorem is asserting that `a ⊔ (⨅ i, f i) = ⨅ i, (a ⊔ f i)`.
More concisely: For any type `α` with a coframe order structure, the supremum of an element `a` in `α` and the infimum of the supremums of `a` and `f(i)` over all `i` in an index type `ι` are equal: `a ⊔ (⨅ i, f i) = ⨅ i, (a ⊔ f i)`.
|
CompleteBooleanAlgebra.sSup_le
theorem CompleteBooleanAlgebra.sSup_le :
∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (s : Set α) (a : α), (∀ b ∈ s, b ≤ a) → sSup s ≤ a
This theorem, named `CompleteBooleanAlgebra.sSup_le`, states that for any type `α` that has a structure of a complete boolean algebra, given a set `s` of elements of type `α` and any element `a` of type `α`, if `a` is an upper bound of the set `s` (i.e., every element `b` in `s` is less than or equal to `a`), then the supremum (least upper bound) of the set `s` is less than or equal to `a`.
More concisely: For any complete boolean algebra type `α`, if `a` is an upper bound of a set `s` in `α`, then the supremum of `s` is less than or equal to `a`.
|
inf_sSup_eq
theorem inf_sSup_eq : ∀ {α : Type u} [inst : Order.Frame α] {s : Set α} {a : α}, a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
This theorem states that for any type `α` that forms a frame (a complete lattice in mathematics), any set `s` of elements of type `α`, and any element `a` of type `α`, the infimum (`⊓`) of `a` and the supremum (`sSup`) of `s` is equal to the supremum (`⨆`) of the infimum (`⊓`) of `a` and each element `b` in `s`. This is a property related to the distributivity of infimum over supremum in a frame.
More concisely: For any frame (complete lattice) `α`, any set `s ⊆ α`, and any `a ∈ α`, the inf inf a and sup s = sup {inf a, b | b ∈ s}.
|
iInf_iSup_eq
theorem iInf_iSup_eq :
∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompletelyDistribLattice α] {f : (a : ι) → κ a → α},
⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
This theorem states that for any type `α` that forms a complete distributive lattice, and for any function `f` that takes an element of type `ι` and an element of type dependent on `ι` to `α`, the infimum (greatest lower bound) over `ι` of the supremum (least upper bound) over `κ` of `f` is equal to the supremum over all functions `g` from `ι` to `κ` of the infimum over `ι` of `f`. In simpler terms, it's saying that you can swap the order of taking the infimum and supremum without changing the result. This is a form of "Fubini's theorem" for lattices.
More concisely: For any complete distributive lattice `α` and any function `f` from `ι × κ` to `α`, the order-theoretic integration of `f` over `κ` with respect to `ι` is equal to the order-theoretic sum of the order-theoretic integrals of `f` over `ι` for each `κ`.
|
disjoint_sSup_iff
theorem disjoint_sSup_iff :
∀ {α : Type u} [inst : Order.Frame α] {a : α} {s : Set α}, Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b
This theorem states that for any type `α` equipped with a frame order, an element `a` of this type, and a set `s` of elements of this type, `a` is disjoint with the supremum of `s` if and only if `a` is disjoint with every element `b` in `s`. Here, two elements of a lattice are considered disjoint if their infimum is the bottom element. The supremum of a set (`sSup s`) represents the least upper bound of the set `s` in the given order.
More concisely: For any lattice with frame order, an element is disjoint with the supreme of a set if and only if it is disjoint with every element in the set.
|
le_iInf_iSup
theorem le_iInf_iSup :
∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompleteLattice α] {f : (a : ι) → κ a → α},
⨆ g, ⨅ a, f a (g a) ≤ ⨅ a, ⨆ b, f a b
This theorem states that for any type `α` that forms a complete lattice, and for any function `f` from a pair of indices `(a, g(a))` to `α`, the supremum of the infimums of `f(a, g(a))` over all `g` is less than or equal to the infimum of the supremums of `f(a, b)` over all `b` for each `a`. Here, the infimum and supremum are the greatest lower bound and least upper bound in the complete lattice `α` respectively. This theorem is a formal statement of the generalized distributive law for complete lattices.
More concisely: For any complete lattice `α` and function `f` from a pair of indices to `α`, the supremum of the infima of `f(a, g(a))` over all `g` is less than or equal to the infimum of the supremas of `f(a, b)` over all `b`, for each `a`.
|
CompleteBooleanAlgebra.le_sInf
theorem CompleteBooleanAlgebra.le_sInf :
∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (s : Set α) (a : α), (∀ b ∈ s, a ≤ b) → a ≤ sInf s
This theorem states that for any complete Boolean algebra of type α, any element 'a' of this type which is a lower bound for a set 's' (i.e., 'a' is less than or equal to every element in 's') is also less than or equal to the infimum of the set 's'. Here, infimum of a set is the greatest element that is less than or equal to all elements in the set.
More concisely: For any complete Boolean algebra and any set of elements, the infimum of that set is less than or equal to every lower bound of the set.
|
CompleteBooleanAlgebra.le_sSup
theorem CompleteBooleanAlgebra.le_sSup :
∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (s : Set α), ∀ a ∈ s, a ≤ sSup s
The theorem `CompleteBooleanAlgebra.le_sSup` asserts that for any given set `s` within a `CompleteBooleanAlgebra` of type `α`, any element `a` belonging to this set `s` is less than or equal to the supremum of the set `s`. In mathematical terminology, we often represent this as `∀a∈s, a ≤ sup(s)` where `sup(s)` denotes the supremum of the set `s`.
More concisely: For any set `s` in a Complete Boolean Algebra and any element `a` in `s`, we have `a ≤ sup s`.
|
CompleteAtomicBooleanAlgebra.iInf_sup_le_sup_sInf
theorem CompleteAtomicBooleanAlgebra.iInf_sup_le_sup_sInf :
∀ {α : Type u} [self : CompleteAtomicBooleanAlgebra α] (a : α) (s : Set α), ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
This theorem states that in a complete atomic Boolean algebra, the supremum operation (`⊔`) distributes over the infimum operation (`⨅`). More specifically, for any type `α` (which forms a complete atomic Boolean algebra) and any element `a` of type `α` and any set `s` of elements of type `α`, the infimum of the set of supremum of `a` and `b` for all `b` in `s` is less than or equal to the supremum of `a` and the infimum of `s`. In mathematical notation, it's saying that `∀ a, s, (⨅ b ∈ s, a ⊔ b) ≤ (a ⊔ inf s)`.
More concisely: In a complete atomic Boolean algebra, the supremum of the infimum of supremums of an element with all other elements in a set is less than or equal to the infimum of the set followed by the supremum of that element.
|
CompleteAtomicBooleanAlgebra.inf_compl_le_bot
theorem CompleteAtomicBooleanAlgebra.inf_compl_le_bot :
∀ {α : Type u} [self : CompleteAtomicBooleanAlgebra α] (x : α), x ⊓ xᶜ ≤ ⊥
This theorem states that for any type `α` that has the structure of a 'Complete Atomic Boolean Algebra', the infimum (greatest lower bound) of any element `x` and its complement `xᶜ` is less than or equal to the bottom element `⊥`. Essentially, in such a Boolean algebra, when we take an element and its complement, their greatest common lower bound is always the smallest possible element of the algebra.
More concisely: In a complete atomic boolean algebra, for all elements x, the infimum of x and xᶜ is less than or equal to the bottom element ⊥.
|
CompleteAtomicBooleanAlgebra.himp_eq
theorem CompleteAtomicBooleanAlgebra.himp_eq :
∀ {α : Type u} [self : CompleteAtomicBooleanAlgebra α] (x y : α), x ⇨ y = y ⊔ xᶜ
This theorem states that for any Complete Atomic Boolean Algebra (a mathematical structure used in logic), the 'himp' operation (represented by `x ⇨ y`) on two elements `x` and `y` is equal to the supremum (greatest lower bound or 'join') of `y` and the complement of `x` (noted as `xᶜ`). This holds for all elements `x` and `y` of the algebra.
More concisely: For any Complete Atomic Boolean Algebra, x imp y equals the supremum of y and the complement of x.
|
compl_iSup
theorem compl_iSup :
∀ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ι → α}, (iSup f)ᶜ = ⨅ i, (f i)ᶜ
The theorem `compl_iSup` states that for any type `α` that forms a complete Boolean algebra, and a function `f` from an arbitrary type `ι` to `α`, the complement of the indexed supremum of `f` is equal to the infimum of the complements of the values of `f`. In other words, the theorem expresses the property that the negation of the supremum of a set equals to the infimum of the negations of the elements in that set, in the context of a complete Boolean algebra.
More concisely: In a complete Boolean algebra, the complement of the supremum of a function is equal to the infimum of the complements of its values.
|
disjoint_iSup_iff
theorem disjoint_iSup_iff :
∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] {a : α} {f : ι → α},
Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)
The theorem `disjoint_iSup_iff` states that for any type `α` with a frame order and a function `f` from some index type `ι` to `α`, an element `a` of `α` is disjoint with the supremum (⨆ i, f i) of `f` over all `i` if and only if `a` is disjoint with each element `f i` for every `i` in `ι`. Here, two elements of the lattice `α` are considered disjoint if their infimum is the bottom element.
More concisely: An element of a frame-ordered type `α` is disjoint with the supremum of a function from an index type to `α` if and only if it is disjoint with each image under the function.
|
CompleteBooleanAlgebra.inf_sSup_le_iSup_inf
theorem CompleteBooleanAlgebra.inf_sSup_le_iSup_inf :
∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (a : α) (s : Set α), a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
This theorem states that for any given complete Boolean algebra, the infimum (or greatest lower bound) of an element `a` and the supremum (or least upper bound) of a set `s` is less than or equal to the supremum of the infimum of `a` and each element `b` in the set `s`. In mathematical notation, it can be expressed as: `a ⊓ sup(s) ≤ sup{a ⊓ b | b ∈ s}`.
More concisely: The inf inf(a, s) <= sup {a and b | b in s}, where inf and sup represent the infimum and supremum, respectively, and a is an element and s is a set in a complete Boolean algebra.
|