isOpen_uniformity — Mathlib

English

A set s is open iff for every x in s, the corresponding uniformity neighborhood is in the uniformity filter.

Русский

Множество s открыто тогда и только тогда, когда для каждого x ∈ s соответствующая окрестность в равномерности принадлежит фильтру равномерности.

LaTeX

$$$IsOpen(s) \\iff \\forall x\\in s,\\ {p\\in \\alpha\\times \\alpha\\;|\\; p_{1}=x \\Rightarrow p_{2}\\in s} \\in 𝓤 α$$$

Lean4

theorem isOpen_uniformity {s : Set α} : IsOpen s ↔ ∀ x ∈ s, {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α := by
  simp only [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap_prodMk]

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