total — Mathlib

English

Let s and t be lower sets in a linear order. Then either s ⊆ t or t ⊆ s.

Русский

Пусть s и t — нижние множества в линейном порядке. Тогда либо s ⊆ t, либо t ⊆ s.

LaTeX

$$$\\\\forall \\\\alpha [\\\\mathrm{LinearOrder}(\\\\alpha)], \\\\forall s,t \\\\subseteq \\\\alpha, \\\\mathrm{IsLowerSet}(s) \\\\to \\\\mathrm{IsLowerSet}(t) \\\\to s \\\\subseteq t \\\\lor t \\\\subseteq s$$$

Lean4

theorem total (hs : IsLowerSet s) (ht : IsLowerSet t) : s ⊆ t ∨ t ⊆ s :=
  hs.toDual.total ht.toDual

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