# 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.

source
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
source
theorem continuous_projIcc {α : Type u_1} [LinearOrder α] {a b : α} {h : a ≤ b} [TopologicalSpace α] [OrderTopology α] :
Continuous (Set.projIcc a b h)
source
theorem isQuotientMap_projIcc {α : Type u_1} [LinearOrder α] {a b : α} {h : a ≤ b} [TopologicalSpace α] [OrderTopology α] :
Topology.IsQuotientMap (Set.projIcc a b h)
source
@[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
source
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].

source
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`.

source
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