# Documentation

Mathlib.Topology.Algebra.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} [] {a : α} {b : α} {h : a b} (f : γ↑(Set.Icc a b)β) {la : } {lb : } {lc : } (hf : Filter.Tendsto (f) (lc ×ˢ Filter.map (Set.projIcc a b h) la) lb) :
Filter.Tendsto (()) (lc ×ˢ la) lb
@[deprecated Filter.Tendsto.IccExtend]
theorem Filter.Tendsto.IccExtend' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {a : α} {b : α} {h : a b} (f : γ↑(Set.Icc a b)β) {z : γ} {l : } {l' : } (hf : Filter.Tendsto (f) (nhds z ×ˢ Filter.map (Set.projIcc a b h) l) l') :
theorem continuous_projIcc {α : Type u_1} [] {a : α} {b : α} {h : a b} [] [] :
theorem quotientMap_projIcc {α : Type u_1} [] {a : α} {b : α} {h : a b} [] [] :
@[simp]
theorem continuous_IccExtend_iff {α : Type u_1} {β : Type u_2} [] {a : α} {b : α} {h : a b} [] [] [] {f : ↑(Set.Icc a b)β} :
theorem Continuous.IccExtend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {a : α} {b : α} {h : a b} [] [] [] {f : γ↑(Set.Icc a b)β} {g : γα} (hf : ) (hg : ) :
Continuous fun a => Set.IccExtend h (f a) (g a)

See Note [continuity lemma statement].

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

A useful special case of Continuous.IccExtend.

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