case intro
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hb : IsTopologicalBasis B
u : Set α
ou : IsOpen u
x : α
hx : x ∈ u
⊢ ∃ v, v ∈ B ∧ Set.Nonempty v ∧ v ⊆ u
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hb : IsTopologicalBasis B
u : Set α
hu : Set.Nonempty u
ou : IsOpen u
⊢ ∃ v, v ∈ B ∧ Set.Nonempty v ∧ v ⊆ u
cases' hu with x hx
case intro
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hb : IsTopologicalBasis B
u : Set α
ou : IsOpen u
x : α
hx : ∃ t, t ∈ {s | s ∈ B ∧ s ⊆ u} ∧ x ∈ t
⊢ ∃ v, v ∈ B ∧ Set.Nonempty v ∧ v ⊆ u
case intro
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hb : IsTopologicalBasis B
u : Set α
ou : IsOpen u
x : α
hx : x ∈ u
⊢ ∃ v, v ∈ B ∧ Set.Nonempty v ∧ v ⊆ u
rw [hb.open_eq_sUnion' ou, mem_sUnion] at hx
case intro.intro.intro
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hb : IsTopologicalBasis B
u : Set α
ou : IsOpen u
x : α
v : Set α
hv : v ∈ {s | s ∈ B ∧ s ⊆ u}
hxv : x ∈ v
⊢ ∃ v, v ∈ B ∧ Set.Nonempty v ∧ v ⊆ u
case intro
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hb : IsTopologicalBasis B
u : Set α
ou : IsOpen u
x : α
hx : ∃ t, t ∈ {s | s ∈ B ∧ s ⊆ u} ∧ x ∈ t
⊢ ∃ v, v ∈ B ∧ Set.Nonempty v ∧ v ⊆ u
rcases hx with ⟨v, hv, hxv⟩
no goals
case intro.intro.intro
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hb : IsTopologicalBasis B
u : Set α
ou : IsOpen u
x : α
v : Set α
hv : v ∈ {s | s ∈ B ∧ s ⊆ u}
hxv : x ∈ v
⊢ ∃ v, v ∈ B ∧ Set.Nonempty v ∧ v ⊆ u
exact ⟨v, hv.1, ⟨x, hxv⟩, hv.2⟩