instLinearOrder — Mathlib

English

There is a linear order on UpperSet α when α is linearly ordered, making UpperSet α a linear order itself.

Русский

Существует линейный порядок на множестве UpperSet α, если α линейно упорядовано, поэтому сам UpperSet α образует линейный порядок.

LaTeX

$$$ \text{LinearOrder}(\text{UpperSet}(\alpha)) $$$

Lean4

noncomputable instance instLinearOrder : LinearOrder (UpperSet α) := by classical exact Lattice.toLinearOrder _

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