toAlexandrovDiscrete — Mathlib

English

If α has an IsUpperSet structure, then α is Alexandrov-discrete.

Русский

Если у α есть структура IsUpperSet, то α является Alexandrov-раздельным пространством.

LaTeX

$$$ \text{AlexandrovDiscrete}(\alpha).$$$

Lean4

instance toAlexandrovDiscrete : AlexandrovDiscrete α where
  isOpen_sInter
    S := by
    simpa only [isOpen_iff_isUpperSet] using
      isUpperSet_sInter (α := α)
        -- c.f. isClosed_iff_lower_and_subset_implies_LUB_mem

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