isTrichotomous — Mathlib

English

An ordinal x has a trichotomous membership relation among its elements.

Русский

Ординал x имеет тричотомное отношение принадлежности между своими элементами.

LaTeX

$$$IsOrdinal(x) \Rightarrow IsTrichotomous\_\{Subrel(\in, \in x)\}$(the relation on elements of x is trichotomous)$$

Lean4

protected theorem isTrichotomous (h : x.IsOrdinal) : IsTrichotomous _ (Subrel (· ∈ ·) (· ∈ x)) :=
  ⟨fun ⟨a, ha⟩ ⟨b, hb⟩ ↦ by simpa using mem_trichotomous (h.mem ha) (h.mem hb)⟩

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