Projection onto a closed interval #
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.
@[continuity]
theorem
continuous_proj_Icc
{α : Type u_1}
[topological_space α]
[linear_order α]
[order_topology α]
{a b : α}
{h : a ≤ b} :
continuous (set.proj_Icc a b h)
theorem
quotient_map_proj_Icc
{α : Type u_1}
[topological_space α]
[linear_order α]
[order_topology α]
{a b : α}
{h : a ≤ b} :
quotient_map (set.proj_Icc a b h)
@[simp]
theorem
continuous_Icc_extend_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[linear_order α]
[order_topology α]
[topological_space β]
{a b : α}
{h : a ≤ b}
{f : ↥(set.Icc a b) → β} :
continuous (set.Icc_extend h f) ↔ continuous f
@[continuity]
theorem
continuous.Icc_extend
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[linear_order α]
[order_topology α]
[topological_space β]
{a b : α}
{h : a ≤ b}
{f : ↥(set.Icc a b) → β}
(hf : continuous f) :
continuous (set.Icc_extend h f)