IsLowerModularLattice.inf_covBy_of_covBy_sup
theorem IsLowerModularLattice.inf_covBy_of_covBy_sup :
∀ {α : Type u_2} [inst : Lattice α] [self : IsLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → a ⊓ b ⋖ b
This theorem states that for any type `α` that is a lattice and an instance of a lower modular lattice, and for any elements `a` and `b` of type `α`, if `a` covers the supremum of `a` and `b` (expressed as `a ⋖ a ⊔ b`), then the infimum of `a` and `b` must cover `b` (expressed as `a ⊓ b ⋖ b`). In other words, in a lower modular lattice, if `a` covers the least upper bound of `a` and `b`, then the greatest lower bound of `a` and `b` covers `b`.
More concisely: In a lower modular lattice, if element `a` covers the supremum of `a` and `b`, then the infimum of `a` and `b` covers `b`. Or equivalently, if `a ⋖ a ⊔ b` holds, then `a ⊓ b ⋖ b` holds.
|
CovBy.inf_of_sup_of_sup_left
theorem CovBy.inf_of_sup_of_sup_left :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsWeakLowerModularLattice α] {a b : α},
a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a
This theorem, `CovBy.inf_of_sup_of_sup_left`, is an alias of `inf_covBy_of_covBy_sup_of_covBy_sup_left` and it states that for any type `α` which is a lattice and a weak lower modular lattice, and for any elements `a` and `b` of type `α`, if `a` is covered by the join (sup) of `a` and `b` and `b` is also covered by the join of `a` and `b`, then the meet (inf) of `a` and `b` is covered by `a`. In terms of lattice theory, this theorem describes a condition under which an element is covered by another in the context of a weak lower modular lattice.
More concisely: If `α` is a lattice and a weak lower modular lattice, and `a` and `b` are elements of `α` with `a ≤ a ∨ b` and `b ≤ a ∨ b`, then `inf a b ≤ a`.
|
CovBy.sup_of_inf_of_inf_right
theorem CovBy.sup_of_inf_of_inf_right :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsWeakUpperModularLattice α] {a b : α},
a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b
This theorem, "CovBy.sup_of_inf_of_inf_right", states that for any lattice structure (specified by type `α`) that is also a weak upper modular lattice, given any two elements `a` and `b` of this lattice, if `a` infimum `b` is strictly covered by `a` and `a` infimum `b` is strictly covered by `b` then `b` is strictly covered by `a` supremum `b`. In other words, in such a lattice, if `a` and `b` both strictly cover their infimum, then `b` is strictly covered by the supremum of `a` and `b`.
More concisely: If `α` is a weak upper modular lattice and `a` and `b` are its elements with `a` strictly covering their infimum, then `b` is strictly covered by their supremum.
|
CovBy.inf_of_sup_of_sup_right
theorem CovBy.inf_of_sup_of_sup_right :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsWeakLowerModularLattice α] {a b : α},
a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b
This theorem, `CovBy.inf_of_sup_of_sup_right`, establishes a property in a weak lower modular lattice. In this context, it states for all elements `a` and `b` of a given type `α` that forms a weak lower modular lattice, if `a` is covered by the supremum of `a` and `b`, and `b` is also covered by the same supremum, then the infimum of `a` and `b` covers `b`. In more mathematical terms, if \(a \preceq a \vee b\) and \(b \preceq a \vee b\), then \(a \wedge b \preceq b\).
More concisely: If elements `a` and `b` in a weak lower modular lattice satisfy `a �vreq a ∨ b` and `b �vreq a ∨ b`, then `a ∧ b �vreq b`.
|
wellFounded_lt_exact_sequence
theorem wellFounded_lt_exact_sequence :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] {β : Type u_2} {γ : Type u_3}
[inst_2 : PartialOrder β] [inst_3 : Preorder γ],
(WellFounded fun x x_1 => x < x_1) →
(WellFounded fun x x_1 => x < x_1) →
∀ (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ),
GaloisCoinsertion f₁ f₂ →
GaloisInsertion g₂ g₁ →
(∀ (a : α), f₁ (f₂ a) = a ⊓ K) → (∀ (a : α), g₁ (g₂ a) = a ⊔ K) → WellFounded fun x x_1 => x < x_1
This theorem is a generalization of the concept that if `N` is a submodule of `M` and both `N` and the quotient `M / N` are Artinian, then `M` is also Artinian. More specifically, the theorem states that for any types `α`, `β`, and `γ` with their respective lattice, partial order, and preorder structures, and given certain functions `f₁`, `f₂`, `g₁`, `g₂` between these types and a specific `K` of type `α`, if two certain well-founded relations are satisfied, and if `f₁` and `f₂` form a Galois coinsertion and `g₁` and `g₂` form a Galois insertion such that for any `a` in `α`, `f₁(f₂(a))` equals the meet of `a` and `K`, and `g₁(g₂(a))` equals the join of `a` and `K`, then the third well-founded relation is also satisfied.
More concisely: If `α`, `β`, `γ` are types with lattice, partial order, and preorder structures, `f₁`, `f₂`, `g₁`, `g₂` are functions between them, `K` is in `α`, `f₁` and `f₂` form a Galois coinsertion, `g₁` and `g₂` form a Galois insertion, and for all `a` in `α`, `f₁(f₂(a))` is the meet of `a` and `K` and `g₁(g₂(a))` is the join of `a` and `K`, then the relation defined by `x ≤ y` if and only if `g₁(x) ≤ g₁(y)` is well-founded.
|
wellFounded_gt_exact_sequence
theorem wellFounded_gt_exact_sequence :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] {β : Type u_2} {γ : Type u_3}
[inst_2 : Preorder β] [inst_3 : PartialOrder γ],
(WellFounded fun x x_1 => x > x_1) →
(WellFounded fun x x_1 => x > x_1) →
∀ (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ),
GaloisCoinsertion f₁ f₂ →
GaloisInsertion g₂ g₁ →
(∀ (a : α), f₁ (f₂ a) = a ⊓ K) → (∀ (a : α), g₁ (g₂ a) = a ⊔ K) → WellFounded fun x x_1 => x > x_1
The theorem `wellFounded_gt_exact_sequence` is a generalization of the theorem that if `N` is a submodule of `M` and both `N` and `M / N` are Noetherian, then `M` is Noetherian. For any types `α`, `β`, and `γ` with `α` being a modular lattice, `β` being preordered, and `γ` being partially ordered, if the greater-than relations in `β` and `γ` are well-founded, then for any element `K` in `α`, any pair of functions `f₁ : β → α` and `f₂ : α → β` forming a Galois coinsertion, and any pair of functions `g₁ : γ → α` and `g₂ : α → γ` forming a Galois insertion, with the conditions that for all `a` in `α`, `f₁ (f₂ a)` equals the infimum of `a` and `K`, and `g₁ (g₂ a)` equals the supremum of `a` and `K`, the greater-than relation in `α` is well-founded.
More concisely: Given a modular lattice `α`, a preordered type `β` and a partially ordered type `γ` with well-founded greater-than relations, if `f₁ : β → α` and `f₂ : α → β` form a Galois coinsertion and `g₁ : γ → α` and `g₂ : α → γ` form a Galois insertion such that `f₁ (f₂ a)` is the infimum of `a` and a fixed element `K` in `α`, and `g₁ (g₂ a)` is the supremum of `a` and `K`, then the greater-than relation in `α` is well-founded.
|
IsUpperModularLattice.covBy_sup_of_inf_covBy
theorem IsUpperModularLattice.covBy_sup_of_inf_covBy :
∀ {α : Type u_2} [inst : Lattice α] [self : IsUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → b ⋖ a ⊔ b
This theorem states that in an upper modular lattice of type α, for any two elements a and b, if the meet (infimum) of a and b is covered by a, then b is covered by the join (supremum) of a and b. Here, 'covered by' means that the latter element is either equal to or directly above the former element in the lattice.
More concisely: In an upper modular lattice, if a meets b and a covers their meet, then b is covered by the join of a and b.
|
CovBy.sup_of_inf_left
theorem CovBy.sup_of_inf_left :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → b ⋖ a ⊔ b
This theorem, `CovBy.sup_of_inf_left`, states that for any lattice that is upper modular, given two elements `a` and `b`, if the infimum (greatest lower bound) of `a` and `b` is strictly less than `a`, then `b` is strictly less than the supremum (least upper bound) of `a` and `b`. This theorem is an alias of `covBy_sup_of_inf_covBy_left`.
More concisely: In an upper modular lattice, if the infimum of elements `a` and `b` is strictly less than `a`, then `b` is strictly below the supremum of `a` and `b`.
|
inf_covBy_of_covBy_sup_of_covBy_sup_left
theorem inf_covBy_of_covBy_sup_of_covBy_sup_left :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsWeakLowerModularLattice α] {a b : α},
a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a
This theorem states that for any type `α` that forms a weak lower modular lattice, given any two elements `a` and `b` of this type, if `a` is covered by the join (supremum) of `a` and `b`, and `b` is also covered by the join of `a` and `b`, then the meet (infimum) of `a` and `b` is covered by `a`. In simpler terms, in certain types of orders (like a weak lower modular lattice), if both `a` and `b` are immediately below their join `a ⊔ b`, then their meet `a ⊓ b` is immediately below `a`.
More concisely: In a weak lower modular lattice, if elements `a` and `b` are each covered by their join `a ⊔ b`, then the meet `a ⊓ b` is covered by `a`.
|
CovBy.inf_of_sup_right
theorem CovBy.inf_of_sup_right :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsLowerModularLattice α] {a b : α}, b ⋖ a ⊔ b → a ⊓ b ⋖ a
This theorem, named `CovBy.inf_of_sup_right`, is an alias of `inf_covBy_of_covBy_sup_right`. It states that for any given types `α` which forms a Lattice and a Lower Modular Lattice, and any two elements `a` and `b` of type `α`, if `b` covers `a` joined with `b` (expressed as `b ⋖ a ⊔ b`), then `a` and `b`'s meet (expressed as `a ⊓ b`) covers `a`. In other words, if `b` is immediately above the supremum (least upper bound) of `a` and `b`, then the infimum (greatest lower bound) of `a` and `b` is immediately below `a`.
More concisely: If `b` covers the join of `a` and `b` in a Lower Modular Lattice of a Lattice type `α`, then the meet of `a` and `b` covers `a`.
|
IsWeakLowerModularLattice.inf_covBy_of_covBy_covBy_sup
theorem IsWeakLowerModularLattice.inf_covBy_of_covBy_covBy_sup :
∀ {α : Type u_2} [inst : Lattice α] [self : IsWeakLowerModularLattice α] {a b : α},
a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a
In the setting of a weak lower modular lattice (of any type `α`), the theorem `inf_covBy_of_covBy_covBy_sup` states that if `a` and `b` are covered by their supremum `a ⊔ b` (denoted as `a ⋖ a ⊔ b` and `b ⋖ a ⊔ b`), then their infimum `a ⊓ b` is covered by `a`. In other words, if the supremum of `a` and `b` covers both `a` and `b`, then `a` covers the infimum of `a` and `b`.
More concisely: In a weak lower modular lattice, if `a` and `b` are covered by their supremum, then `a` covers their infimum.
|
IsModularLattice.sup_inf_le_assoc_of_le
theorem IsModularLattice.sup_inf_le_assoc_of_le :
∀ {α : Type u_2} [inst : Lattice α] [self : IsModularLattice α] {x : α} (y : α) {z : α},
x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
The theorem `IsModularLattice.sup_inf_le_assoc_of_le` expresses a property of modular lattices in order theory. Specifically, it states that for any type `α` that forms a lattice and is modular, and for any elements `x`, `y`, and `z` of this type, if `x` is less than or equal to `z`, then the infimum (greatest lower bound) of the supremum (least upper bound) of `x` and `y` with `z` is less than or equal to the supremum of `x` and the infimum of `y` and `z`. This can be denoted mathematically as: if `x ≤ z`, then `(x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)`.
More concisely: In a modular lattice, if `x` is less than or equal to `z`, then `(x ⊔ y) ⊓ z` is less than or equal to `x ⊔ (y ⊓ z)`, where `⊔` denotes the supremum (least upper bound) and `⊓` the infimum (greatest lower bound) operations.
|
CovBy.inf_of_sup_left
theorem CovBy.inf_of_sup_left :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → a ⊓ b ⋖ b
This theorem, referred to as `CovBy.inf_of_sup_left`, establishes a property of lattices, specifically lower modular lattices. For any such lattice of type `α`, and any two elements `a` and `b` of this type, if `a` is covered by the supremum (least upper bound) of `a` and `b`, then the infimum (greatest lower bound) of `a` and `b` is covered by `b`. This is a fundamental property of ordering in a lower modular lattice.
More concisely: In a lower modular lattice, if an element is covered by the supremum of two elements, then the infimum of those two elements is covered by the larger one.
|
inf_sup_assoc_of_le
theorem inf_sup_assoc_of_le :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] {x : α} (y : α) {z : α},
z ≤ x → x ⊓ y ⊔ z = x ⊓ (y ⊔ z)
This theorem, `inf_sup_assoc_of_le`, states that for any type `α` that forms a lattice and is a modular lattice, and for any elements `x`, `y`, and `z` in `α`, if `z` is less than or equal to `x`, then the infimum (greatest lower bound) of `x` and `y` combined with the supremum (least upper bound) of `z`, is equal to the infimum of `x` and the supremum of `y` and `z`. This is a property of the associativity between the infimum and supremum operations in a modular lattice.
More concisely: In a modular lattice, the infimum of the infimum of two elements and the supremum of a third element equals the infimum of the first two elements and the supremum of the third.
|
CovBy.sup_of_inf_of_inf_left
theorem CovBy.sup_of_inf_of_inf_left :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsWeakUpperModularLattice α] {a b : α},
a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b
This theorem, `CovBy.sup_of_inf_of_inf_left`, states that for any type `α` that is a lattice and a weak upper modular lattice, given any two elements `a` and `b` of this type, if the infimum (`⊓`, greatest lower bound) of `a` and `b` is covered by `a` and the infimum of `a` and `b` is also covered by `b`, then `a` is covered by the supremum (`⊔`, least upper bound) of `a` and `b`. In mathematical terms, if $a \wedge b < a$ and $a \wedge b < b$ then $a < a \vee b$.
More concisely: If in a lattice and weak upper modular lattice, the infimum of two elements is covered by each element, then the elements are related by the ordering of their supremum. (That is, $a \wedge b < a$ and $a \wedge b < b$ imply $a < a \vee b$.)
|
CovBy.sup_of_inf_right
theorem CovBy.sup_of_inf_right :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsUpperModularLattice α] {a b : α}, a ⊓ b ⋖ b → a ⋖ a ⊔ b
The theorem `CovBy.sup_of_inf_right` states that for any lattice that is also an upper modular lattice, and for any two elements `a` and `b` of the lattice, if `a` inf `b` is strictly covered by `b`, then `a` is strictly covered by `a` sup `b`. Here, the operator `⊓` represents the infimum or 'greatest lower bound' operation, `⋖` represents the 'strictly covered by' relation, and `⊔` represents the supremum or 'least upper bound' operation.
More concisely: If in an upper modular lattice, `a` inf `b` strictly covers `b`, then `a = a ⊔ b`.
|
sup_inf_assoc_of_le
theorem sup_inf_assoc_of_le :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] {x : α} (y : α) {z : α},
x ≤ z → (x ⊔ y) ⊓ z = x ⊔ y ⊓ z
This theorem, `sup_inf_assoc_of_le`, states that for any type `α` that forms a lattice and is also a modular lattice, and for any elements `x`, `y`, and `z` of that type, if `x` is less than or equal to `z`, then the supremum (join) of `x` and `y`, infimum (meet) with `z`, is equal to `x` join with the infimum of `y` and `z`. This theorem captures an important property of modular lattices - the associativity of supremum and infimum under the given condition.
More concisely: For any lattice and modular lattice type `α` and elements `x`, `y`, `z` of `α`, if `x ≤ z`, then `x ⨂ (y ⋁ z) = (x ⋁ y) ⋁ z`, where `⨂` denotes infimum (meet) and `⋁` denotes supremum (join).
|
IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy
theorem IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy :
∀ {α : Type u_2} [inst : Lattice α] [self : IsWeakUpperModularLattice α] {a b : α},
a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b
This theorem states that in a weak upper modular lattice of type α, for any two elements `a` and `b` in the lattice, if `a` and `b` both cover the infimum of `a` and `b` (denoted as `a ⊓ b`), then the supremum of `a` and `b` (denoted as `a ⊔ b`) covers `a`. In the context of lattices, the term "cover" means that one element is immediately above another, with no elements in between.
More concisely: In a weak upper modular lattice, if elements `a` and `b` both cover their infimum `a ⊓ b`, then `a ⊔ b` covers `a`.
|