English
Let P be a property of sets and let hP be monotone with respect to inclusion. Then P holds for all s ∈ 𝓝 x if and only if P holds for all open s with x ∈ s.
Русский
Пусть P — свойство множеств и P монотонно в отношении включения. Тогда P выполняется для всех s ∈ 𝓝 x тогда и только тогда, когда P выполняется для всех открытых s, содержащих x.
LaTeX
$$$\\forall s ∈ 𝓝 x,\ P(s) \\quad\\text{iff}\\quad \\forall s\\ IsOpen(s) \\land x ∈ s,\\ P(s).$$$
Lean4
theorem all_mem_nhds (x : X) (P : Set X → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) :
(∀ s ∈ 𝓝 x, P s) ↔ ∀ s, IsOpen s → x ∈ s → P s :=
((nhds_basis_opens x).forall_iff hP).trans <| by simp only [@and_comm (x ∈ _), and_imp]
