isOpen_iff_ultrafilter — Mathlib

English

A set s is open if and only if for every x ∈ s and every ultrafilter l on X with l ≤ 𝓝 x, we have s ∈ l.

Русский

Множество s открыто тогда и только тогда для каждого x ∈ s и каждого ультрафильтра l на X с l ≤ 𝓝 x выполняется s ∈ l.

LaTeX

$$$\\IsOpen(s) \\iff \\forall x \\in s, \\forall l : Ultrafilter X, l \\le 𝓝 x \\rightarrow s \\in l$$$

Lean4

theorem isOpen_iff_ultrafilter : IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → s ∈ l := by
  simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter]

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