mathlib3 documentation

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

See Note [continuity lemma statement].

@[continuity]
theorem continuous.Icc_extend' {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} {h : a b} [topological_space α] [order_topology α] [topological_space β] {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 α] [topological_space γ] {a b : α} {h : a b} [topological_space α] [order_topology α] [topological_space β] {x : γ} (f : γ (set.Icc a b) β) {g : γ α} (hf : continuous_at f (x, set.proj_Icc a b h (g x))) (hg : continuous_at g x) :
continuous_at (λ (a_1 : γ), set.Icc_extend h (f a_1) (g a_1)) x