gt — Mathlib · SciLib

English

WithTop IsWellOrder GT: If α is well-ordered by > then WithTop α is well-ordered by >.

Русский

WithTop имеет хорошо упорядоченность по '>' если α хорошо упорядочено по '>'.

LaTeX

$$$\\operatorname{IsWellOrder}(\\mathrm{WithTop}\\,\\alpha, >)$ given $\\operatorname{IsWellOrder}(\\alpha, >)$.$$

Lean4

instance _root_.WithBot.isWellOrder.gt [Preorder α] [h : IsWellOrder α (· > ·)] : IsWellOrder (WithBot α) (· > ·) where
  trichotomous x y := by cases x <;> cases y <;> simp; simpa using trichotomous_of (· > ·) ..

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