α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
change _ ↔ _ ∧ ∀ b : α, b ≠ a → IsOpen {b}
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ 𝓝 a ≤ pure a ⊔ f → ((∀ (b : α), b ≠ a → 𝓝 b = pure b) ↔ ∀ (b : α), b ≠ a → IsOpen {b})
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
rw [le_nhdsAdjoint_iff', and_congr_right_iff]
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
x✝ : 𝓝 a ≤ pure a ⊔ f
b : α
⊢ b ≠ a → 𝓝 b = pure b ↔ b ≠ a → IsOpen {b}
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ 𝓝 a ≤ pure a ⊔ f → ((∀ (b : α), b ≠ a → 𝓝 b = pure b) ↔ ∀ (b : α), b ≠ a → IsOpen {b})
refine fun _ => forall_congr' fun b => ?_
no goals
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
x✝ : 𝓝 a ≤ pure a ⊔ f
b : α
⊢ b ≠ a → 𝓝 b = pure b ↔ b ≠ a → IsOpen {b}
rw [@isOpen_singleton_iff_nhds_eq_pure α t b]