Theorem: ChartedSpace.regularSpace (Ray/Misc/ChartedSpace.lean)

State before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
⊢ RegularSpace M
Tactic:
apply RegularSpace.ofExistsMemNhdsIsClosedSubset
State after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
⊢ ∀ (x : M), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

State before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
⊢ ∀ (x : M), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
intro x s n
State after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

State before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
set t := (chartAt A x).target ∩ (chartAt A x).symm ⁻¹' ((chartAt A x).source ∩ s)
State after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

State before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
have cn : (chartAt A x).source ∈ 𝓝 x :=
  (chartAt A x).open_source.mem_nhds (mem_chart_source A x)
State after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

State before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
have tn : t ∈ 𝓝 (chartAt A x x) := by
  apply Filter.inter_mem ((chartAt A x).open_target.mem_nhds (mem_chart_target A x))
  apply ((chartAt A x).continuousAt_symm (mem_chart_target _ _)).preimage_mem_nhds
  rw [(chartAt A x).left_inv (mem_chart_source _ _)]; exact Filter.inter_mem cn n
State after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
tn : t ∈ 𝓝 (↑(_root_.chartAt A x) x)
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

State before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
tn : t ∈ 𝓝 (↑(_root_.chartAt A x) x)
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
rcases local_compact_nhds tn with ⟨u, un, ut, uc⟩
State after:
case h.intro.intro.intro
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
tn : t ∈ 𝓝 (↑(_root_.chartAt A x) x)
u : Set A
un : u ∈ 𝓝 (↑(_root_.chartAt A x) x)
ut : u ⊆ t
uc : IsCompact u
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

State before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(_root_.chartAt A x) x)
Tactic:
apply Filter.inter_mem ((chartAt A x).open_target.mem_nhds (mem_chart_target A x))
State after:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s) ∈ 𝓝 (↑(_root_.chartAt A x) x)

State before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s) ∈ 𝓝 (↑(_root_.chartAt A x) x)
Tactic:
apply ((chartAt A x).continuousAt_symm (mem_chart_target _ _)).preimage_mem_nhds
State after:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ (_root_.chartAt A x).source ∩ s ∈ 𝓝 (↑(_root_.chartAt A x).symm (↑(_root_.chartAt A x) x))

State before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ (_root_.chartAt A x).source ∩ s ∈ 𝓝 (↑(_root_.chartAt A x).symm (↑(_root_.chartAt A x) x))
Tactic:
rw [(chartAt A x).left_inv (mem_chart_source _ _)]
State after:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ (_root_.chartAt A x).source ∩ s ∈ 𝓝 x

State before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ (_root_.chartAt A x).source ∩ s ∈ 𝓝 x
Tactic:
exact Filter.inter_mem cn n
State after:
no goals