instOrderTop — Mathlib

English

The open neighborhoods of x form a ordered set (by inclusion) with a greatest element given by the whole space.

Русский

Открытые окрестности точки x образуют упорядоченную по включению совокупность с верхним элементом, равным всему пространству.

LaTeX

$$$\\\\forall U : \\\\mathrm{OpenNhdsOf}(x),\\\\ (U : Set\\\\,\\\\alpha) \\\\subseteq \\\\mathrm{univ}.$$$

Lean4

instance : OrderTop (OpenNhdsOf x) where
  top := ⟨⊤, Set.mem_univ _⟩
  le_top _ := subset_univ _

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