α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
x : α
h : HasBasis (𝓝 x) p s
⊢ (∀ (i : ι), p i → x ∈ s i) ∧ ∀ (x_1 : α), (∀ (i : ι), p i → x_1 ∈ s i) → x_1 = x
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
x : α
h : HasBasis (𝓝 x) p s
⊢ (⋂ (i : ι) (_ : p i), s i) = {x}
simp only [eq_singleton_iff_unique_mem, mem_iInter]
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
x : α
h : HasBasis (𝓝 x) p s
y : α
hy : ∀ (i : ι), p i → y ∈ s i
⊢ y = x
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
x : α
h : HasBasis (𝓝 x) p s
⊢ (∀ (i : ι), p i → x ∈ s i) ∧ ∀ (x_1 : α), (∀ (i : ι), p i → x_1 ∈ s i) → x_1 = x
refine' ⟨fun i hi => mem_of_mem_nhds <| h.mem_of_mem hi, fun y hy => _⟩
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
x : α
h : HasBasis (𝓝 x) p s
y : α
hy : y ≠ x
⊢ ∃ i, p i ∧ ¬y ∈ s i
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
x : α
h : HasBasis (𝓝 x) p s
y : α
hy : ∀ (i : ι), p i → y ∈ s i
⊢ y = x
contrapose! hy
case intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
x : α
h : HasBasis (𝓝 x) p s
y : α
hy : y ≠ x
i : ι
hi : p i
hsub : s i ⊆ {y}ᶜ
⊢ ∃ i, p i ∧ ¬y ∈ s i
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
x : α
h : HasBasis (𝓝 x) p s
y : α
hy : y ≠ x
⊢ ∃ i, p i ∧ ¬y ∈ s i
rcases h.mem_iff.1 (compl_singleton_mem_nhds hy.symm) with ⟨i, hi, hsub⟩
no goals
case intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
x : α
h : HasBasis (𝓝 x) p s
y : α
hy : y ≠ x
i : ι
hi : p i
hsub : s i ⊆ {y}ᶜ
⊢ ∃ i, p i ∧ ¬y ∈ s i
exact ⟨i, hi, fun h => hsub h rfl⟩