mathlib documentation

topology.algebra.ordered.proj_Icc

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.

theorem continuous_proj_Icc {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] {a b : α} {h : a b} :
theorem quotient_map_proj_Icc {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] {a b : α} {h : a b} :
@[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) → β} :
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) :