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 : Tendsto (↿f) (lc ×ˢ map (Set.projIcc a b h) la) lb) : Tendsto (↿(Set.IccExtend h ∘ f)) (lc ×ˢ la) lb

theorem continuous_projIcc {α : Type u_1} [LinearOrder α] {a b : α} {h : a ≤ b} [TopologicalSpace α] [OrderTopology α] : Continuous (Set.projIcc a b h)

theorem isQuotientMap_projIcc {α : Type u_1} [LinearOrder α] {a b : α} {h : a ≤ b} [TopologicalSpace α] [OrderTopology α] : Topology.IsQuotientMap (Set.projIcc a b h)

@[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) → β} : Continuous (Set.IccExtend h f) ↔ Continuous f

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) : Continuous (Set.IccExtend h 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