instTop — Mathlib

English

The top element of ClopenUpperSet α is the pair consisting of the largest open set (the whole space) and the corresponding upper structure.

Русский

Верхний элемент ClopenUpperSet α — это пара, состоящая из наибольшего открытого множества (всего пространства) и соответствующей верхней структуры.

LaTeX

$$$\\\\text{instTop}: \\\\text{Top}(ClopenUpperSet(\\\\alpha)) \\\\text{ with } (top) = \\\\langle\\\\top, isUpperSet\\\\_univ\\\\rangle.$$$

Lean4

instance : Top (ClopenUpperSet α) :=
  ⟨⟨⊤, isUpperSet_univ⟩⟩

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