instOrderTop — Mathlib

English

There exists a top element in the order on DiscreteQuotient X, corresponding to the trivial quotient.

Русский

Существет элемент верх в порядке на DiscreteQuotient X, соответствующий тривиальному факторному отношению.

LaTeX

$$$ \\top \\in \\text{DiscreteQuotient}(X)$ is the trivial quotient$$

Lean4

instance : OrderTop (DiscreteQuotient X)
    where
  top := ⟨⊤, fun _ => isOpen_univ⟩
  le_top a := by tauto

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