-
Notifications
You must be signed in to change notification settings - Fork 307
/
ProjIcc.lean
72 lines (57 loc) · 3.17 KB
/
ProjIcc.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov, Patrick Massot
-/
import Mathlib.Data.Set.Intervals.ProjIcc
import Mathlib.Topology.Order.Basic
#align_import topology.algebra.order.proj_Icc from "leanprover-community/mathlib"@"4c19a16e4b705bf135cf9a80ac18fcc99c438514"
/-!
# 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.
-/
open Set Filter Topology
variable {α β γ : Type*} [LinearOrder α] [TopologicalSpace γ] {a b c : α} {h : a ≤ b}
-- Porting note (#10756): new lemma
protected theorem Filter.Tendsto.IccExtend (f : γ → Icc a b → β) {la : Filter α} {lb : Filter β}
{lc : Filter γ} (hf : Tendsto (↿f) (lc ×ˢ la.map (projIcc a b h)) lb) :
Tendsto (↿(IccExtend h ∘ f)) (lc ×ˢ la) lb :=
hf.comp <| tendsto_id.prod_map tendsto_map
@[deprecated Filter.Tendsto.IccExtend]
theorem Filter.Tendsto.IccExtend' (f : γ → Icc a b → β) {z : γ} {l : Filter α} {l' : Filter β}
(hf : Tendsto (↿f) (𝓝 z ×ˢ l.map (projIcc a b h)) l') :
Tendsto (↿(IccExtend h ∘ f)) (𝓝 z ×ˢ l) l' :=
hf.IccExtend f
#align filter.tendsto.Icc_extend Filter.Tendsto.IccExtend'
variable [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β]
@[continuity]
theorem continuous_projIcc : Continuous (projIcc a b h) :=
(continuous_const.max <| continuous_const.min continuous_id).subtype_mk _
#align continuous_proj_Icc continuous_projIcc
theorem quotientMap_projIcc : QuotientMap (projIcc a b h) :=
quotientMap_iff.2 ⟨projIcc_surjective h, fun s =>
⟨fun hs => hs.preimage continuous_projIcc, fun hs => ⟨_, hs, by ext; simp⟩⟩⟩
#align quotient_map_proj_Icc quotientMap_projIcc
@[simp]
theorem continuous_IccExtend_iff {f : Icc a b → β} : Continuous (IccExtend h f) ↔ Continuous f :=
quotientMap_projIcc.continuous_iff.symm
#align continuous_Icc_extend_iff continuous_IccExtend_iff
/-- See Note [continuity lemma statement]. -/
protected theorem Continuous.IccExtend {f : γ → Icc a b → β} {g : γ → α} (hf : Continuous ↿f)
(hg : Continuous g) : Continuous fun a => IccExtend h (f a) (g a) :=
show Continuous (↿f ∘ fun x => (x, projIcc a b h (g x)))
from hf.comp <| continuous_id.prod_mk <| continuous_projIcc.comp hg
#align continuous.Icc_extend Continuous.IccExtend
/-- A useful special case of `Continuous.IccExtend`. -/
@[continuity]
protected theorem Continuous.Icc_extend' {f : Icc a b → β} (hf : Continuous f) :
Continuous (IccExtend h f) :=
hf.comp continuous_projIcc
#align continuous.Icc_extend' Continuous.Icc_extend'
theorem ContinuousAt.IccExtend {x : γ} (f : γ → Icc a b → β) {g : γ → α}
(hf : ContinuousAt (↿f) (x, projIcc a b h (g x))) (hg : ContinuousAt g x) :
ContinuousAt (fun a => IccExtend h (f a) (g a)) x :=
show ContinuousAt (↿f ∘ fun x => (x, projIcc a b h (g x))) x from
ContinuousAt.comp hf <| continuousAt_id.prod <| continuous_projIcc.continuousAt.comp hg
#align continuous_at.Icc_extend ContinuousAt.IccExtend