Continuous.IccExtend
theorem Continuous.IccExtend :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace γ] {a b : α}
{h : a ≤ b} [inst_2 : TopologicalSpace α] [inst_3 : OrderTopology α] [inst_4 : TopologicalSpace β]
{f : γ → ↑(Set.Icc a b) → β} {g : γ → α},
Continuous ↿f → Continuous g → Continuous fun a_1 => Set.IccExtend h (f a_1) (g a_1)
The theorem `Continuous.IccExtend` states that for any types `α`, `β`, and `γ` where `α` has a linear order and `α`, `β`, `γ` each have a topological space structure, and `α` has an order topology, given any two continuous functions `f : γ → ↑(Set.Icc a b) → β` and `g : γ → α` (where `Set.Icc a b` denotes the closed interval from `a` to `b` and `a ≤ b`), the function that maps each element `a_1` of type `γ` to the extension of `f a_1` from the interval `[a, b]` to `β` at the point `g(a_1)` in `α` is also continuous. In other words, this theorem provides a condition under which the extension of a function on a closed interval to arbitrary points in the domain remains continuous.
More concisely: If `α` is a type with a linear order and topology, and `β`, `γ` are types with topologies, `f : γ → α → β` and `g : γ → α` are continuous, then the function that extends `f` at each point `g(a)` in `α` is continuous.
|
Continuous.Icc_extend'
theorem Continuous.Icc_extend' :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} {h : a ≤ b} [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : TopologicalSpace β] {f : ↑(Set.Icc a b) → β},
Continuous f → Continuous (Set.IccExtend h f)
This theorem states that if we have a function `f` that is defined and continuous on a closed interval [a, b] for some type `α` equipped with a linear order and a topological structure, and `β` is any type with a topological structure, then the extension of this function `f` to the entire set `α` using `Set.IccExtend` is also continuous. The linear order and topological structure on `α` are compatible in the sense that the order induces the given topological structure.
More concisely: If `f` is a continuous function on a closed interval [a, b] of a linearly ordered and topologically structured type `α`, then the extended function `Set.IccExtend f` is also continuous.
|
continuous_projIcc
theorem continuous_projIcc :
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} {h : a ≤ b} [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α], Continuous (Set.projIcc a b h)
This theorem states that for any type `α` that has a linear order and a topology which is an order topology, the projection of `α` onto the closed interval `[a, b]` is a continuous function, given that `a` is less than or equal to `b`. In mathematical terms, for any `α` in a topological space with an order topology, the function that maps any element to the closed interval `[a, b]` is continuous.
More concisely: For any type `α` with a linear order and an order topology, the function mapping elements to their closed intervals `[a, b]` (with `a ≤ b`) is continuous.
|