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') :
filter.tendsto ↿(set.Icc_extend h ∘ f) ((nhds z).prod l) l'
@[continuity]
theorem
continuous_proj_Icc
{α : Type u_1}
[linear_order α]
{a b : α}
{h : a ≤ b}
[topological_space α]
[order_topology α] :
continuous (set.proj_Icc a b h)
theorem
quotient_map_proj_Icc
{α : Type u_1}
[linear_order α]
{a b : α}
{h : a ≤ b}
[topological_space α]
[order_topology α] :
quotient_map (set.proj_Icc a b h)
@[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) → β} :
continuous (set.Icc_extend h f) ↔ continuous f
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))
@[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) :
continuous (set.Icc_extend h 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