Documentation

Mathlib.Topology.Order.ProjIcc

Projection onto a closed interval #

In this file we prove that the projection Set.projIcc f a b h is a quotient map, and use it to show that Set.IccExtend h f is continuous if and only if f is continuous.

theorem Filter.Tendsto.IccExtend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] {a : α} {b : α} {h : a b} (f : γ(Set.Icc a b)β) {la : Filter α} {lb : Filter β} {lc : Filter γ} (hf : Filter.Tendsto (f) (lc ×ˢ Filter.map (Set.projIcc a b h) la) lb) :
theorem continuous_projIcc {α : Type u_1} [LinearOrder α] {a : α} {b : α} {h : a b} [TopologicalSpace α] [OrderTopology α] :
theorem quotientMap_projIcc {α : Type u_1} [LinearOrder α] {a : α} {b : α} {h : a b} [TopologicalSpace α] [OrderTopology α] :
@[simp]
theorem continuous_IccExtend_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} {h : a b} [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] {f : (Set.Icc a b)β} :
theorem Continuous.IccExtend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] {a : α} {b : α} {h : a b} [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [TopologicalSpace γ] {f : γ(Set.Icc a b)β} {g : γα} (hf : Continuous f) (hg : Continuous g) :
Continuous fun (a_1 : γ) => Set.IccExtend h (f a_1) (g a_1)

See Note [continuity lemma statement].

theorem Continuous.Icc_extend' {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} {h : a b} [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] {f : (Set.Icc a b)β} (hf : Continuous f) :

A useful special case of Continuous.IccExtend.

theorem ContinuousAt.IccExtend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] {a : α} {b : α} {h : a b} [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [TopologicalSpace γ] {x : γ} (f : γ(Set.Icc a b)β) {g : γα} (hf : ContinuousAt (f) (x, Set.projIcc a b h (g x))) (hg : ContinuousAt g x) :
ContinuousAt (fun (a_1 : γ) => Set.IccExtend h (f a_1) (g a_1)) x