GaloisConnection.l_u_l_eq_l
theorem GaloisConnection.l_u_l_eq_l :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ (a : α), l (u (l a)) = l a
The theorem `GaloisConnection.l_u_l_eq_l` states that for any types `α` and `β` equipped with a preorder and a partial order respectively, and given functions `l : α → β` and `u : β → α` that establish a Galois connection between `α` and `β`, for any element `a` of type `α`, applying `l` to `u` of `l` of `a` gives back `l` of `a`. This property is essentially saying that the application of `l` after `u` after `l` is idempotent.
More concisely: For any Galois connection between preordered type `α` and ordered type `β` with functions `l : α → β` and `u : β → α`, the composition `l ∘ u ∘ l` equals `l`.
|
GaloisConnection.l_bot
theorem GaloisConnection.l_bot :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot β]
[inst_3 : OrderBot α] {l : α → β} {u : β → α}, GaloisConnection l u → l ⊥ = ⊥
This theorem states that for any two ordered types `α` and `β`, both with a bottom element (`OrderBot α` and `OrderBot β` respectively), if there is a Galois connection between `α` and `β` given by functions `l` and `u`, then the minimum (bottom) element of `α` mapped by the function `l` is the minimum (bottom) element of `β`. In other words, the bottom element of `α` when transformed by `l`, stays the bottom element in the `β` space, respecting the Galois connection between the two spaces.
More concisely: For any Galois connection between ordered types `α` and `β` with bottom elements, the image of the bottom element of `α` under the left adjoint function `l` is the bottom element of `β`.
|
GaloisConnection.compose
theorem GaloisConnection.compose :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
{l1 : α → β} {u1 : β → α} {l2 : β → γ} {u2 : γ → β},
GaloisConnection l1 u1 → GaloisConnection l2 u2 → GaloisConnection (l2 ∘ l1) (u1 ∘ u2)
The theorem `GaloisConnection.compose` states that if we have two Galois connections, the first one between sets of types `α` and `β` with functions `l1` and `u1`, and the second one between sets of types `β` and `γ` with functions `l2` and `u2`, then the composition of these Galois connections, with `l2 ∘ l1` and `u1 ∘ u2`, is also a Galois connection. Here `α`, `β`, and `γ` are types with a preorder, and a Galois connection between two preordered sets is a pair of functions `l` and `u` where for all elements `a` of the first set and `b` of the second set, `l a ≤ b` if and only if `a ≤ u b`.
More concisely: Given Galois connections between sets `α` and `β` with functions `l1` and `u1`, and between sets `β` and `γ` with functions `l2` and `u2`, the composition of these Galois connections, defined by `l2 ∘ l1` and `u1 ∘ u2`, is itself a Galois connection between `α` and `γ`.
|
GaloisConnection.u_sInf
theorem GaloisConnection.u_sInf :
∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {s : Set β}, u (sInf s) = ⨅ a ∈ s, u a
The theorem `GaloisConnection.u_sInf` states that for any types `α` and `β` which form complete lattices, and for any functions `l : α → β` and `u : β → α` that form a Galois connection, the function `u` applied to the infimum (`sInf`) of a set `s` of elements of type `β` is equal to the infimum of the function `u` applied to each element of the set `s`. In mathematical terms, this can be represented as \(u(\text{inf}(s)) = \text{inf}\{u(a) : a \in s\}\). This theorem captures one of the important properties of Galois connections in the context of complete lattices.
More concisely: For any complete lattices α and β, and any Galois connection {l : α → β, u : β → α}, u(∧^β s) = ∧^α {u(a) | a ∈ s}, where ∧^β s is the infimum of set s in lattice β and ∧^α {u(a) | a ∈ s} is the infimum of the set {u(a) | a ∈ s} in lattice α.
|
GaloisConnection.isLeast_l
theorem GaloisConnection.isLeast_l :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {a : α}, IsLeast {b | a ≤ u b} (l a)
The theorem `GaloisConnection.isLeast_l` states that: For any types `α` and `β` that are preordered, any two functions `l : α → β` and `u : β → α` forming a Galois Connection, and any element `a` of type `α`, the image of `a` under `l` is a least element of the set of `b` in `β` such that `a` is less than or equal to `u b`. In other words, if you have a Galois Connection between two preordered sets, then for any element in the first set, the image of that element in the second set through the function `l` is the smallest element among those to which it is related by the Galois Connection.
More concisely: For any Galois connection between preordered types `α` and `β` and any `α` element `a`, `l(a)` is the least `β` element greater than or equal to `u(b)` for all `β` elements `b` less than or equal to `a`.
|
GaloisConnection.l_u_le
theorem GaloisConnection.l_u_le :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ (a : β), l (u a) ≤ a
The theorem `GaloisConnection.l_u_le` states that for any types `α` and `β` that have a preorder relation defined on them, and any functions `l : α → β` and `u : β → α` forming a Galois connection, for every element `a` of type `β`, the inequality `l (u a) ≤ a` holds. In other words, applying `u` to `a` and then `l` to the result never produces a value greater than the original `a`. This is a characteristic property of Galois connections in order theory.
More concisely: For any Galois connection between types `α` and `β` with functions `l : α → β` and `u : β → α`, `l (u a) ≤ a` for all `a : β`.
|
GaloisInsertion.gc
theorem GaloisInsertion.gc :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisInsertion l u → GaloisConnection l u
This theorem states that for any types `α` and `β`, if there exists a preorder relation on both types and there are functions `l : α → β` and `u : β → α` which form a Galois insertion, then this Galois insertion implies the existence of a Galois connection between `l` and `u`. In other words, if a pair of functions `l` and `u` satisfy the properties of a Galois insertion, they also satisfy the properties of a Galois connection.
In mathematical terms, if for all `a : α` and `b : β`, `l a ≤ b` if and only if `a ≤ u b` (the definition of a Galois connection), then there exists a corresponding Galois insertion. Here, the functions `l` and `u` are said to form a Galois connection if, for every `a : α` and `b : β`, `l a ≤ b` if and only if `a ≤ u b`.
More concisely: If `l` and `u` form a Galois insertion between types `α` and `β` with a preorder relation, then `l` and `u` also form a Galois connection.
|
GaloisCoinsertion.u_sup_l
theorem GaloisCoinsertion.u_sup_l :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β],
GaloisCoinsertion l u → ∀ (a b : α), u (l a ⊔ l b) = a ⊔ b
This theorem states that for any two types `α` and `β`, a function `l` from `α` to `β`, a function `u` from `β` to `α`, and two elements `a` and `b` of type `α`, given that there exists a Galois coinsertion for `l` and `u`, and both `α` and `β` are semilattice sups, then applying `u` to the sup of `l a` and `l b` yields the same result as taking the sup of `a` and `b` itself. In other words, the sup operation (usually depicted as `⊔`), when applied after the function `l` and then `u`, is preserved. This theorem is a fundamental property of Galois coinsertions in the context of ordered algebraic structures.
More concisely: For any semilattice suprema `l a`, `l b` of types `α`, and functions `l : α → β`, `u : β → α` with a Galois coinsertion, we have `u (l a ⊔ l b) = a ⊔ b`.
|
GaloisConnection.l_sSup
theorem GaloisConnection.l_sSup :
∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {s : Set α}, l (sSup s) = ⨆ a ∈ s, l a
This theorem states that for any two types `α` and `β` which are complete lattices, and for any pair of functions `l` from `α` to `β` and `u` from `β` to `α` that form a Galois connection, the application of `l` to the supremum of any set `s` of type `α` is equal to the supremum of the set obtained by applying `l` to each element of `s`. In other words, under a Galois connection, the function `l` preserves the supremum operation from the lattice of `α` to the lattice of `β`.
More concisely: Given complete lattices `α` and `β`, and a Galois connection between functions `l: α → β` and `u: β → α`, the supremum of `l` applied to a set `s ⊆ α` equals the application of `l` to the set `{l(x) | x ∈ s} ⊆ β`.
|
GaloisConnection.isLUB_l_image
theorem GaloisConnection.isLUB_l_image :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {s : Set α} {a : α}, IsLUB s a → IsLUB (l '' s) (l a)
The theorem `GaloisConnection.isLUB_l_image` asserts that for any two types `α` and `β` with preorders, and functions `l : α → β` and `u : β → α` forming a Galois connection, if `a` is a least upper bound (LUB) of a set `s` of elements from type `α`, then `l a` is the least upper bound of the image of `s` under `l`. In other words, the image under the function `l` of a set which has a least upper bound `a`, has its least upper bound at `l a`.
More concisely: Given a Galois connection between preordered types `α` and `β` via functions `l : α → β` and `u : β → α`, if `a` is the least upper bound of a set `s` in `α`, then `l a` is the least upper bound of `l''s` in `β`.
|
GaloisConnection.u_unique
theorem GaloisConnection.u_unique :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u →
∀ {l' : α → β} {u' : β → α}, GaloisConnection l' u' → (∀ (a : α), l a = l' a) → ∀ {b : β}, u b = u' b
The theorem `GaloisConnection.u_unique` states that for any two types `α` and `β` that are partially ordered and pre-ordered respectively, if there exists two pairs of functions `(l, u)` and `(l', u')` that both form a Galois connection between `α` and `β`, then if all elements of `α` map to the same value under both `l` and `l'`, it necessarily follows that all elements of `β` map to the same value under both `u` and `u'`. In other words, if two Galois connections on the same types have the same lower adjoint, they must also have the same upper adjoint.
More concisely: If two Galois connections between partially ordered type `α` and pre-ordered type `β` have the same lower adjoint functions, then their upper adjoint functions are equal.
|
GaloisCoinsertion.gc
theorem GaloisCoinsertion.gc :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisCoinsertion l u → GaloisConnection l u
This theorem, referred to as `GaloisCoinsertion.gc`, states that for any two types `α` and `β` that are preordered, and for any two functions `l : α → β` and `u : β → α`, if `l` and `u` form a Galois coinsertion then they also form a Galois connection. In other words, if a pair of functions `l` and `u` satisfy the properties of a Galois coinsertion, then they also satisfy the condition `l a ≤ b ↔ a ≤ u b` for all `a` in `α` and `b` in `β`, which defines a Galois connection.
More concisely: If `l` and `u` form a Galois coinsertion between preordered types `α` and `β`, then `l` and `u` satisfy the condition that `l a ≤ b ↔ a ≤ u b` for all `a ∈ α` and `b ∈ β`.
|
OrderIso.bddAbove_image
theorem OrderIso.bddAbove_image :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set α},
BddAbove (⇑e '' s) ↔ BddAbove s
The theorem `OrderIso.bddAbove_image` states that for any two types `α` and `β`, both equipped with a preorder, and an order isomorphism `e` from `α` to `β`, a set `s` of type `α` is bounded above if and only if the image of `s` under the isomorphism `e` is also bounded above. This theorem basically shows that the property of being bounded above is preserved under an order isomorphism.
More concisely: For any preorders on types `α` and `β`, and an order isomorphism `e` from `α` to `β`, if a subset `s` of `α` is bounded above, then the image of `s` under `e` is also bounded above.
|
GaloisInsertion.l_iSup_u
theorem GaloisInsertion.l_iSup_u :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
GaloisInsertion l u → ∀ {ι : Sort x} (f : ι → β), l (⨆ i, u (f i)) = ⨆ i, f i
The theorem `GaloisInsertion.l_iSup_u` states that for all types `α` and `β`, and for all functions `l : α → β` and `u : β → α`, given `α` and `β` are both complete lattices, and that there is a Galois insertion between `l` and `u`, then for any function `f : ι → β`, where ι is an arbitrary type, the lift of the supremum (least upper bound) of `u` applied to `f i` for all `i` under `l` equals to the supremum of `f i` for all `i`. Symbolically, this can be expressed as \(l (\bigvee_{i} u(f(i))) = \bigvee_{i} f(i)\).
More concisely: Given types `α` and `β`, functions `l : α → β` and `u : β → α` between complete lattices with a Galois insertion, and a function `f : ι → β`, the lift of the supremum of `u(f i)` under `l` is equal to the supremum of `f i` for all `i`. Symbolically, \(l (\bigvee\_{i} u(f(i))) = \bigvee\_{i} f(i)\).
|
GaloisConnection.le_u
theorem GaloisConnection.le_u :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {a : α} {b : β}, l a ≤ b → a ≤ u b
The theorem `GaloisConnection.le_u` states that for any types `α` and `β` that have a Preorder structure, and for any functions `l : α → β` and `u : β → α`, if `l` and `u` form a Galois connection, then for all elements `a` of type `α` and `b` of type `β`, if `l a` is less than or equal to `b`, then `a` is less than or equal to `u b`.
More concisely: For any Preorder types α and β and Galois connection functions l : α → β and u : β → α, if l(a) ≤ b holds then a ≤ u(b).
|
GaloisCoinsertion.l_injective
theorem GaloisCoinsertion.l_injective :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder α] [inst_1 : Preorder β],
GaloisCoinsertion l u → Function.Injective l
The theorem `GaloisCoinsertion.l_injective` states that for any two types `α` and `β`, if there is a function `l` from `α` to `β` and a function `u` from `β` to `α`, such that `α` has a partial order and `β` has a preorder, and there is a Galois coinsertion between `l` and `u`, then the function `l` is injective. Here, the injective means that for all `x` and `y` in `α`, if `l(x) = l(y)` then `x = y`. The Galois coinsertion, in this case, is a specific relationship between the functions `l` and `u` related to their ordering properties.
More concisely: If there is a Galois coinsertion between functions `l: α → β` and `u: β → α` with `α` a partial order and `β` a preorder, then `l` is an injective function.
|
GaloisInsertion.isLUB_of_u_image
theorem GaloisInsertion.isLUB_of_u_image :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β],
GaloisInsertion l u → ∀ {s : Set β} {a : α}, IsLUB (u '' s) a → IsLUB s (l a)
The theorem `GaloisInsertion.isLUB_of_u_image` states that for any types `α` and `β`, given a function `l` from `α` to `β`, a function `u` from `β` to `α`, a set `s` of type `β`, and an element `a` of type `α`, if there exists a Galois insertion between these functions `l` and `u` (indicating a certain relationship between them regarding closure operations), and `a` is a least upper bound (LUB) of the image of set `s` under function `u`, then the image of `a` under function `l` is a least upper bound of the original set `s`. This theorem is in the context of partial orderings, which are given by the `Preorder` type classes on `α` and `β`.
More concisely: If there is a Galois connection between functions `l: α → β` and `u: β → α` and `a ∈ α` is the least upper bound of set `s ⊆ β` under `u`, then `l(a)` is the least upper bound of set `s` under `l`.
|
GaloisInsertion.strictMono_u
theorem GaloisInsertion.strictMono_u :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β],
GaloisInsertion l u → StrictMono u
The theorem `GaloisInsertion.strictMono_u` states that for any two types `α` and `β` with preorder, given functions `l : α → β` and `u : β → α` such that `GaloisInsertion l u` holds (meaning `l` and `u` form a Galois Insertion), the function `u` is strictly monotone. In other words, if `a < b` for any two elements `a`, `b` in the type `β`, then `u(a) < u(b)`.
More concisely: If `l : α → β` and `u : β → α` form a Galois Insertion in types `α` and `β` with preorder, then `u` is a strictly monotone function.
|
GaloisInsertion.l_inf_u
theorem GaloisInsertion.l_inf_u :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β],
GaloisInsertion l u → ∀ (a b : β), l (u a ⊓ u b) = a ⊓ b
This theorem states that for any two types `α` and `β`, and any two functions `l : α → β` and `u : β → α`, if `l` and `u` form a Galois Insertion and the SemilatticeInf structure exists on both `α` and `β`, then for any elements `a` and `b` of type `β`, the result of applying `l` to the infimum of `u a` and `u b` is equal to the infimum of `a` and `b`. In terms of order theory, this basically asserts that the lower adjoint `l` of a Galois insertion preserves infimums.
More concisely: For any Galois insertions `l : α → β` and `u : β → α` between semilattically ordered types `α` and `β`, the lower adjoint `l` preserves infima, that is, `l (inf (u a) (u b)) = inf a b`.
|
GaloisCoinsertion.u_l_eq
theorem GaloisCoinsertion.u_l_eq :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder α] [inst_1 : Preorder β],
GaloisCoinsertion l u → ∀ (a : α), u (l a) = a
This theorem states that for any types `α` and `β` and functions `l : α → β` and `u : β → α`, given a partial order on `α` and a preorder on `β`, if there exists a Galois coinsertion between `l` and `u`, then for any element `a` of type `α`, applying `l` to `a` and then `u` to the result returns `a`. In other words, the function `u` followed by `l` acts as the identity on `α`. This property is a fundamental characteristic of Galois coinsertions in order theory.
More concisely: Given functions `l : α → β` and `u : β → α` between partially ordered types `α` and `β` with a preorder on `β`, if there is a Galois coinsertion between `l` and `u`, then `u ∘ l = id_α`.
|
GaloisConnection.monotone_u
theorem GaloisConnection.monotone_u :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → Monotone u
The theorem `GaloisConnection.monotone_u` states that for any types `α` and `β` that have a preorder, and for any functions `l : α → β` and `u : β → α` that form a Galois connection, the function `u` is monotone. In other words, if `l` and `u` satisfy the property that for all `a` in `α` and `b` in `β`, `l a` is less than or equal to `b` if and only if `a` is less than or equal to `u b`, then whenever `b1` is less than or equal to `b2` for any `b1, b2` in `β`, we have `u b1` is less than or equal to `u b2`.
More concisely: If `l : α → β` and `u : β → α` form a Galois connection on preordered types `α` and `β`, then the function `u` is monotone, i.e., `u (b1) ≤ u (b2)` for all `b1 ≤ b2` in `β`.
|
GaloisCoinsertion.l_le_l_iff
theorem GaloisCoinsertion.l_le_l_iff :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β],
GaloisCoinsertion l u → ∀ {a b : α}, l a ≤ l b ↔ a ≤ b
This theorem states that for any types `α` and `β`, and any functions `l : α → β` and `u : β → α`, where `α` and `β` both have a preorder (a binary relation that is reflexive and transitive), if `l` and `u` form a Galois coinsertion, then for all elements `a` and `b` of `α`, `l a` is less than or equal to `l b` if and only if `a` is less than or equal to `b`. A Galois coinsertion is a special relationship between two functions, where one function is the left adjoint and the other is the right adjoint, and the function composition from right to left is less than or equal to the identity function.
More concisely: For functions `l : α → β` and `u : β → α` between preordered types `α` and `β`, if `l` and `u` form a Galois coinsertion, then `l a ≤ l b` if and only if `a ≤ b`.
|
GaloisInsertion.l_surjective
theorem GaloisInsertion.l_surjective :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : PartialOrder β],
GaloisInsertion l u → Function.Surjective l
The theorem `GaloisInsertion.l_surjective` states that for any types `α` and `β` with a function `l : α → β` and `u : β → α`, where `α` is a preorder and `β` is a partial order, if `l` and `u` form a Galois insertion, then the function `l` is surjective. In mathematical terms, this means that for every element `b` in `β`, there exists an element `a` in `α` such that `l(a) = b`.
More concisely: If `l : α -> β` and `u : β -> α` form a Galois insertion between preordered type `α` and partially ordered type `β`, then `l` is surjective.
|
GaloisCoinsertion.u_l_le
theorem GaloisCoinsertion.u_l_le :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisCoinsertion l u → ∀ (x : α), u (l x) ≤ x
This theorem states the main property of a Galois coinsertion in the context of preordered sets. Specifically, for any types `α` and `β` with preorder structures, and function `l` from `α` to `β` and function `u` from `β` to `α` such that `l` and `u` form a Galois coinsertion, for any element `x` of type `α`, the result of applying `u` to the result of applying `l` to `x` is less than or equal to `x`. This is a key property that defines the notion of Galois coinsertion, which is a concept in order theory, a branch of mathematics that deals with the properties and structure of ordered sets.
More concisely: For any preordered sets (α, ≤α) and (β, ≤β), and Galois coinsertion pair (l : α → β, u : β → α) with l ∘ u ≤ idβ, we have u (l x) ≤ x for all x : α.
|
GaloisCoinsertion.u_surjective
theorem GaloisCoinsertion.u_surjective :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder α] [inst_1 : Preorder β],
GaloisCoinsertion l u → Function.Surjective u
The theorem `GaloisCoinsertion.u_surjective` states that for any two types `α` and `β`, and any two functions `l : α → β` and `u : β → α`, given that `α` is a partial order and `β` is a preorder, if a Galois coinsertion exists between `l` and `u`, then the function `u` is surjective. In other words, for every element of type `β`, there exists an element of type `α` such that applying the function `u` to the element of type `β` yields this element of `α`.
More concisely: If `l : α → β` and `u : β → α` define a Galois coinsertion between partial order `α` and preorder `β`, then `u` is a surjection.
|
GaloisInsertion.l_u_eq
theorem GaloisInsertion.l_u_eq :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : PartialOrder β],
GaloisInsertion l u → ∀ (b : β), l (u b) = b
This theorem states that for any types `α` and `β`, and any functions `l : α → β` and `u : β → α`, given a preorder on `α` and a partial order on `β`, if a Galois insertion is established between `l` and `u`, then for any element `b` of type `β`, applying `u` followed by `l` to `b` will yield `b` again. In other words, the composition of `l` and `u` acts as the identity on the domain of `β`. This is a characteristic property of Galois insertions, which are a fundamental concept in order theory and lattice theory.
More concisely: Given a Galois insertion between functions `l : α → β` and `u : β → α` over a preorder on `α` and a partial order on `β`, `u ∘ l = id_β`.
|
GaloisConnection.l_eq_bot
theorem GaloisConnection.l_eq_bot :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot β] {l : α → β}
{u : β → α}, GaloisConnection l u → ∀ {x : α}, l x = ⊥ ↔ x ≤ u ⊥
This theorem states that for any types `α` and `β` with a preorder on `α`, a partial order on `β`, and a least element (denoted as `⊥`) in `β`, and any functions `l: α → β` and `u: β → α` that form a Galois connection, then for any element `x` of `α`, `l x` is equal to the least element in `β` if and only if `x` is less than or equal to `u ⊥`. This theorem is crucial in connecting the concept of a Galois connection to the properties of the associated order structures.
More concisely: For any Galois connection between preordered type `α` and partially ordered type `β` with a least element `⊥`, the image `l(x)` of an element `x` in `α` under `l` is equal to `⊥` if and only if `x` is less than or equal to `u⊥` in `α`.
|
GaloisConnection.le_u_l_trans
theorem GaloisConnection.le_u_l_trans :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {x y z : α}, x ≤ u (l y) → y ≤ u (l z) → x ≤ u (l z)
This theorem states that if `(l, u)` forms a Galois connection, then the relation `x ≤ u (l y)` is transitive. In other words, if for any elements `x`, `y`, and `z` in a preordered set `α`, if `x` is less than or equal to `u(l(y))` and `y` is less than or equal to `u(l(z))`, then `x` is less than or equal to `u(l(z))`. If `l` is a closure operator (such as `Submodule.span` or `Subgroup.closure`) and `u` is the coercion to `Set`, this can be interpreted as: if `U` is in the closure of `V` and `V` is in the closure of `W`, then `U` is in the closure of `W`.
More concisely: If `(l, u)` is a Galois connection on a preordered set, then the relation `x ≤ u(l(y))` is transitive, meaning that if `x ≤ u(l(y))` and `y ≤ u(l(z))`, then `x ≤ u(l(z))`.
|
GaloisConnection.u_l_u_eq_u
theorem GaloisConnection.u_l_u_eq_u :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ (b : β), u (l (u b)) = u b
The theorem `GaloisConnection.u_l_u_eq_u` states that for any types `α` and `β` with `α` partially ordered and `β` preordered, and for any functions `l : α → β` and `u : β → α` that form a Galois connection, the value of `u` applied to the composition of `l` and `u` applied to any element `b` of type `β` is equal to `u` applied to `b`. In other words, it states that in a Galois connection, the composition of `u`, `l`, and `u` is a kind of idempotent operation on `u`.
More concisely: In a Galois connection between partially ordered type `α` and preordered type `β` given functions `l : α → β` and `u : β → α`, the composition `u ∘ l ∘ u` equals `u`.
|
GaloisConnection.l_le
theorem GaloisConnection.l_le :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {a : α} {b : β}, a ≤ u b → l a ≤ b
This theorem states that for any types `α` and `β` which have preorder relations, and for any functions `l : α → β` and `u : β → α` which form a Galois connection, if an element `a` of type `α` is less than or equal to `u b` (where `b` is an element of type `β`), then `l a` is less than or equal to `b`. This is a part of the definition of a Galois connection which states that `l a ≤ b` if and only if `a ≤ u b`. In essence, this theorem captures one direction of this equivalence.
More concisely: For any Galois connection between preordered types `α` and `β` and elements `a : α` and `b : β` with `a ≤ u b`, it holds that `l a ≤ b`.
|
sInf_image2_eq_sInf_sInf
theorem sInf_image2_eq_sInf_sInf :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
[inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β},
(∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) →
(∀ (a : α), GaloisConnection (l₂ a) (u a)) → sInf (Set.image2 u s t) = u (sInf s) (sInf t)
The theorem `sInf_image2_eq_sInf_sInf` states that for any types `α`, `β`, and `γ` that are complete lattices, any sets `s` and `t` of `α` and `β` respectively, and any binary function `u` from `α` and `β` to `γ`, if for each `b` in `β`, the function `l₁ b` and the function `u` with its arguments swapped form a Galois connection, and if for each `a` in `α`, the function `l₂ a` and the function `u` with `a` fixed form a Galois connection, then the infimum of the image of the binary function `u` over the sets `s` and `t` is equal to the value of the function `u` at the infimum of `s` and the infimum of `t`.
In simpler words, this theorem is about the relationship between a binary function applied to two sets and the infimum (greatest lower bound) of those sets. It says that under certain conditions (the Galois connections), the infimum of all function values is the same as the function value at the infimum of the sets.
More concisely: If `u:` `α` x `β` -> `γ`, `s` a set of `α`, and `t` a set of `β` are such that for all `b` in `β`, the functions `l₁ b` and `u` with arguments swapped form a Galois connection, and for all `a` in `α`, the functions `l₂ a` and `u` with `a` fixed form a Galois connection, then `inf (map u s) = u (inf s inf t)`.
|
GaloisConnection.u_inf
theorem GaloisConnection.u_inf :
∀ {α : Type u} {β : Type v} {b₁ b₂ : β} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {l : α → β}
{u : β → α}, GaloisConnection l u → u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂
The theorem `GaloisConnection.u_inf` states that for any types `α` and `β`, given two elements `b₁` and `b₂` in `β`, if `α` and `β` are both semilattice inf (i.e., they are equipped with a binary operation "infimum" or "meet" denoted by `⊓` which is associative, commutative, idempotent, and satisfies the absorption law), and if `l` and `u` establish a Galois connection between `α` and `β`, then the infimum of `u(b₁)` and `u(b₂)` in `α` is equal to `u` of the infimum of `b₁` and `b₂` in `β`. In simpler terms, the `u` function preserves the infimum operation from `β` to `α`.
More concisely: For any semilattices `α` and `β` with Galois connection `l` and `u`, the operation `u` preserves the infimum, i.e., `u(inf b₁ b₂) = inf (u b₁) (u b₂)` for all `b₁, b₂ ∈ β`.
|
OrderIso.bddBelow_image
theorem OrderIso.bddBelow_image :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set α},
BddBelow (⇑e '' s) ↔ BddBelow s
This theorem states that for any two types 'α' and 'β' with a pre-order relation, and an order isomorphism 'e' between them, a set 's' of type 'α' is bounded below if and only if the image of 's' under 'e' is also bounded below. In other words, the property of having a lower bound is preserved under an order isomorphism.
More concisely: For any pre-orders on types 'α' and 'β' with an order isomorphism between them, if a subset of 'α' has a lower bound, then its image under the isomorphism has a lower bound in 'β'.
|
GaloisConnection.u_top
theorem GaloisConnection.u_top :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderTop α]
[inst_3 : OrderTop β] {l : α → β} {u : β → α}, GaloisConnection l u → u ⊤ = ⊤
The theorem `GaloisConnection.u_top` states that for any types `α` and `β` which have a partial order and a predefined maximum element (top), if two functions `l : α → β` and `u : β → α` form a Galois connection, then the maximum element of type `β` when mapped through the function `u` gives the maximum element (top) of type `α`. In other words, for a Galois connection, the function `u` sends the top element of `β` to the top element of `α`.
More concisely: For any Galois connection between partially ordered types with top elements, the image of the top element of the second type under the second function is the top element of the first type.
|
gc_Ici_sInf
theorem gc_Ici_sInf :
∀ {α : Type u} [inst : CompleteSemilatticeInf α],
GaloisConnection (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
The theorem `gc_Ici_sInf` states that for any type `α` that has an instance of `CompleteSemilatticeInf` (meaning that `α` forms a complete semilattice with an infimum operation), the composition of `toDual` and `Ici` and the composition of `sInf` and `ofDual` form a Galois connection. In other words, for any two elements `a` and `b` of type `α`, the dual of the left-closed right-infinite interval starting from `a` is less than or equal to `b` if and only if `a` is less than or equal to the infimum of the dual of `b`. Here, `toDual` and `ofDual` are the identity functions to and from the order dual of `α`, `Ici` denotes the left-closed right-infinite interval, and `sInf` denotes the infimum operation in a complete semilattice.
More concisely: For any complete semilattice `α` with infimum operation `sInf`, the dual of the left-closed right-infinite interval `Ici(a)` of an element `a` is less than or equal to `b` if and only if `a` is less than or equal to the infimum of the duals of elements in `Ici(b)`.
|
GaloisInsertion.le_l_u
theorem GaloisInsertion.le_l_u :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisInsertion l u → ∀ (x : β), x ≤ l (u x)
This theorem is stating the main property of a Galois insertion in the context of preordered sets. Specifically, given any two types `α` and `β` with preorder relations, and functions `l : α → β` and `u : β → α` that form a Galois insertion, for any element `x` in `β`, `x` is less than or equal to `l (u x)`. This encapsulates the fundamental property of a Galois insertion that the right adjoint (in this case, `u`) followed by the left adjoint (in this case, `l`) produces a value that is greater than or equal to the original.
More concisely: For any Galois insertion between preordered sets `(α, ≤α)` and `(β, ≤β)` with left adjoint `l : α → β` and right adjoint `u : β → α`, given `x : β`, we have `x ≤ l (u x)`.
|
GaloisConnection.dual
theorem GaloisConnection.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u →
GaloisConnection (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)
The `GaloisConnection.dual` theorem states that for any two types `α` and `β` that are preordered, and two functions `l : α → β` and `u : β → α` that form a Galois Connection, the composition of these functions with the `OrderDual.toDual` and `OrderDual.ofDual` (which are identity functions on the dual orders) also forms a Galois Connection. In other words, it states that the concept of a Galois Connection is preserved under the operation of taking duals of the orders.
More concisely: Given types `α` and `β` preordered with functions `l : α → β` and `u : β → α` forming a Galois connection, their compositions with the order dual functions form another Galois connection. That is, `OrderDual.toDual ∘ l` and `OrderDual.ofDual ∘ u` constitute a Galois connection.
|
GaloisConnection.le_u_l
theorem GaloisConnection.le_u_l :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ (a : α), a ≤ u (l a)
This theorem states that for any types `α` and `β` equipped with preorders, and for any pair of functions `l : α → β` and `u : β → α` forming a Galois connection, it is always the case that `a` is less than or equal to `u (l a)` for all `a` in `α`. In other words, for a Galois connection between two preordered sets, any element `a` from the domain is always less than or equal to the result of applying `u` to the image of `a` under `l`. This property is a fundamental characteristic of a Galois connection in order theory.
More concisely: For any Galois connection between preordered types `α` and `β` via functions `l : α → β` and `u : β → α`, `a ≤ u (l a)` for all `a ∈ α`.
|
sSup_image2_eq_sSup_sSup
theorem sSup_image2_eq_sSup_sSup :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
[inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
(∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
(∀ (a : α), GaloisConnection (l a) (u₂ a)) → sSup (Set.image2 l s t) = l (sSup s) (sSup t)
The theorem states that for all types `α`, `β`, `γ` that have complete lattice structures, given two sets `s : Set α` and `t : Set β`, a binary function `l : α → β → γ`, and two functions `u₁ : β → γ → α` and `u₂ : α → γ → β` that form Galois connections when combined with `l` (where `l` is swapped with `b` for `u₁`), the supremum (or the least upper bound) of the image of the binary function applied to `s` and `t` is equal to the result of applying `l` to the supremum of `s` and the supremum of `t`.
In mathematical terms, if we have a Galois connection between functions `l` and `u₁` (for each `b : β`) and between `l` and `u₂` (for each `a : α`), then we have $\sup(l(s,t)) = l(\sup s, \sup t)$ where $l$ is a binary function and $s$ and $t$ are sets in the respective complete lattices.
More concisely: For sets $s$ and $t$ in complete lattices $\alpha$ and $\beta$, respectively, and with Galois connections between the binary function $l$ and functions $u\_1$ and $u\_2$, we have $\sup(l(s,t)) = l(\sup s, \sup t)$.
|
GaloisInsertion.choice_eq
theorem GaloisInsertion.choice_eq :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
(self : GaloisInsertion l u) (a : α) (h : u (l a) ≤ a), self.choice a h = l a
This theorem states a property of the choice function in the context of a Galois insertion. For any types α and β, where both α and β are preordered, and for any functions `l : α → β` and `u : β → α` constituting a Galois insertion, if an element `a` of α satisfies the condition that `u (l a)` is less than or equal to `a`, then the choice function applied to `a` and `h` (which is the proof of the condition) will equal `l a`. This essentially describes the Galois connection between the preordered sets α and β, and how elements are related under specific conditions.
More concisely: For any Galois insertion between preordered types α and β given by functions `l : α → β` and `u : β → α`, if `a ∈ α` satisfies `u (l a) ≤ a`, then the choice function `choose_galois α β h a = l a`, where `h : u (l a) ≤ a`.
|
GaloisConnection.l_comm_of_u_comm
theorem GaloisConnection.l_comm_of_u_comm :
∀ {X : Type u_2} [inst : Preorder X] {Y : Type u_3} [inst_1 : Preorder Y] {Z : Type u_4} [inst_2 : Preorder Z]
{W : Type u_5} [inst_3 : PartialOrder W] {lYX : X → Y} {uXY : Y → X},
GaloisConnection lYX uXY →
∀ {lWZ : Z → W} {uZW : W → Z},
GaloisConnection lWZ uZW →
∀ {lWY : Y → W} {uYW : W → Y},
GaloisConnection lWY uYW →
∀ {lZX : X → Z} {uXZ : Z → X},
GaloisConnection lZX uXZ →
(∀ (w : W), uXZ (uZW w) = uXY (uYW w)) → ∀ {x : X}, lWZ (lZX x) = lWY (lYX x)
The theorem `GaloisConnection.l_comm_of_u_comm` states that for any four types `X`, `Y`, `Z`, and `W`, with `X`, `Y`, and `Z` being preordered and `W` being partially ordered, and four Galois connections given by functions `(lYX, uXY)`, `(lWZ, uZW)`, `(lWY, uYW)`, and `(lZX, uXZ)`, if for every element `w` in `W`, the composition of `uXZ` and `uZW` applied to `w` is equal to the composition of `uXY` and `uYW` applied to `w`, then for every element `x` in `X`, the composition of `lWZ` and `lZX` applied to `x` is equal to the composition of `lWY` and `lYX` applied to `x`. This theorem shows the interplay between multiple Galois connections under certain conditions.
More concisely: If `uXZ ∘ uZW = uXY ∘ uYW` for all `w` in `W`, then `lWZ ∘ lZX = lWY ∘ lYX` for all `x` in `X`.
|
GaloisConnection.exists_eq_l
theorem GaloisConnection.exists_eq_l :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ (b : β), (∃ a, b = l a) ↔ b = l (u b)
This theorem states that given a Galois connection, defined by functions `l : α → β` and `u : β → α` between types `α` and `β` with preorder and partial order structures respectively, if there exists an element `a` in `α` such that `b` in `β` is equal to `l a`, then `a` is equal to `u b`. In other words, for any `b` in `β`, there exists an `a` in `α` such that `b` is the image of `a` under `l` if and only if `b` is the image of `u b` under `l`. This characterizes `u b` as a particular 'pre-image' of `b` under `l` in the context of a Galois connection.
More concisely: In a Galois connection with functions `l : α → β` and `u : β → α`, if `l a = b` implies `a = u b`, then `l` and `u` have mutual inverse images.
|
GaloisInsertion.u_le_u_iff
theorem GaloisInsertion.u_le_u_iff :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β],
GaloisInsertion l u → ∀ {a b : β}, u a ≤ u b ↔ a ≤ b
The theorem states that for all types `α` and `β` with preorders, and for all functions `l` from `α` to `β` and `u` from `β` to `α` that form a Galois insertion, the inequality `u a ≤ u b` holds if and only if `a ≤ b` for any elements `a` and `b` of `β`. In other words, for a Galois insertion, the ordering of elements in `β` is preserved when mapped to `α` via function `u`.
More concisely: For every Galois insertion between preordered types `α` and `β` via functions `l` from `α` to `β` and `u` from `β` to `α`, the order relation `u(a) ≤ u(b)` in `α` if and only if `a ≤ b` in `β` for all elements `a` and `b` in `β`.
|
GaloisConnection.exists_eq_u
theorem GaloisConnection.exists_eq_u :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ (a : α), (∃ b, a = u b) ↔ a = u (l a)
This theorem states that given a Galois connection, denoted by the functions `l` and `u` between two preordered sets `α` and `β`, for any element `a` in `α`, there exists an element `b` such that `a = u b` if and only if `a = u (l a)`. In other words, if there's an element `b` that makes `a` equal to `u b`, then `l a` is guaranteed to be one such element.
More concisely: For any element `a` in a preordered set `α` with respect to a given Galois connection `l` and `u` between `α` and another preordered set `β`, `u` has a unique solution `b` in `β` for the equation `u(b) = a` if and only if `b = l(a)`.
|
GaloisConnection.u_eq_top
theorem GaloisConnection.u_eq_top :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderTop α] {l : α → β}
{u : β → α}, GaloisConnection l u → ∀ {x : β}, u x = ⊤ ↔ l ⊤ ≤ x
The theorem `GaloisConnection.u_eq_top` states that for any types `α` and `β`, with `α` being a partially ordered set and `β` being a preordered set, and `α` having a greatest element (`OrderTop α`), given two functions `l : α → β` and `u : β → α` that form a Galois Connection, for any element `x` of `β`, `u(x)` equals the greatest element of `α` if and only if `l` of the greatest element of `α` is less than or equal to `x`. In simpler terms, it states a condition under which the function `u` applied to any element gives the maximum element in a Galois connection.
More concisely: For any Galois connection between partially ordered set `α` with greatest element `OrderTop α` and preordered set `β`, `u(x) = OrderTop α` if and only if `l(OrderTop α) ≤ x`.
|
gc_sSup_Iic
theorem gc_sSup_Iic : ∀ {α : Type u} [inst : CompleteSemilatticeSup α], GaloisConnection sSup Set.Iic
This theorem states that for any type `α` that forms a complete semilattice with respect to the supremum operation, the supremum (`sSup`) and the function that defines a left-infinite right-closed interval (`Iic`) form a Galois Connection. Intuitively, this means that taking the supremum of a set of elements in `α` and considering all elements in `α` that are less than or equal to a certain element are operations that 'dual' to each other in a precise sense: any element of `α` is less than or equal to the supremum of a set if and only if that set is contained in the set of all elements less than or equal to the given element.
More concisely: For any complete semilattice `α` with supremum operation `sSup`, the functions `sSup : set α → α` and `Iic : α → set α` form a Galois connection.
|
GaloisCoinsertion.choice_eq
theorem GaloisCoinsertion.choice_eq :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
(self : GaloisCoinsertion l u) (a : β) (h : a ≤ l (u a)), self.choice a h = u a
This theorem, named `GaloisCoinsertion.choice_eq`, establishes a property of the choice function in the context of a Galois coinsertion. Specifically, for any two types `α` and `β` with a preorder relationship defined on both, and for any functions `l : α → β` and `u : β → α` forming a Galois coinsertion, the theorem states that for any element `a` of type `β` and for any proof `h` that `a` is less than or equal to `l (u a)`, the choice function applied to `a` and `h` equals `u a`. This theorem essentially relates the choice function to the upper adjoint `u` of the Galois coinsertion under certain conditions.
More concisely: For any Galois coinsertion `l : α → β` and `u : β → α` and for any `a : β` with `h : a ≤ l (u a)`, the choice function `choice` applied to `a` and `h` equals `u a`.
|
GaloisInsertion.u_injective
theorem GaloisInsertion.u_injective :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : PartialOrder β],
GaloisInsertion l u → Function.Injective u
The theorem `GaloisInsertion.u_injective` asserts that for any two types `α` and `β`, given the functions `l : α → β` and `u : β → α`, and assuming that `α` is a preordered set and `β` is a partially ordered set, if `l` and `u` form a Galois insertion, then the function `u` is injective. In other words, if `u` maps two elements of `β` to the same element of `α`, then these two elements of `β` must be the same. This is a property of Galois insertions in order theory.
More concisely: If `l : α → β` and `u : β → α` form a Galois insertion between preordered set `α` and partially ordered set `β`, then `u` is an injective function.
|
GaloisConnection.l_sup
theorem GaloisConnection.l_sup :
∀ {α : Type u} {β : Type v} {a₁ a₂ : α} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {l : α → β}
{u : β → α}, GaloisConnection l u → l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂
The theorem `GaloisConnection.l_sup` states that for any types `α` and `β` where `α` and `β` are both semilattices, and any elements `a₁` and `a₂` of type `α`, if a Galois connection exists between a function `l` from `α` to `β` and a function `u` from `β` to `α`, then the function `l` preserves the operation of taking supremum (join operation in semilattice), i.e., the value of `l` at the supremum of `a₁` and `a₂` is the same as the supremum of the values of `l` at `a₁` and `a₂`. In mathematical notation, this can be represented as `l(a₁ ⊔ a₂) = l(a₁) ⊔ l(a₂)`.
More concisely: For any semilattices types `α` and `β` and elements `a₁` and `a₂` in `α`, if there exists a Galois connection between functions `l: α → β` and `u: β → α`, then `l( sup a₁ a₂ ) = sup ( l(a₁) ) ( l(a₂) )`.
|
GaloisConnection.monotone_l
theorem GaloisConnection.monotone_l :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → Monotone l
The theorem `GaloisConnection.monotone_l` states that for any types `α` and `β` equipped with preorder structures, if a pair of functions `l : α → β` and `u : β → α` form a Galois connection, then the function `l` is monotone. In other words, if for all `a` in `α` and `b` in `β`, `l a` is less than or equal to `b` if and only if `a` is less than or equal to `u b`, then for all `a, b` in `α`, if `a` is less than or equal to `b`, then `l a` is less than or equal to `l b`.
More concisely: If `l` and `u` form a Galois connection between preordered types `α` and `β`, then `l` is a monotone function from `α` to `β`.
|
GaloisInsertion.l_sup_u
theorem GaloisInsertion.l_sup_u :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β],
GaloisInsertion l u → ∀ (a b : β), l (u a ⊔ u b) = a ⊔ b
This theorem states that for any two types `α` and `β`, a pair of functions `l : α → β` and `u : β → α`, and instances of semilattice structure (which means binary operation that is associative, commutative, idempotent, and has an order relation) on `α` and `β`, if `l` and `u` form a Galois insertion (a special relationship between `l` and `u` such that for all `a` in `α` and `b` in `β`, `l a ≤ b` iff `a ≤ u b`), then for any two elements `a` and `b` in `β`, the function `l` applied to the sup (the least upper bound operation, here denoted by `⊔`) of `u a` and `u b` is equal to the sup of `a` and `b`.
More concisely: For any semilattices `α` and `β` with a Galois connection between functions `l : α → β` and `u : β → α`, the sup of `l (a ⊔ b)` equals `l a ⊔ l b` for all elements `a, b` in `α`.
|
GaloisCoinsertion.strictMono_l
theorem GaloisCoinsertion.strictMono_l :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β],
GaloisCoinsertion l u → StrictMono l
The theorem `GaloisCoinsertion.strictMono_l` states that for any two types `α` and `β`, given two functions `l : α → β` and `u : β → α`, and provided that both `α` and `β` have a preorder relation, if there exists a Galois coinsertion between `l` and `u`, then the function `l` is strictly monotone. In other words, if `a < b` for any `a, b ∈ α`, then `l(a) < l(b)`.
More concisely: If types `α` and `β` have preorders, and there exists a Galois coinsertion between functions `l : α → β` and `u : β → α`, then `l` is a strictly increasing function.
|
GaloisConnection.l_unique
theorem GaloisConnection.l_unique :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] {l : α → β} {u : β → α},
GaloisConnection l u →
∀ {l' : α → β} {u' : β → α}, GaloisConnection l' u' → (∀ (b : β), u b = u' b) → ∀ {a : α}, l a = l' a
The theorem `GaloisConnection.l_unique` states that for any two pairs of functions `(l, u)` and `(l', u')` from a Preorder `α` to a PartialOrder `β` and vice versa, if both pairs form a Galois connection (i.e., for each `l a ≤ b` if and only if `a ≤ u b`, and the same holds with `l'` and `u'`), and the second functions of both pairs `u` and `u'` are equal for all `b` in `β`, then the first functions `l` and `l'` of these pairs are also equal for all `a` in `α`. In other words, given two Galois connections with the same right-adjoint, their left-adjoints are equal.
More concisely: If two Galois connection pairs between a preorder and a partial order have equal right-adjoint functions, then their left-adjoint functions are equal.
|
GaloisConnection.u_iInf
theorem GaloisConnection.u_iInf :
∀ {α : Type u} {β : Type v} {ι : Sort x} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {l : α → β}
{u : β → α}, GaloisConnection l u → ∀ {f : ι → β}, u (iInf f) = ⨅ i, u (f i)
The theorem `GaloisConnection.u_iInf` states that for any types `α`, `β`, and `ι`, given that `α` and `β` form complete lattices, and given a Galois connection between `α` and `β` defined by the functions `l` and `u`, then for any function `f` from `ι` to `β`, the application of `u` to the infimum over `f` is equal to the infimum over the application of `u` to `f(i)` for all `i` in `ι`. In other words, the function `u` distributes over the infimum of a set, transforming the infimum of the image set under `f` to the infimum of the image set under the composition of `u` and `f`.
More concisely: For any complete lattices α, β and a Galois connection between them defined by functions l and u, the application of u to the infimum over a function f from ι to β is equal to the infimum over the application of u to f(i) for all i in ι. In other words, u distributes over the infimum.
|
GaloisCoinsertion.u_inf_l
theorem GaloisCoinsertion.u_inf_l :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β],
GaloisCoinsertion l u → ∀ (a b : α), u (l a ⊓ l b) = a ⊓ b
This theorem, `GaloisCoinsertion.u_inf_l`, states that for any two types `α` and `β`, a function `l` from `α` to `β`, a function `u` from `β` to `α`, and given that `α` and `β` are both semilattice inf (i.e., they have an infimum operation), if `l` and `u` form a Galois coinsertion, then for any two elements `a` and `b` of type `α`, the infimum of `l a` and `l b` after applying `u` is equal to the infimum of `a` and `b`. In mathematical terms, this says that for all `a, b` in `α`, `u(l(a) ⊓ l(b)) = a ⊓ b` where `⊓` is the infimum operation.
More concisely: For any semilattices α and β, and Galois coinsertion functions l: α -> β and u: β -> α, the infimum of l(a) and l(b) under u is equal to the infimum of a and b in α. (That is, u(l(a) ∧ l(b)) = a ∧ b.)
|
GaloisCoinsertion.u_iSup_l
theorem GaloisCoinsertion.u_iSup_l :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
GaloisCoinsertion l u → ∀ {ι : Sort x} (f : ι → α), u (⨆ i, l (f i)) = ⨆ i, f i
This theorem states that, for any types `α` and `β`, functions `l : α → β` and `u : β → α`, and for any complete lattices over `α` and `β`, if there exists a Galois coinsertion between `l` and `u`, then for any function `f` indexed by some sort `ι`, the function `u` applied to the supremum (expressed by `⨆`) over `i` of `l` applied to `f i` equals the supremum over `i` of `f i`. In other words, the coinsertion property allows us to move the `u` function outside of the supremum.
More concisely: Given functions `l : α → β`, `u : β → α` between complete lattices `α` and `β`, if there exists a Galois coinsertion between `l` and `u`, then for any function `f : ι → α`, we have `u (⨆ i, l i (f i)) = ⨆ i, f i`.
|
GaloisConnection.l_iSup₂
theorem GaloisConnection.l_iSup₂ :
∀ {α : Type u} {β : Type v} {ι : Sort x} {κ : ι → Sort u_1} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
{l : α → β} {u : β → α},
GaloisConnection l u → ∀ {f : (i : ι) → κ i → α}, l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)
This theorem states that given a Galois connection (defined by function pairs `l` and `u`), for every function `f` mapping from a type `ι` to another type `κ`, which then maps to a type `α` in a complete lattice, the supremum (or least upper bound, denoted by ⨆) of the function `l` applied on `f` over all `i` and `j` is equal to the function `l` applied on the supremum of `f` over all `i` and `j`. This theorem is significant as it captures the preservation property of Galois connections across complete lattices with respect to the operation of taking supremums.
More concisely: Given a Galois connection `(l, u)` and a function `f` from a complete lattice `ι` to a type `α`, the supremum of `l ∘ f` over all `i` and `j` equals `l` applied to the supremum of `f` over all `i` and `j`.
|
GaloisCoinsertion.u_iInf_l
theorem GaloisCoinsertion.u_iInf_l :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
GaloisCoinsertion l u → ∀ {ι : Sort x} (f : ι → α), u (⨅ i, l (f i)) = ⨅ i, f i
This theorem states that for any two types `α` and `β`, given a pair of functions `l : α → β` and `u : β → α`, along with the assumption that `α` and `β` form complete lattices, if `l` and `u` form a Galois coinsertion, then for any index set `ι` and any family of elements `(f : ι → α)`, the value of applying `u` to the infimum (greatest lower bound) over `ι` of `l(f i)` is the same as the infimum over `ι` of `f i`. In mathematical terms, it says that the function `u` commutes with the operation of taking infima in the context of a Galois coinsertion.
More concisely: Given types `α` and `β` that form complete lattices, if functions `l : α → β` and `u : β → α` form a Galois coinsertion, then for any indexed family `(f : ι → α)`, `inf (map l (ι → α) f) = inf (list ι) (map (u ∘) (ι → α) f)`.
|
GaloisInsertion.l_iInf_u
theorem GaloisInsertion.l_iInf_u :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
GaloisInsertion l u → ∀ {ι : Sort x} (f : ι → β), l (⨅ i, u (f i)) = ⨅ i, f i
This theorem states that for any types `α` and `β`, and for any functions `l : α → β` and `u : β → α`, given that the pair `(l, u)` forms a Galois Insertion and that `α` and `β` are both complete lattices, then for any function `f : ι → β` (where `ι` is any type), the lower bound (infimum) of the image of `f` under `u`, after being transformed by `l`, returns the infimum of `f`. In mathematical terms, if `l` and `u` form a Galois Insertion and `α`, `β` are complete lattices, then we have `l (inf i, u (f i)) = inf i, f i`.
More concisely: Given a Galois connection between complete lattices `α` and `β` via functions `l : α → β` and `u : β → α`, the infimum of the composition `l (inf i, u (f i))` equals the infimum of `f` for any function `f : ι → β`.
|
GaloisConnection.lt_iff_lt
theorem GaloisConnection.lt_iff_lt :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {a : α} {b : β}, b < l a ↔ u b < a
The theorem `GaloisConnection.lt_iff_lt` states that for any types `α` and `β` with a linear order, given a Galois connection between `α` and `β` defined by functions `l` and `u`, for all elements `a` of type `α` and `b` of type `β`, `b` is less than `l a` if and only if `u b` is less than `a`. This theorem essentially extends the property of a Galois connection to the strict less than relation, in addition to the less than or equal to relation.
More concisely: For any types with a linear order and a Galois connection between them, the elements are related by strict order in one direction if and only if they are related by the opposite orders in the other direction. (Specifically, `b < l a` if and only if `u b < a`.)
|
GaloisConnection.upperBounds_l_image
theorem GaloisConnection.upperBounds_l_image :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ (s : Set α), upperBounds (l '' s) = u ⁻¹' upperBounds s
This theorem states that for any two types `α` and `β` that have a preorder relation, and for any pair of functions `l : α → β` and `u : β → α` that form a Galois Connection, the set of upper bounds of the image of a set `s` under the function `l` equals the preimage of the set of upper bounds of `s` under the function `u`. In other words, if you apply `l` to each element of `s` and then find all upper bounds of the resulting set in `β`, you will get the same set as if you first find all upper bounds of `s` in `α` and then apply `u` to each of them.
More concisely: For any preorder (α, ≤) and functions l : α → β and u : β → α forming a Galois connection, the upper bounds of the image of a set s under l equals the preimage of the set of upper bounds of s under u. In other words, (∃ x : β. ∀ y ∈ s. l y ≤ x) iff ∃ x' : α. ∀ y ∈ s. y ≤ u x'.
|
GaloisCoinsertion.u_l_leftInverse
theorem GaloisCoinsertion.u_l_leftInverse :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder α] [inst_1 : Preorder β],
GaloisCoinsertion l u → Function.LeftInverse u l
This theorem, `GaloisCoinsertion.u_l_leftInverse`, states that for any two types `α` and `β` along with functions `l : α → β` and `u : β → α`, given a partial order on `α` and a preorder on `β`, if a Galois coinsertion exists between `l` and `u`, then `u` is a left inverse to `l`. In other words, applying `u` after `l` gives the original input, i.e., for all `x` in `α`, we have `u(l(x)) = x`.
More concisely: If functions `l : α → β` and `u : β → α` have a Galois coinsertion and `α` is partially ordered, then `u` is a left inverse of `l`, that is, `u (l(x)) = x` for all `x` in `α`.
|
GaloisConnection.le_iff_le
theorem GaloisConnection.le_iff_le :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {a : α} {b : β}, l a ≤ b ↔ a ≤ u b
The theorem `GaloisConnection.le_iff_le` states that for any two types `α` and `β` that have a preorder (a reflexive and transitive binary relation), and any two functions `l : α → β` and `u : β → α`, if a Galois connection is established between `l` and `u`, then for all elements `a` of type `α` and `b` of type `β`, `l a` is less than or equal to `b` if and only if `a` is less than or equal to `u b`. In other words, the condition `l a ≤ b` is equivalent to `a ≤ u b` under the Galois connection between `l` and `u`.
More concisely: For any preorders (reflexive and transitive relations) on types `α` and `β`, and given functions `l : α → β` and `u : β → α` defining a Galois connection, `l(a) ≤ b` if and only if `a ≤ u(b)` for all `α` elements `a` and `β` elements `b`.
|
OrderIso.to_galoisConnection
theorem OrderIso.to_galoisConnection :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (oi : α ≃o β),
GaloisConnection ⇑oi ⇑oi.symm
The theorem `OrderIso.to_galoisConnection` establishes that for any given order-preserving bijection `oi` between two types `α` and `β`, which are both preordered, there exists a Galois connection. Specifically, the Galois connection is established between the function `oi` and the inverse function of `oi`, represented by `OrderIso.symm oi`. This means that for any elements `a` from `α` and `b` from `β`, `oi a` is less than or equal to `b` if and only if `a` is less than or equal to the inverse of `oi` applied to `b`.
More concisely: Given an order-preserving bijection between two preordered types `α` and `β`, there exists a Galois connection between the function and its inverse. Specifically, for all `a : α` and `b : β`, `a ≤ oi⁻¹(b)` if and only if `oi(a) ≤ b`.
|
GaloisConnection.l_iSup
theorem GaloisConnection.l_iSup :
∀ {α : Type u} {β : Type v} {ι : Sort x} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {l : α → β}
{u : β → α}, GaloisConnection l u → ∀ {f : ι → α}, l (iSup f) = ⨆ i, l (f i)
The theorem `GaloisConnection.l_iSup` states that for all types `α`, `β`, and `ι`, given `α` and `β` are complete lattices, and provided a Galois connection between functions `l : α → β` and `u : β → α`, for any function `f : ι → α`, the function `l` applied to the indexed supremum of `f` is equal to the supremum over `ι` of `l` applied to `f(i)`. In other words, the `l` function distributes over the indexed supremum.
More concisely: For any complete lattices α and β, and a Galois connection between functions l : α → β and u : β → α, the supremum of l o f over an indexed family f : ι → α equals l (supremum of f over ι), where supremum denotes the indexed supremum.
|
GaloisInsertion.isGLB_of_u_image
theorem GaloisInsertion.isGLB_of_u_image :
∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β],
GaloisInsertion l u → ∀ {s : Set β} {a : α}, IsGLB (u '' s) a → IsGLB s (l a)
This theorem states that for any types `α` and `β`, any functions `l : α → β` and `u : β → α`, and any set `s` of type `β`, if `l` and `u` form a Galois insertion with respect to the given preorders on `α` and `β`, and if `a` is a greatest lower bound of the image of `s` under `u`, then `l a` is a greatest lower bound of `s`. A Galois insertion is a pair of functions that describe an order-theoretic relationship between two partially ordered sets. The theorem is essentially stating a property about how greatest lower bounds translate across this Galois insertion.
More concisely: Given a Galois insertion between types `α` and `β` via functions `l : α → β` and `u : β → α`, if `s` is a set of type `β` with greatest lower bound `a` in `β`, then `l a` is the greatest lower bound of `s` in `α`.
|