isTotal_le — Mathlib

English

The collection of upper sets is totally ordered under inclusion when the base type is linearly ordered; any two upper sets are comparable.

Русский

Множество верхних множеств образует линейный порядок по включению: любые два верхних множества сравнимы.

LaTeX

$$$ \forall s,t \in \text{UpperSet}(\alpha),\ s \le t \ \lor\ t \le s $$$

Lean4

instance isTotal_le : IsTotal (UpperSet α) (· ≤ ·) :=
  ⟨fun s t => t.upper.total s.upper⟩

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