α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ x ∈ v ∧ v ⊆ U
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
⊢ IsTopologicalBasis {s | IsClopen s}
refine isTopologicalBasis_of_open_of_nhds (fun u hu => hu.1) fun x U memU hU => ?_
case intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ x ∈ v ∧ v ⊆ U
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ x ∈ v ∧ v ⊆ U
obtain ⟨s, comp, xs, sU⟩ := exists_compact_subset hU memU
case intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ x ∈ v ∧ v ⊆ U
case intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ x ∈ v ∧ v ⊆ U
let u : Set s := ((↑) : s → H) ⁻¹' interior s
case intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ x ∈ v ∧ v ⊆ U
case intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ x ∈ v ∧ v ⊆ U
have u_open_in_s : IsOpen u := isOpen_interior.preimage continuous_subtype_val
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ ↑x ∈ v ∧ v ⊆ U
case intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ x ∈ v ∧ v ⊆ U
lift x to s using interior_subset xs
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ ↑x ∈ v ∧ v ⊆ U
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ ↑x ∈ v ∧ v ⊆ U
haveI : CompactSpace s := isCompact_iff_compactSpace.1 comp
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ ↑x ∈ v ∧ v ⊆ U
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ ↑x ∈ v ∧ v ⊆ U
obtain ⟨V : Set s, clopen_in_s, Vx, V_sub⟩ := compact_exists_clopen_in_open u_open_in_s xs
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
V_clopen : IsClopen (Subtype.val '' V)
⊢ Subtype.val '' V ⊆ s
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
V_clopen : IsClopen (Subtype.val '' V)
⊢ ∃ v, v ∈ {s | IsClopen s} ∧ ↑x ∈ v ∧ v ⊆ U
refine' ⟨(↑) '' V, V_clopen, by simp [Vx], Subset.trans _ sU⟩
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
V_clopen : IsClopen (Subtype.val '' V)
⊢ Subtype.val '' V ⊆ s
simp
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ IsOpen (Subtype.val '' V)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ IsClopen (Subtype.val '' V)
refine' ⟨_, comp.isClosed.closedEmbedding_subtype_val.closed_iff_image_closed.1 clopen_in_s.2⟩
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
⊢ IsOpen (Subtype.val '' V)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ IsOpen (Subtype.val '' V)
let v : Set u := ((↑) : u → s) ⁻¹' V
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
⊢ IsOpen (Subtype.val '' V)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
⊢ IsOpen (Subtype.val '' V)
have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
⊢ IsOpen (Subtype.val '' V)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
⊢ IsOpen (Subtype.val '' V)
have f0 : Embedding ((↑) : u → H) := embedding_subtype_val.comp embedding_subtype_val
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
f1 : OpenEmbedding fun x => ↑↑x
f2 : IsOpen v
⊢ IsOpen (Subtype.val '' V)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
f1 : OpenEmbedding fun x => ↑↑x
⊢ IsOpen (Subtype.val '' V)
have f2 : IsOpen v := clopen_in_s.1.preimage continuous_subtype_val
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
f1 : OpenEmbedding fun x => ↑↑x
f2 : IsOpen v
f3 : Subtype.val '' V = (fun x => ↑↑x) '' v
⊢ IsOpen (Subtype.val '' V)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
f1 : OpenEmbedding fun x => ↑↑x
f2 : IsOpen v
⊢ IsOpen (Subtype.val '' V)
have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by
  rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_left V_sub]
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
f1 : OpenEmbedding fun x => ↑↑x
f2 : IsOpen v
f3 : Subtype.val '' V = (fun x => ↑↑x) '' v
⊢ IsOpen ((fun x => ↑↑x) '' v)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
f1 : OpenEmbedding fun x => ↑↑x
f2 : IsOpen v
f3 : Subtype.val '' V = (fun x => ↑↑x) '' v
⊢ IsOpen (Subtype.val '' V)
rw [f3]
no goals
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
f1 : OpenEmbedding fun x => ↑↑x
f2 : IsOpen v
f3 : Subtype.val '' V = (fun x => ↑↑x) '' v
⊢ IsOpen ((fun x => ↑↑x) '' v)
apply f1.isOpenMap v f2
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
⊢ IsOpen (range fun x => ↑↑x)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
⊢ OpenEmbedding fun x => ↑↑x
refine' ⟨f0, _⟩
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝¹ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this✝ : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
this : (range fun x => ↑↑x) = interior s
⊢ IsOpen (range fun x => ↑↑x)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
⊢ IsOpen (range fun x => ↑↑x)
have : Set.range ((↑) : u → H) = interior s := by
  rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
  apply Set.inter_eq_self_of_subset_left interior_subset
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝¹ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this✝ : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
this : (range fun x => ↑↑x) = interior s
⊢ IsOpen (interior s)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝¹ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this✝ : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
this : (range fun x => ↑↑x) = interior s
⊢ IsOpen (range fun x => ↑↑x)
rw [this]
no goals
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝¹ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this✝ : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
this : (range fun x => ↑↑x) = interior s
⊢ IsOpen (interior s)
apply isOpen_interior
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
⊢ interior s ∩ s = interior s
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
⊢ (range fun x => ↑↑x) = interior s
rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
no goals
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
⊢ interior s ∩ s = interior s
apply Set.inter_eq_self_of_subset_left interior_subset
no goals
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x => ↑↑x) = Subtype.val ∘ Subtype.val
f0 : _root_.Embedding fun x => ↑↑x
f1 : OpenEmbedding fun x => ↑↑x
f2 : IsOpen v
⊢ Subtype.val '' V = (fun x => ↑↑x) '' v
rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_left V_sub]
no goals
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
H : Type u_1
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
clopen_in_s : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
V_clopen : IsClopen (Subtype.val '' V)
⊢ ↑x ∈ Subtype.val '' V
simp [Vx]