OrderHom.le_map_sSup_subset_fixedPoints
theorem OrderHom.le_map_sSup_subset_fixedPoints :
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), ∀ A ⊆ Function.fixedPoints ⇑f, sSup A ≤ f (sSup A) := by
sorry
The theorem `OrderHom.le_map_sSup_subset_fixedPoints` states that for any type `α` that forms a complete lattice and for any order-preserving function `f : α →o α`, if a subset `A` is contained within the set of fixed points of the function `f`, then the supremum (or least upper bound) of `A`, denoted `sSup A`, is less than or equal to the result of applying `f` to `sSup A`. In other words, `f` does not increase the supremum of any set of its fixed points.
More concisely: For any complete lattice `α` and order-preserving function `f : α → α`, if `A ⊆ fixedPoints f`, then `sSup A ≤ f (sSup A)`.
|
OrderHom.map_sInf_subset_fixedPoints_le
theorem OrderHom.map_sInf_subset_fixedPoints_le :
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), ∀ A ⊆ Function.fixedPoints ⇑f, f (sInf A) ≤ sInf A := by
sorry
This theorem states that for any type `α` that forms a complete lattice, and any order-preserving function `f : α → α`, if a set `A` is a subset of the fixed points of `f`, then the image of the infimum (`sInf`) of `A` under `f` is less than or equal to the infimum of `A`. In other words, if all elements of `A` are fixed points of `f`, `f` will map the infimum of `A` to a value that is less than or equal to the original infimum.
More concisely: For any complete lattice `α` and order-preserving function `f` on `α`, if `A ⊆ fixpoints(f)`, then `f(sInf A) ≤ sInf A`.
|
OrderHom.map_le_lfp
theorem OrderHom.map_le_lfp :
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, a ≤ OrderHom.lfp f → f a ≤ OrderHom.lfp f := by
sorry
The theorem `OrderHom.map_le_lfp` states that for any type `α` that forms a complete lattice, and for any monotone function `f : α → α`, if a certain element `a` of the type `α` is less than or equal to the least fixed point of the function `f` (denoted by `OrderHom.lfp f`), then the image of `a` under `f` (i.e., `f a`) is also less than or equal to the least fixed point of `f`. In other words, this theorem ensures the monotonicity property of the least fixed point operator with respect to the given monotone function `f`.
More concisely: For any complete lattice `α` and monotone function `f : α → α`, if `a ≤ OrderHom.lfp f`, then `f a ≤ OrderHom.lfp f`.
|
OrderHom.le_nextFixed
theorem OrderHom.le_nextFixed :
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x), x ≤ ↑(f.nextFixed x hx)
This theorem states that for any type `α` that forms a complete lattice, given a function `f` that is a monotone self-map on `α`, and a point `x` such that `x` is less than or equal to the image of `x` under `f`, then `x` is less than or equal to the next fixed point of `f` starting from `x`. In other words, it guarantees that the ordering of `x` and its next fixed point under the function `f` is preserved, which is a fundamental property in the study of monotone functions over complete lattices.
More concisely: For any complete lattice `α` and monotone self-map `f` on `α`, if `x` is in `α` and `x ≤ f(x)`, then `x ≤ f^(n+1)(x)` for some `n ∈ ℕ`. (Here, `f^n` denotes the `n`-th power of the function `f`.)
|
OrderHom.lfp_le
theorem OrderHom.lfp_le :
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, f a ≤ a → OrderHom.lfp f ≤ a
This theorem states that for any type `α` that forms a complete lattice, and for any order-preserving function `f` from `α` to `α`, if `f a` is less than or equal to `a` for some `a` in `α`, then the least fixed point of `f` is less than or equal to `a`. In other words, `a` is an upper bound of the least fixed point of the monotone function `f`.
More concisely: If `f` is an order-preserving function on a complete lattice `α` with `a` in `α` such that `f(a) ≤ a`, then the least fixed point of `f` is less than or equal to `a`.
|
OrderHom.nextFixed_le
theorem OrderHom.nextFixed_le :
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) {y : ↑(Function.fixedPoints ⇑f)},
x ≤ ↑y → f.nextFixed x hx ≤ y
This theorem states that for all types `α` forming a complete lattice, and for any monotone function `f` from `α` to `α`, given `x` in `α` such that `x` is less than or equal to `f(x)`, and a fixed point `y` of `f`, if `x` is less than or equal to `y`, then the next fixed point of `f` that is greater than or equal to `x` is less than or equal to `y`. In other words, if `x` is less than or equal to a fixed point `y`, then the smallest fixed point of `f` that is greater than or equal to `x` is also less than or equal to `y`.
More concisely: Given a complete lattice `α`, a monotone function `f` from `α` to `α`, a fixed point `y` of `f`, and `x` in `α` with `x ≤ y` and `x ≤ f(x)`, the next fixed point of `f` greater than or equal to `x` is less than or equal to `y`.
|
OrderHom.map_lfp
theorem OrderHom.map_lfp :
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), f (OrderHom.lfp f) = OrderHom.lfp f
This theorem states that for any type `α` that forms a complete lattice and any order-preserving function `f : α →o α`, the function `f` maps the least fixed point of `f` to itself. In other words, if we apply `f` to the least fixed point of `f`, we still get the least fixed point of `f`. This is essentially asserting that the least fixed point of a monotone function is a fixed point of the function itself. In mathematical terms, for a monotone function `f`, we have `f(lfp(f)) = lfp(f)`, where `lfp(f)` is the least fixed point of `f`.
More concisely: If `f : α → α` is a monotone function on a complete lattice `α`, then the least fixed point of `f` is a fixed point of `f`. (i.e., `lfp(f) = fixpoint(f)`)
|
OrderHom.le_map_sup_fixedPoints
theorem OrderHom.le_map_sup_fixedPoints :
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x y : ↑(Function.fixedPoints ⇑f)), ↑x ⊔ ↑y ≤ f (↑x ⊔ ↑y)
The theorem `OrderHom.le_map_sup_fixedPoints` states that for any complete lattice `α`, an order-preserving function `f` mapping `α` to `α`, and any two elements `x` and `y` in the set of fixed points of `f`, the join (or supremum) of `x` and `y` is less than or equal to the image of their join under `f`. In other words, for fixed points in a complete lattice, `f` preserves the order when applied to their supremum.
More concisely: For any complete lattice α and order-preserving function f: α → α, if x and y are fixed points, then f(sup x y) ≤ sup (fx) (fy).
|