isChain_univ_iff — Mathlib

English

The whole set is a chain if and only if the relation is trichotomous.

Русский

Вся множества является цепью тогда и только тогда, когда отношение тричотомично.

LaTeX

$$$\operatorname{IsChain}(r, \mathrm{univ}) \iff \operatorname{IsTrichotomous}(\alpha, r)$$$

Lean4

theorem isChain_univ_iff : IsChain r (univ : Set α) ↔ IsTrichotomous α r :=
  by
  refine ⟨fun h => ⟨fun a b => ?_⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩
  rw [or_left_comm, or_iff_not_imp_left]
  exact h trivial trivial

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