case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
b : Set (Set α)
hb : IsTopologicalBasis b
x y : α
h : x ≠ y
a : Set α
ab : a ∈ b
xa : x ∈ a
ha : a ⊆ {y_1 | y_1 ≠ y}
⊢ ∃ a, a ∈ b ∧ x ∈ a ∧ ¬y ∈ a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
b : Set (Set α)
hb : IsTopologicalBasis b
x y : α
h : x ≠ y
⊢ ∃ a, a ∈ b ∧ x ∈ a ∧ ¬y ∈ a
rcases hb.isOpen_iff.1 isOpen_ne x h with ⟨a, ab, xa, ha⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
b : Set (Set α)
hb : IsTopologicalBasis b
x y : α
h : x ≠ y
a : Set α
ab : a ∈ b
xa : x ∈ a
ha : a ⊆ {y_1 | y_1 ≠ y}
⊢ ∃ a, a ∈ b ∧ x ∈ a ∧ ¬y ∈ a
exact ⟨a, ab, xa, fun h => ha h rfl⟩