α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔ ∀ (a : α), a ∈ {x | p x} → {x | p x} ∈ 𝓝 a
α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ Continuous p ↔ IsOpen {x | p x}
simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_Prop, isOpen_iff_mem_nhds]
no goals
α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔ ∀ (a : α), a ∈ {x | p x} → {x | p x} ∈ 𝓝 a
rfl