Projection onto a closed interval #
In this file we prove that the projection Set.projIcc f a b h is a quotient map, and use it
to show that Set.IccExtend h f is continuous if and only if f is continuous.
theorem
Filter.Tendsto.IccExtend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[LinearOrder α]
{a b : α}
{h : a ≤ b}
(f : γ → ↑(Set.Icc a b) → β)
{la : Filter α}
{lb : Filter β}
{lc : Filter γ}
(hf : Tendsto (↿f) (lc ×ˢ map (Set.projIcc a b h) la) lb)
:
Tendsto (↿(Set.IccExtend h ∘ f)) (lc ×ˢ la) lb
theorem
continuous_projIcc
{α : Type u_1}
[LinearOrder α]
{a b : α}
{h : a ≤ b}
[TopologicalSpace α]
[OrderTopology α]
:
Continuous (Set.projIcc a b h)
theorem
isQuotientMap_projIcc
{α : Type u_1}
[LinearOrder α]
{a b : α}
{h : a ≤ b}
[TopologicalSpace α]
[OrderTopology α]
:
Topology.IsQuotientMap (Set.projIcc a b h)
@[simp]
theorem
continuous_IccExtend_iff
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
{a b : α}
{h : a ≤ b}
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
{f : ↑(Set.Icc a b) → β}
:
theorem
Continuous.IccExtend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[LinearOrder α]
{a b : α}
{h : a ≤ b}
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : γ → ↑(Set.Icc a b) → β}
{g : γ → α}
(hf : Continuous ↿f)
(hg : Continuous g)
:
Continuous fun (a_1 : γ) => Set.IccExtend h (f a_1) (g a_1)
See Note [continuity lemma statement].
theorem
Continuous.Icc_extend'
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
{a b : α}
{h : a ≤ b}
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
{f : ↑(Set.Icc a b) → β}
(hf : Continuous f)
:
Continuous (Set.IccExtend h f)
A useful special case of Continuous.IccExtend.
theorem
ContinuousAt.IccExtend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[LinearOrder α]
{a b : α}
{h : a ≤ b}
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
[TopologicalSpace γ]
{x : γ}
(f : γ → ↑(Set.Icc a b) → β)
{g : γ → α}
(hf : ContinuousAt ↿f (x, Set.projIcc a b h (g x)))
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a_1 : γ) => Set.IccExtend h (f a_1) (g a_1)) x