Monotone.map_ciSup_of_continuousAt
theorem Monotone.map_ciSup_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
[inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β]
[inst_4 : TopologicalSpace β] [inst_5 : OrderClosedTopology β] [inst_6 : Nonempty γ] {f : α → β} {g : γ → α},
ContinuousAt f (⨆ i, g i) → Monotone f → BddAbove (Set.range g) → f (⨆ i, g i) = ⨆ i, f (g i)
The theorem `Monotone.map_ciSup_of_continuousAt` states that for any types `α`, `β`, and `γ` equipped with the appropriate topological and order structures, and given a nonempty type `γ`, if we have a monotone function `f` from `α` to `β` and another function `g` from `γ` to `α`, and if `f` is continuous at the supremum (least upper bound) of `g` over all of `γ`, and the range of function `g` is bounded above, then `f` takes this supremum to the supremum of the composition `f ∘ g`. In other words, the supremum of the composed function `f(g(i))` for all `i` in `γ` is the same as `f` applied to the supremum of `g(i)` for all `i` in `γ`. It shows the interaction of continuity and monotonicity with respect to the operation of taking supremum in ordered topological spaces.
More concisely: Given a monotone, continuous-at-the-supremum function `f` from `α` to `β`, and a function `g` from a nonempty, bounded-above `γ` to `α`, the supremum of `f ∘ g` over `γ` equals `f` applied to the supremum of `g` over `γ`.
|
Monotone.map_iSup_of_continuousAt
theorem Monotone.map_iSup_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {ι : Sort u_4} {f : α → β} {g : ι → α},
ContinuousAt f (iSup g) → Monotone f → f ⊥ = ⊥ → f (⨆ i, g i) = ⨆ i, f (g i)
This theorem states that if we have a function `f` which is monotone (meaning that if `a ≤ b` then `f(a) ≤ f(b)`) and sends the bottom element (`bot`) to bottom, and if this function is continuous at the supremum (`iSup`) of some indexed function `g` over a certain sort `ι`, then `f` sends this supremum to the supremum of the composition of `f` and `g`. In other words, applying `f` to the supremum of values generated by `g` (denoted as `⨆ i, g i`) yields the same result as taking the supremum of the values generated by applying `f` to each value of `g` (denoted as `⨆ i, f (g i)`). The theorem requires the preconditions that the types `α` and `β` are both complete linear orders and topological spaces, and that `β` has an order-closed topology.
More concisely: If `f` is a monotone, continuous function from a complete linear order and topological space `α` to another complete linear order and topological space `β` with order-closed topology, such that `f(bot) = bot`, then `f(⨆ i, g i) = ⨆ i, f(g i)`, where `g` is a function from `ι` to `α`.
|
Monotone.map_iInf_of_continuousAt'
theorem Monotone.map_iInf_of_continuousAt' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {ι : Sort u_4} [inst_6 : Nonempty ι] {f : α → β} {g : ι → α},
ContinuousAt f (iInf g) → Monotone f → autoParam (BddBelow (Set.range g)) _auto✝ → f (⨅ i, g i) = ⨅ i, f (g i)
This theorem states that for a monotone function `f` from one conditionally complete linear order type `α` to another `β`, that is continuous at the indexed lower bound (infimum) of a nonempty `Sort` `ι` indexed function `g`, if the range of `g` is bounded below (with an automatic parameter that does not affect elaboration), then applying `f` to the infimum over `ι` of `g`, equals to the infimum over `ι` of the composition of `f` and `g`.
In mathematical terms, if `f` is a monotone function and is continuous at the infimum of function `g` over some indexing set `ι`, and if the range of `g` has a lower bound, then the image under `f` of the infimum of `g` is equal to the infimum of the function `f(g)`, i.e., `f(inf(g)) = inf(f(g))`.
More concisely: If `f` is a monotone, continuous function from a conditionally complete linear order type `α` to another `β`, and `g` is an `Sort` `ι`-indexed function with bounded below range, then `f(inf(g)) = inf(f . g)`.
|
Antitone.map_iSup_of_continuousAt'
theorem Antitone.map_iSup_of_continuousAt' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {ι : Sort u_4} [inst_6 : Nonempty ι] {f : α → β} {g : ι → α},
ContinuousAt f (iSup g) → Antitone f → autoParam (BddAbove (Set.range g)) _auto✝ → f (⨆ i, g i) = ⨅ i, f (g i)
This theorem states that given a conditionally complete linearly ordered topological space `α`, another conditionally complete linearly ordered space `β` equipped with a topological structure, a nonempty `Sort` indexed collection of elements of `α`, a function `f` from `α` to `β`, and a function `g` from `Sort` to `α`, if `f` is continuous at the supremum (`iSup`) of `g` and `f` is antitone (meaning that `f` decreases or remains constant as its argument increases), then provided the range of `g` is bounded above (which is automatically inferred), the image under `f` of the supremum of `g` equals the infimum of the images under `f` of the elements of `g`. This is denoted mathematically as `f (⨆ i, g i) = ⨅ i, f (g i)`. This result essentially conveys that antitone functions reverse the order of supremums and infimums under certain conditions.
More concisely: If `α` and `β` are conditionally complete linearly ordered topological spaces, `f: α → β` is a continuous, antitone function, and `g: Sort → α` has a bounded above range, then `f (⨆ i, g i) = ⨅ i, f (g i)`.
|
Antitone.map_iInf_of_continuousAt
theorem Antitone.map_iInf_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {ι : Sort u_4} {f : α → β} {g : ι → α},
ContinuousAt f (iInf g) → Antitone f → f ⊤ = ⊥ → f (iInf g) = iSup (f ∘ g)
This theorem states that, given a complete linear order `α`, a topological space structure on `α`, an order topology on `α`, a complete linear order `β`, a topological space structure on `β`, an order closed topology on `β`, an index of sort `ι`, and functions `f : α → β` and `g : ι → α`, if function `f` is continuous at the indexed infimum of function `g`, and `f` is an antitone function (a function where if `a ≤ b` then `f(b) ≤ f(a)`), and `f` of the greatest element of `α` equals the least element of `β`, then the value of function `f` at the indexed infimum of function `g` equals the indexed supremum of the composition of functions `f` and `g`. In mathematical terms, if `f` is continuous at $\inf_{i \in I} g(i)$, antitone, and $f(\top) = \bot$, then the theorem states that $f(\inf_{i \in I} g(i)) = \sup_{i \in I} (f \circ g)(i)$.
More concisely: If `f : α → β` is a continuous, antitone function with `f(⊤) = ⊥`, then `f(⨅ i ∈ I (gi)) = ⨆ i ∈ I (f ∘ gi)`. Here, `α` and `β` are complete linear orders with order topologies, `I` is an index set, `gi` are functions from `I` to `α`, `⊤` is the greatest element of `α`, `⊥` is the least element of `β`, and `⨅` and `⨆` denote indexed infima and suprema, respectively.
|
Antitone.map_sInf_of_continuousAt
theorem Antitone.map_sInf_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {s : Set α},
ContinuousAt f (sInf s) → Antitone f → f ⊤ = ⊥ → f (sInf s) = sSup (f '' s)
This theorem states that for every antitone function 'f' mapping the top element to the bottom element and is continuous at the infimum of a set 's', it will map the infimum of 's' to the supremum of the image of 's'. This is true given that 'α' and 'β' are types with complete linear order, 'α' is a topological space with order topology, and 'β' is a topological space with order-closed topology. The antitone property of 'f' means that whenever 'a' is less than or equal to 'b', 'f(b)' is less than or equal to 'f(a)', and the continuity of 'f' at the infimum of 's' means that as we approach the infimum of 's', the function values approach 'f' evaluated at the infimum of 's'.
More concisely: For every antitone (order-reversing and monotonic), continuous function $f$ from a complete lattice $(A, \leq)$ with top element $\top$ and bottom element $\bot$, where $A$ is a topological space with order topology, and $\beta$ is a topological space with order-closed topology, maps the infimum of $A$ to the supremum of $f(A)$.
|
Antitone.map_csInf_of_continuousAt
theorem Antitone.map_csInf_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {s : Set α},
ContinuousAt f (sInf s) → Antitone f → s.Nonempty → BddBelow s → f (sInf s) = sSup (f '' s)
This theorem states that if we have an antitone function `f` (meaning that if `a ≤ b`, then `f(b) ≤ f(a)`) that is also continuous at the infimum (greatest lower bound) of a nonempty set `s` which is bounded below, then applying this function to the infimum of `s` results in the supremum (least upper bound) of the image of `s` under `f`. In mathematical terms, if `f` is antitone and continuous at `inf(s)`, then `f(inf(s)) = sup(f(s))`. Here, `inf` represents the infimum, `sup` represents the supremum, and `f(s)` is the set of all the images of elements of `s` under `f`. The theorem applies to any types `α` and `β` that are equipped with a conditionally complete linear order and a topological space structure such that the order topology is closed.
More concisely: If `f` is an antitone and continuous function between complete lattice-ordered topological spaces `α` and `β`, then `f(inf(s)) = sup(f(s))` for any nonempty `s ⊆ α` bounded below.
|
Monotone.tendsto_nhdsWithin_Ioi
theorem Monotone.tendsto_nhdsWithin_Ioi :
∀ {α : Type u_4} {β : Type u_5} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β]
{f : α → β}, Monotone f → ∀ (x : α), Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioi x)))
This theorem states that, for any given point `x`, a monotone mapping `f` (from a linear ordered space `α` to a conditionally complete linear ordered space `β`, both with their respective topologies and order topologies) has a limit within the open interval to the right of `x` that tends to the greatest lower bound (infimum or `sInf`) of the image of the interval under the function `f`. In other words, as we consider points in `α` increasingly larger than `x`, the corresponding `f` values approach the smallest `f` value that is larger than `f(x)`.
More concisely: For any monotone function `f` from a linearly ordered space `α` to a conditionally complete linearly ordered space `β`, and any point `x` in `α`, there exists a limit of `f` within the open interval to the right of `x` equal to the infimum of the image of that interval under `f`.
|
Monotone.map_csSup_of_continuousAt
theorem Monotone.map_csSup_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {s : Set α},
ContinuousAt f (sSup s) → Monotone f → s.Nonempty → BddAbove s → f (sSup s) = sSup (f '' s)
The theorem `Monotone.map_csSup_of_continuousAt` states that for any nonempty set `s` which is bounded above, if a function `f` is both monotone and continuous at the supremum of `s`, then the value of `f` at the supremum of `s` is equal to the supremum of the image of `s` under `f`. In other words, the function `f` maps the supremum of `s` to the supremum of the image of `s`. This theorem applies under the conditions that `α` and `β` are conditionally complete linear orders (meaning every nonempty set bounded above has a supremum and every nonempty set bounded below has an infimum), `α` and `β` are topological spaces, the order topology is defined on `α`, and the order closed topology is defined on `β`.
More concisely: If `s` is a nonempty, bounded above set in a conditionally complete linear order `α`, and `f` is a monotone and continuous function from `α` to another conditionally complete linear order `β` with order topology and order-closed topology, then `f` maps the supremum of `s` to the supremum of `f``(s)`.
|
Monotone.map_sInf_of_continuousAt'
theorem Monotone.map_sInf_of_continuousAt' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {A : Set α},
ContinuousAt f (sInf A) → Monotone f → A.Nonempty → autoParam (BddBelow A) _auto✝ → f (sInf A) = sInf (f '' A)
This theorem states that for any two types `α` and `β`, if `α` has the structure of a conditionally complete linear order and a topological space with an order topology, and `β` also has the structure of a conditionally complete linear order and a topological space with an order-closed topology, then for any function `f` from `α` to `β` and any set `A` of type `α`, if the function `f` is continuous at the infimum of the set `A`, and `f` is a monotone function, and the set `A` is nonempty and bounded below (which is assumed implicitly), then the image of the infimum of `A` under `f` equals the infimum of the image of `A` under `f`. In mathematical terms, if `f` is continuous and monotone, `f(inf A) = inf f(A)` for a nonempty set `A` that is bounded below.
More concisely: If `f` is a continuous and monotone function between two conditionally complete linear orders `α` and `β`, where `α` and `β` are also topological spaces with order topologies and order-closed topologies, respectively, then the infimum of `f(A)` equals `f(inf A)` for any nonempty and bounded below set `A` in `α`.
|
Monotone.tendsto_nhdsWithin_Iio
theorem Monotone.tendsto_nhdsWithin_Iio :
∀ {α : Type u_4} {β : Type u_5} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β]
{f : α → β}, Monotone f → ∀ (x : α), Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Iio x)))
This theorem asserts that for any given point `x` and a function `f` that is monotone (meaning if `a ≤ b` then `f(a) ≤ f(b)`), the function `f` has a limit to the left of `x`, which is equal to the supremum (`sSup`) of the image of the function `f` over the left-open interval up to `x` (`Iio x`). Here, `Filter.Tendsto` describes the limit of the function, `nhdsWithin` describes the neighborhood within a set, and `nhds` indicates the neighborhood filter around a given point. The set `Iio x` represents all elements less than `x`. So, in simpler terms, the theorem says that for a function that is increasing, the limit of the function as it approaches any point from the left (or lower values) is the greatest value that the function takes on for inputs less than that point.
More concisely: For a monotone function `f`, the left limit of `f` at a point `x` equals the supremum of `f` over the left-open interval around `x`.
|
Antitone.map_ciSup_of_continuousAt
theorem Antitone.map_ciSup_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
[inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β]
[inst_4 : TopologicalSpace β] [inst_5 : OrderClosedTopology β] [inst_6 : Nonempty γ] {f : α → β} {g : γ → α},
ContinuousAt f (⨆ i, g i) → Antitone f → BddAbove (Set.range g) → f (⨆ i, g i) = ⨅ i, f (g i)
The theorem states that if we have an antitone function `f` (a function which reverses the order) that is continuous at the supremum (greatest element) of another function `g` indexed over some nonempty type `γ`, and if the range of `g` is bounded above, then `f` maps the supremum of `g` to the infimum (smallest element) of the composition of `f` and `g`. This is expressed in terms of conditions on three types `α`, `β`, and `γ`. Both `α` and `β` are assumed to be conditionally complete linear orders (that is, all nonempty bounded subsets have suprema and infima) and topological spaces in which the order topology is closed. The condition of the continuity of `f` is expressed in terms of the topology on `α`.
More concisely: If `f: α → β` is an antitone, continuous function at the supremum of the bounded above function `g: γ → α`, then `f(sup(g)) = inf(f ∘ g)`.
|
Antitone.map_iSup_of_continuousAt
theorem Antitone.map_iSup_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {ι : Sort u_4} {f : α → β} {g : ι → α},
ContinuousAt f (iSup g) → Antitone f → f ⊥ = ⊤ → f (⨆ i, g i) = ⨅ i, f (g i)
This theorem states that if we have an anti-monotone function `f` that maps the bottom (`bot`) element of the domain (a complete linear order `α`) to the top (`top`) element of the codomain (another complete linear order `β`), and this function is continuous at the indexed supremum (`iSup`) of a function `g` (that ranges over an arbitrary sort `ι`), then `f` maps this indexed supremum to the indexed infimum (`⨅ i, f (g i)`) of the function composition. In other words, `f` transforms the greatest upper bound of `g`'s output into the smallest lower bound in the image of `f` composed with `g`. This theorem combines notions from both topology (continuity and order topology) and order theory (anti-monotone property, supremum and infimum).
More concisely: If `f` is an anti-monotone, continuous function mapping the bottom element of a complete linear order to the top element of another complete linear order, then `f` transforms the supremum of `g` to the infimum of `f ∘ g`.
|
Monotone.map_sSup_of_continuousAt'
theorem Monotone.map_sSup_of_continuousAt' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {A : Set α},
ContinuousAt f (sSup A) → Monotone f → A.Nonempty → autoParam (BddAbove A) _auto✝ → f (sSup A) = sSup (f '' A)
This theorem states that if you have a monotone function `f` that is also continuous at the supremum (`sSup`) of a nonempty set `A`, then the value of `f` at the `sSup` of `A` is equal to the `sSup` of the image of `A` under `f`. This essentially means that the function `f` is mapping the supremum of `A` to the supremum of its image. Additionally, it is assumed that the set `A` is bounded above, but this is an automatic parameter which Lean fills in on its own, without requiring explicit specification. The theorem applies in the context of conditionally complete linear orders and topological spaces where the order topology is derived from the linear order and the topology is closed under limit of sequences decreasing to a limit.
More concisely: If `f` is a monotone and continuous function on a nonempty, bounded above set `A` in a conditionally complete linear order or topological space, then `f(sSup A) = sSup (f ``A``)`.
|
Monotone.map_sSup_of_continuousAt
theorem Monotone.map_sSup_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {s : Set α},
ContinuousAt f (sSup s) → Monotone f → f ⊥ = ⊥ → f (sSup s) = sSup (f '' s)
The theorem `Monotone.map_sSup_of_continuousAt` states that for all types `α` and `β`, given the conditions that `α` and `β` are complete linear orders, `α` is a topological space with an order topology, and `β` is a topological space with an order-closed topology, if `f` is a monotone function from `α` to `β` that sends `bot` (the least element) to `bot`, and is continuous at the supremum of a set `s` of elements in `α`, then `f` sends the supremum of the set `s` to the supremum of the image of `s` under `f`.
In simpler terms, a monotone function that is continuous at the maximum value of a set will map this maximum value to the maximum value of the set of output values.
More concisely: For monotone functions `f` from a complete linear order `α` (with order topology) to a topological space `β` (with order-closed topology), if `f` is continuous at the supremum of a set `s` in `α` and sends the least element to the least element, then `f` maps the supremum of `s` to the supremum of `f``(s)`.
|
Monotone.map_iSup_of_continuousAt'
theorem Monotone.map_iSup_of_continuousAt' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {ι : Sort u_4} [inst_6 : Nonempty ι] {f : α → β} {g : ι → α},
ContinuousAt f (iSup g) → Monotone f → autoParam (BddAbove (Set.range g)) _auto✝ → f (⨆ i, g i) = ⨆ i, f (g i)
The theorem `Monotone.map_iSup_of_continuousAt'` states that if you have a monotone function `f` from a conditionally complete linearly ordered topological space `α` to another such space `β`, and this function is continuous at the indexed supremum (or least upper bound) of a function `g` mapping from a nonempty `Sort` `ι` to `α` (denoted by `iSup g`), then `f` maps this supremum to the supremum of the function obtained by composing `f` and `g`. In mathematical notation, if `f` is monotone and is continuous at `sup g` (`sup` denotes the supremum), and the range of `g` is bounded above, then `f(sup g) = sup (f ∘ g)`. The `autoParam` is a Lean feature that automatically fills in some arguments during elaboration, in this case, a proof that the range of `g` is bounded above.
More concisely: If `f` is a monotone, continuous function from a conditionally complete linearly ordered topological space to another such space, and `g` is a function mapping a nonempty set to this space with bounded above range, then `f(sup g) = sup (f ∘ g)`.
|
Monotone.map_iInf_of_continuousAt
theorem Monotone.map_iInf_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {ι : Sort u_4} {f : α → β} {g : ι → α},
ContinuousAt f (iInf g) → Monotone f → f ⊤ = ⊤ → f (iInf g) = iInf (f ∘ g)
The theorem states that for any two types `α` and `β` which are complete linear orders with topological spaces, where the topological space has order topology for `α` and order closed topology for `β`, and a `Sort` index `ι`, if a function `f` from `α` to `β` is continuous at the infimum of a function `g` from `ι` to `α` and is monotone, and if `f` maps the top element of `α` to the top of `β`, then `f` maps the infimum of `g` to the infimum of the composition function `f ∘ g`.
In simple terms, under these conditions, the function `f` preserves the infimum of the function `g` when applied after `g`, even when the infimum is taken over the potentially infinite index `ι`.
More concisely: If `f: α → β` is a monotone, continuous function between complete linear orders `α` and `β` with order topologies, where `f` maps the top element of `α` to the top of `β`, then `f` preserves the infimum of any function `g: ι → α`, i.e., `f (��inf g) = ��inf (f ∘ g)`.
|
Monotone.map_ciInf_of_continuousAt
theorem Monotone.map_ciInf_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
[inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β]
[inst_4 : TopologicalSpace β] [inst_5 : OrderClosedTopology β] [inst_6 : Nonempty γ] {f : α → β} {g : γ → α},
ContinuousAt f (⨅ i, g i) → Monotone f → BddBelow (Set.range g) → f (⨅ i, g i) = ⨅ i, f (g i)
This theorem states that for three types `α`, `β`, and `γ`, given `α` and `β` are conditionally complete linear orders and both have topological structures, `α` has an order topology, `β` has an order closed topology, `γ` is nonempty, and given two functions `f : α → β` and `g : γ → α`, if `f` is continuous at the infimum (greatest lower bound) of the values of `g` and `f` is a monotone function, and the set of all values of `g` is bounded below, then the value of `f` at the infimum of the values of `g` is equal to the infimum of the values of `f` at each value of `g`. This effectively means that a continuous monotone function maps the infimum of a set of values to the infimum of its image, under the assumption that the original set of values is bounded below.
More concisely: If `α` and `β` are conditionally complete linear orders with topologies, `γ` is nonempty, `f : α → β` is a continuous, monotone function, and the set of `g : γ → α` has a bottom element, then `f` maps the infimum of `g` to the infimum of `f` over the values of `g`.
|
Antitone.map_sInf_of_continuousAt'
theorem Antitone.map_sInf_of_continuousAt' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {A : Set α},
ContinuousAt f (sInf A) → Antitone f → A.Nonempty → autoParam (BddBelow A) _auto✝ → f (sInf A) = sSup (f '' A)
This theorem states that for a function `f` from one topological space to another, if `f` is continuous at the infimum of a nonempty set `A` and `f` is an antitone function (a function where if `a` is less than or equal to `b`, then `f(b)` is less than or equal to `f(a)`), and `A` is bounded below, then the value of `f` at the infimum of `A` is equal to the supremum of the image of `A` under `f`. This conditionally holds for a complete linear order and a closed order topology in the domain and codomain. The autoParam function is used to provide an automatic parameter which doesn't affect the theorem but it helps during the proof elaboration.
More concisely: If `f` is a continuous, antitone function between complete linear orders with bounded below domains and codomains under closed order topologies, then `f` maps the infimum of the domain to the supremum of `f`'s image of the domain.
|
Antitone.map_iInf_of_continuousAt'
theorem Antitone.map_iInf_of_continuousAt' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {ι : Sort u_4} [inst_6 : Nonempty ι] {f : α → β} {g : ι → α},
ContinuousAt f (iInf g) → Antitone f → autoParam (BddBelow (Set.range g)) _auto✝ → f (⨅ i, g i) = ⨆ i, f (g i)
The theorem `Antitone.map_iInf_of_continuousAt'` states that for any type `α` with a conditionally complete linear order, a topological space structure and an order topology; any `β` with a conditionally complete linear order, a topological space structure and an order closed topology; a nonempty type `ι`, a function `f` from `α` to `β`, a function `g` from `ι` to `α`; if the function `f` is continuous at the indexed infimum of `g`, `f` is antitone and the range of `g` is bounded below, then the value of `f` at the infimum over `ι` of `g` equals the supremum over `ι` of the values of `f` at `g`. In other words, an antitone function, which is continuous at the infimum of a function `g`, maps this infimum to the supremum of the composition of `f` and `g`.
More concisely: If `f: α → β` is an antitone, continuous-at-infimum function between conditionally complete linear orders with order topologies, and `g: ι → α` has a bounded below range, then `f(⨶ i ∈ ι g i) = ⨆ i ∈ ι f(g i)`.
|
Monotone.map_sInf_of_continuousAt
theorem Monotone.map_sInf_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {s : Set α},
ContinuousAt f (sInf s) → Monotone f → f ⊤ = ⊤ → f (sInf s) = sInf (f '' s)
The theorem `Monotone.map_sInf_of_continuousAt` states that, given a monotone function `f` that maps the greatest element (designated as `⊤`) to the greatest element, and is continuous at the infimum (the greatest lower bound) of a set `s`, then `f` maps the infimum of the set `s` to the infimum of the image of set `s` under function `f`. This is under the conditions that `α` and `β` are both complete linear orders, `α` is a topological space with order topology and `β` is a topological space with order closed topology.
In other words, for a given set `s`, the function `f` takes the smallest element of `s` and maps it to the smallest element of the set created by applying `f` to every element of `s`. This holds true when `f` is a function that is continuous at the infimum of `s` and is order preserving, i.e., a monotone function.
More concisely: If `f` is a monotone function from a complete linear order `α` to another complete linear order `β`, continuous at the infimum of a set `s` in `α`, then `f` maps the infimum of `s` to the infimum of `f``(s)` in `β`.
|
Monotone.map_csInf_of_continuousAt
theorem Monotone.map_csInf_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {s : Set α},
ContinuousAt f (sInf s) → Monotone f → s.Nonempty → BddBelow s → f (sInf s) = sInf (f '' s)
The theorem states that if we have a function `f` from a conditionally complete linearly ordered topological space `α` to another such space `β`, and if this function is monotone and continuous at the infimum (greatest lower bound) of a nonempty set `s` that is bounded from below, then the function `f` maps the infimum of set `s` to the infimum of the image of set `s` under function `f`. This theorem connects the continuity and monotonicity of a function at the infimum of a set with the behaviour of the function on the infimum of the image of the set.
More concisely: If `f` is a monotone and continuous function from a conditionally complete linearly ordered topological space to another such space, and `s` is a nonempty, bounded from below set with an infimum in the domain of `f`, then `f` maps the infimum of `s` to the infimum of `f`'s image of `s`.
|
Antitone.map_sSup_of_continuousAt
theorem Antitone.map_sSup_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {s : Set α},
ContinuousAt f (sSup s) → Antitone f → f ⊥ = ⊤ → f (sSup s) = sInf (f '' s)
The theorem states that for a function `f` from one complete linear order `α` to another complete linear order `β`, both equipped with a topology that makes them topological spaces and that makes the order operations continuous (order topology for `α` and order closed topology for `β`), if `f` is antitone (i.e., it reverses the order), maps the bottom element of `α` to the top element of `β`, and is continuous at the supremum of a set `s` in `α`, then the value of `f` at the supremum of `s` is equal to the infimum of the image of `s` under `f` in `β`. In simpler terms, the theorem says that an order-reversing function that is continuous at a supremum sends the supremum to the infimum of the image of the set.
More concisely: If `f` is a continuous, antitone function from a complete lattice `(α, ∧, ∨, ⊥)` to another complete lattice `(β, ∧', ∨', ⊤)` with order topologies, where `∧` and `∨` are infima and suprema respectively, `⊥` is the bottom element, and `⊤` is the top element, then `f` maps the supremum of any set `s` to the infimum of the images of elements in `s`.
|
Antitone.map_sSup_of_continuousAt'
theorem Antitone.map_sSup_of_continuousAt' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {A : Set α},
ContinuousAt f (sSup A) → Antitone f → A.Nonempty → autoParam (BddAbove A) _auto✝ → f (sSup A) = sInf (f '' A)
The theorem states that if we have a function `f` from a topological space to another topological space that is anti-tone (meaning that if `a ≤ b` then `f(b) ≤ f(a)`) and is continuous at the supremum of a non-empty set `A`, then the function sends the supremum of `A` to the infimum of the image of `A` under `f`. This also requires that the set `A` is bounded above, a condition that is assumed to be automatically provided by the autoParam utility. In mathematical terms, if `f` is a continuous and anti-tone function, `A` is a non-empty set bounded above, and `sSup A` denotes the supremum of `A`, then `f(sSup A) = sInf(f(A))`, where `sInf(f(A))` stands for the infimum of the set of all images of elements of `A` under `f`.
More concisely: If `f` is a continuous and anti-tone function from a topological space to another, and `A` is a non-empty, bounded above set, then `f(sup A) = inf(f(x) | x ∈ A)`.
|
Antitone.map_csSup_of_continuousAt
theorem Antitone.map_csSup_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β]
[inst_5 : OrderClosedTopology β] {f : α → β} {s : Set α},
ContinuousAt f (sSup s) → Antitone f → s.Nonempty → BddAbove s → f (sSup s) = sInf (f '' s)
The theorem `Antitone.map_csSup_of_continuousAt` states that if you have an antitone function `f` (a function that reversely preserves the order between elements, i.e., if `a ≤ b`, then `f(b) ≤ f(a)`) that is continuous at the supremum of a nonempty set `s` that is bounded above (a set for which there exists an upper bound), then the value of the function `f` at the supremum of `s` is equal to the infimum (the greatest lower bound) of the image of the set `s` under the function `f`. In other words, the supremum of the original set is mapped to the infimum of its image under a continuous, antitone function. The theorem is valid in the context of conditionally complete linear orders and topological spaces equipped with an order topology, which is a topology induced by a linear order on a set.
More concisely: If `f` is an antitone, continuous function on a nonempty, bounded above set `s` in a conditionally complete linear order and topological space with order topology, then `f(⨝(s)) = ⨟(f[s])`, where `⨝(s)` is the supremum of `s` and `⨟(f[s])` is the infimum of the image of `s` under `f`.
|
Antitone.map_ciInf_of_continuousAt
theorem Antitone.map_ciInf_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
[inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β]
[inst_4 : TopologicalSpace β] [inst_5 : OrderClosedTopology β] [inst_6 : Nonempty γ] {f : α → β} {g : γ → α},
ContinuousAt f (⨅ i, g i) → Antitone f → BddBelow (Set.range g) → f (⨅ i, g i) = ⨆ i, f (g i)
This theorem states that for any types `α`, `β`, and `γ`, given `α` and `β` are conditionally complete linear orders and `α` and `β` are topological spaces with `α` having order topology and `β` having order closed topology, if `γ` is nonempty, then for any functions `f : α → β` and `g : γ → α`, if `f` is continuous at the greatest lower bound (infimum) of the set of values obtained by `g` and `f` is an antitone function (i.e., it reverses the order), and the set of values obtained by `g` is bounded below, then the value of `f` at the greatest lower bound of the set of values obtained by `g` equals the least upper bound (supremum) of the set of values obtained by applying `f` to each value in the set obtained by `g`. In mathematical terms, if `f` is continuous and antitone, then `f(inf{g(i) for all i in γ}) = sup{f(g(i)) for all i in γ}` under the assumption that `inf{g(i) for all i in γ}` exists.
More concisely: If `α`, `β`, and `γ` are types with `α` and `β` being conditionally complete linear orders and topological spaces, `α` having order topology and `β` having order closed topology, `γ` is nonempty, `f : α → β` is a continuous and antitone function, and the set of values obtained by `g : γ → α` is bounded below, then `f(inf(g(i) | i ∈ γ)) = sup(f(g(i)) | i ∈ γ)`.
|