OmegaCompletePartialOrder.Continuous.of_bundled'
theorem OmegaCompletePartialOrder.Continuous.of_bundled' :
∀ {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
(f : α →o β), OmegaCompletePartialOrder.Continuous f → OmegaCompletePartialOrder.Continuous' ⇑f
This theorem states that for any two types `α` and `β` endowed with the structures of omega complete partial orders, if a function `f` from `α` to `β` is a continuous function (as a bundled function in the sense of order theory), then it is also continuous in the sense of being both monotone and omega continuous. In other words, if a function preserves the order and is continuous in the order-theoretic sense, then it also has the property that it preserves the order and is continuous in the context of omega complete partial orders.
More concisely: If `α` and `β` are omega complete partial orders and `f` is a bundled continuous function from `α` to `β`, then `f` is both monotone and omega continuous.
|
CompleteLattice.sSup_continuous
theorem CompleteLattice.sSup_continuous :
∀ {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst_1 : CompleteLattice β] (s : Set (α →o β)),
(∀ f ∈ s, OmegaCompletePartialOrder.Continuous f) → OmegaCompletePartialOrder.Continuous (sSup s)
This theorem, named `CompleteLattice.sSup_continuous`, establishes that given two types, `α` and `β`, where `α` is an omega-complete partial order, and `β` is a complete lattice, for any set `s` of order-preserving maps from `α` to `β`, if every function `f` in `s` is continuous, then the supremum (or least upper bound) of the set `s`, denoted as `sSup s`, is also continuous. The continuity here is defined in the sense of the omega-complete partial order. Therefore, this theorem essentially states the preservation of continuity under the taking of suprema in the context of complete lattices and omega-complete partial orders.
More concisely: If `α` is an omega-complete partial order and `β` is a complete lattice, then the supremum of a set of order-preserving, continuous functions from `α` to `β` is itself continuous.
|
OmegaCompletePartialOrder.Chain.map_comp
theorem OmegaCompletePartialOrder.Chain.map_comp :
∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
(c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (g : β →o γ), (c.map f).map g = c.map (g.comp f)
The theorem `OmegaCompletePartialOrder.Chain.map_comp` states that for all types `α`, `β`, and `γ` that are preordered, and for any chain `c` in `α`, and any order preserving functions `f` from `α` to `β` and `g` from `β` to `γ`, mapping the chain `c` first by `f` and then by `g` (i.e., doing two consecutive mappings) is the same as first composing the functions `g` and `f` and then mapping the chain `c` by the composed function. This theorem therefore asserts the compatibility of the chain mapping operation with the function composition operation in the context of omega complete partial orders.
More concisely: For any chain in an omega complete preordered type `α`, and order preserving functions `f : α → β` and `g : β → γ`, the composition `g ∘ f` preserves the ordering between elements of the chain if and only if the chain application of `g` followed by the chain application of `f` also preserves the ordering.
|
OmegaCompletePartialOrder.ωSup_le
theorem OmegaCompletePartialOrder.ωSup_le :
∀ {α : Type u_1} [self : OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) (x : α),
(∀ (i : ℕ), c i ≤ x) → OmegaCompletePartialOrder.ωSup c ≤ x
The theorem `OmegaCompletePartialOrder.ωSup_le` states that for any type `α` equipped with a structure of an `OmegaCompletePartialOrder`, any chain `c` in `α`, and any member `x` of `α`, if every element of the chain `c` is less than or equal to `x`, then the ω-supremum (the supremum of the increasing sequence) of the chain `c` is less than or equal to `x`. In simpler terms, the supremum of the increasing sequence is a lower bound of the set of upper bounds of the increasing sequence.
More concisely: In an OmegaCompletePartialOrder, the ω-supremum of a chain is less than or equal to any upper bound of the chain.
|
OmegaCompletePartialOrder.continuous_comp
theorem OmegaCompletePartialOrder.continuous_comp :
∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : OmegaCompletePartialOrder α]
[inst_1 : OmegaCompletePartialOrder β] [inst_2 : OmegaCompletePartialOrder γ] (f : α →o β) (g : β →o γ),
OmegaCompletePartialOrder.Continuous f →
OmegaCompletePartialOrder.Continuous g → OmegaCompletePartialOrder.Continuous (g.comp f)
This theorem states that for any three types `α`, `β`, and `γ` that are instances of `OmegaCompletePartialOrder`, if we have two order homomorphisms `f` from `α` to `β` and `g` from `β` to `γ`, and both of these order homomorphisms are continuous, then the composition of `g` and `f` (given by `OrderHom.comp g f`) is also a continuous order homomorphism. In other words, the continuity property for order homomorphisms is preserved under function composition.
More concisely: If `f` is a continuous order homomorphism from `α` to `β` and `g` is a continuous order homomorphism from `β` to `γ`, then their composition `g ∘ f` is a continuous order homomorphism from `α` to `γ`.
|
Mathlib.Order.OmegaCompletePartialOrder._auxLemma.12
theorem Mathlib.Order.OmegaCompletePartialOrder._auxLemma.12 :
∀ {α : Type u} [inst : OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) (x : α),
(OmegaCompletePartialOrder.ωSup c ≤ x) = ∀ (i : ℕ), c i ≤ x
This theorem states that for any type `α` equipped with an Omega Complete Partial Order structure, any chain `c` of elements of type `α`, and any element `x` of type `α`, the condition that the supremum (ωSup) of the chain `c` is less than or equal to `x` is equivalent to the condition that every element of the chain `c` is less than or equal to `x`. In more mathematical terms, for all i in ℕ (the set of natural numbers), the i-th element of the chain `c` is less than or equal to `x`.
More concisely: For any Omega Complete Partial Order (OP) `α`, chain `c` in `α`, and `x` in `α`, `sup c <= x` if and only if `c.i <= x` for all `i` in `N`.
|
OmegaCompletePartialOrder.Continuous'.to_bundled
theorem OmegaCompletePartialOrder.Continuous'.to_bundled :
∀ {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (f : α → β)
(hf : OmegaCompletePartialOrder.Continuous' f),
OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := ⋯ }
The theorem `OmegaCompletePartialOrder.Continuous'.to_bundled` states that for all types `α` and `β` which are instances of `OmegaCompletePartialOrder`, and for any function `f` from `α` to `β` that is continuous in the sense of `OmegaCompletePartialOrder.Continuous'`, the function `f` can be bundled into an instance of `OmegaCompletePartialOrder.Continuous`. The function `f` in this context is both monotone and continuous according to the definition provided by `OmegaCompletePartialOrder.Continuous'`.
More concisely: For any continuous and monotone function `f` between two omega-complete partial orders `α` and `β`, `f` is an instance of `OmegaCompletePartialOrder.Continuous`.
|
OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge
theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge :
∀ {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
(c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) (z : β),
(∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
This theorem, for any types `α` and `β` that are endowed with an `OmegaCompletePartialOrder`, and for any chains `c₀` of continuous functions from `α` to `β`, `c₁` of elements of `α`, and a bound `z` in `β`, states that to show that every application of a function in the chain `c₀` to a value in the chain `c₁` is less than or equal to `z`, it is sufficient to show that the result of applying each function in `c₀` to the corresponding value (at the same index) in `c₁` is less than or equal to `z`. This theorem is more specific than necessary as it only needs `c₀` to be a chain of monotone functions, however it is only used with continuous functions.
More concisely: For any continuous chains of functions from an OmegaCompletePartialOrder to another and any corresponding elements in the ordering, if each function application is less than or equal to a bound, then every function application from the chain to the corresponding elements is also less than or equal to the bound.
|
OmegaCompletePartialOrder.Continuous'.to_monotone
theorem OmegaCompletePartialOrder.Continuous'.to_monotone :
∀ {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {f : α → β},
OmegaCompletePartialOrder.Continuous' f → Monotone f
The theorem `OmegaCompletePartialOrder.Continuous'.to_monotone` states that for all types `α` and `β`, given any function `f` that maps `α` to `β`, if `f` is continuous in the sense of the `OmegaCompletePartialOrder`, then `f` is also monotone. Here, a function is said to be continuous in the `OmegaCompletePartialOrder` if it is both monotone and continuous. Being monotone means that for any elements `a` and `b` in the domain, if `a` is less than or equal to `b`, then the value of the function at `a` is less than or equal to the value of the function at `b`.
More concisely: If a function between two types is continuous in the sense of an Omega Complete Partial Order, then it is monotone.
|
OmegaCompletePartialOrder.ContinuousHom.cont
theorem OmegaCompletePartialOrder.ContinuousHom.cont :
∀ {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
(self : α →𝒄 β), OmegaCompletePartialOrder.Continuous self.toOrderHom
This theorem states that for any two types `α` and `β` that are instances of `OmegaCompletePartialOrder`, the underlying function of a `ContinuousHom` from `α` to `β` is continuous, meaning it preserves the supremum (`ωSup`) of a directed set. Here, `ContinuousHom` is a type representing continuous homomorphisms between ordered algebraic structures, and `OmegaCompletePartialOrder` is a typeclass representing a complete partial order where every increasing sequence has a supremum.
More concisely: Given two types `α` and `β` instanced with `OmegaCompletePartialOrder`, the continuous homomorphism from `α` to `β` preserves suprema of directed sets.
|
OmegaCompletePartialOrder.Continuous.of_bundled
theorem OmegaCompletePartialOrder.Continuous.of_bundled :
∀ {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (f : α → β)
(hf : Monotone f),
OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf } → OmegaCompletePartialOrder.Continuous' f
This theorem states that for any types `α` and `β`, given that `α` and `β` are both Omega Complete Partial Orders, for any function `f` from `α` to `β` that is monotone (i.e., `a ≤ b` implies `f(a) ≤ f(b)`), if that function is continuous when bundled with its monotonicity proof, then that function is also `Continuous'` in the sense of the `OmegaCompletePartialOrder` class. Essentially, this theorem connects the bundled and unbundled definitions of a continuous function in the context of Omega Complete Partial Orders.
More concisely: If `f` is a monotone function from an Omega Complete Partial Order `α` to another Omega Complete Partial Order `β` and `f` is continuous when bundled with its monotonicity proof, then `f` is continuous in the sense of the `OmegaCompletePartialOrder` class.
|
OmegaCompletePartialOrder.ContinuousHom.monotone
theorem OmegaCompletePartialOrder.ContinuousHom.monotone :
∀ {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
(f : α →𝒄 β), Monotone ⇑f
This theorem states that for any types `α` and `β` that have an instance of `OmegaCompletePartialOrder`, any function `f` from `α` to `β` that is a continuous homomorphism (denoted as `α →𝒄 β`), is a monotone function. In other words, if `a` and `b` are elements of type `α` such that `a` is less than or equal to `b`, then the application of `f` to `a` (denoted as `f a` or `⇑f a`) is less than or equal to the application of `f` to `b` (denoted as `f b` or `⇑f b`).
More concisely: For any continuous homomorphism between two types with an OmegaCompletePartialOrder structure, the image of a smaller element is less than or equal to the image of a larger element.
|
OmegaCompletePartialOrder.ContinuousHom.continuous
theorem OmegaCompletePartialOrder.ContinuousHom.continuous :
∀ {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (F : α →𝒄 β)
(C : OmegaCompletePartialOrder.Chain α),
F (OmegaCompletePartialOrder.ωSup C) = OmegaCompletePartialOrder.ωSup (C.map ↑F)
This theorem is about the continuity of homomorphisms in the context of omega complete partial orders. It states that for all types `α` and `β`, which are both omega complete partial orders, and for a continuous homomorphism `F` from `α` to `β`, and a chain `C` in `α`, the application of `F` to the supremum of the chain `C` is equal to the supremum of the chain obtained by mapping `C` through `F`. In simpler terms, it asserts that continuous homomorphisms preserve the order-theoretic supremum of increasing sequences, which is a key property of continuity in the context of omega complete partial orders.
More concisely: For any omega complete partial orders `α` and `β`, and a continuous homomorphism `F` from `α` to `β`, if `C` is a chain in `α`, then `F(sup C) = sup (F '' C)`.
|
OmegaCompletePartialOrder.le_ωSup
theorem OmegaCompletePartialOrder.le_ωSup :
∀ {α : Type u_1} [self : OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) (i : ℕ),
c i ≤ OmegaCompletePartialOrder.ωSup c
This theorem states that for any chain `c` in a type `α` that is an `OmegaCompletePartialOrder`, the element at any index `i` of the chain `c` is less than or equal to the supremum of the chain `c`. In other words, the supremum function `ωSup` provides an upper bound for all elements of the increasing sequence defined by the chain.
More concisely: For any chain `c` in an `OmegaCompletePartialOrder` type `α`, the element `c.{i}` at index `i` of `c` is less than or equal to the supremum `ωSup c` of the chain.
|
OmegaCompletePartialOrder.le_ωSup_of_le
theorem OmegaCompletePartialOrder.le_ωSup_of_le :
∀ {α : Type u} [inst : OmegaCompletePartialOrder α] {c : OmegaCompletePartialOrder.Chain α} {x : α} (i : ℕ),
x ≤ c i → x ≤ OmegaCompletePartialOrder.ωSup c
This theorem states that for any type `α` that has an `OmegaCompletePartialOrder` structure, given a chain `c` from this type and an element `x` from the same type, if `x` is less than or equal to the `i`th element of the chain `c`, then `x` will also be less than or equal to the supremum of the chain `c`. Here, a chain is defined as a monotone (non-decreasing) sequence of elements from `α`, and the supremum of a chain is the least upper bound of all elements in that chain.
More concisely: For any chain `c` in an `OmegaCompletePartialOrder` type `α`, and any `x` in `α` less than or equal to the `i`th element of `c`, we have `x ≤ sup c`.
|