isWellOrder — Mathlib

English

An ordinal x is well-ordered by ∈ when restricted to x.

Русский

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

LaTeX

$$$IsOrdinal(x) \Rightarrow IsWellOrder\_\{Subrel(\in, \in x)\}$$$

Lean4

protected theorem isWellOrder (h : x.IsOrdinal) : IsWellOrder _ (Subrel (· ∈ ·) (· ∈ x))
    where
  wf := (Subrel.relEmbedding _ _).wellFounded mem_wf
  trans := h.isTrans.1
  trichotomous := h.isTrichotomous.1

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