# mathlib3documentation

topology.algebra.order.proj_Icc

# Projection onto a closed interval #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem filter.tendsto.Icc_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [linear_order α] {a b : α} {h : a b} (f : γ (set.Icc a b) β) {z : γ} {l : filter α} {l' : filter β} (hf : ((nhds z).prod (filter.map b h) l)) l') :
((nhds z).prod l) l'
@[continuity]
theorem continuous_proj_Icc {α : Type u_1} [linear_order α] {a b : α} {h : a b}  :
theorem quotient_map_proj_Icc {α : Type u_1} [linear_order α] {a b : α} {h : a b}  :
@[simp]
theorem continuous_Icc_extend_iff {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} {h : a b} {f : (set.Icc a b) β} :
theorem continuous.Icc_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [linear_order α] {a b : α} {h : a b} {f : γ (set.Icc a b) β} {g : γ α} (hf : continuous f) (hg : continuous g) :
continuous (λ (a_1 : γ), (f a_1) (g a_1))
@[continuity]
theorem continuous.Icc_extend' {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} {h : a b} {f : (set.Icc a b) β} (hf : continuous f) :

A useful special case of continuous.Icc_extend.

theorem continuous_at.Icc_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [linear_order α] {a b : α} {h : a b} {x : γ} (f : γ (set.Icc a b) β) {g : γ α} (hf : (x, b h (g x))) (hg : x) :
continuous_at (λ (a_1 : γ), (f a_1) (g a_1)) x