total — Mathlib

English

In a linear order, any two upper sets are comparable by inclusion: for any upper sets s and t, either s ⊆ t or t ⊆ s.

Русский

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

LaTeX

$$$\text{If } s,t \subseteq α \text{ are IsUpperSet, then } s \subseteq t \lor t \subseteq s.$$$

Lean4

theorem total (hs : IsUpperSet s) (ht : IsUpperSet t) : s ⊆ t ∨ t ⊆ s :=
  by
  by_contra! h
  simp_rw [Set.not_subset] at h
  obtain ⟨⟨a, has, hat⟩, b, hbt, hbs⟩ := h
  obtain hab | hba := le_total a b
  · exact hbs (hs hab has)
  · exact hat (ht hba hbt)

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