isOpen_iff_nhds — Mathlib

English

A set s is open iff every point x in s has nhds x contained in the principal filter of s.

Русский

Множество s открыто тогда и только тогда, когда для каждого x ∈ s окрестности x удовлетворяют 𝓝(x) ≤ 𝓟(s).

LaTeX

$$$\\text{IsOpen}(s) \\iff \\forall x \\in s, \\mathcal{N}(x) \\le \\mathcal{P}(s)$$$

Lean4

theorem isOpen_iff_nhds : IsOpen s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s :=
  calc
    IsOpen s ↔ s ⊆ interior s := subset_interior_iff_isOpen.symm
    _ ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s := by simp_rw [interior_eq_nhds, subset_def, mem_setOf]

Похожие утверждения