ofLinearWellFoundedGT — Mathlib

English

A linear order with well-founded greater-than relation yields a PredOrder structure; the construction uses the LT well-foundedness on the dual.

Русский

Линейный порядок с хорошо основанным отношением больше даёт структуру PredOrder; конструирование через LT на двойственном порядке.

LaTeX

$$$\\text{PredOrder}(\\alpha) \\text{ из линейного порядка } \\alpha \\text{ с WellFoundedGT } \\alpha.$$$

Lean4

/-- A linear order with well-founded greater-than relation is a `PredOrder`. -/
noncomputable def ofLinearWellFoundedGT (α) [LinearOrder α] [WellFoundedGT α] : PredOrder α :=
  letI := SuccOrder.ofLinearWellFoundedLT αᵒᵈ;
  inferInstanceAs (PredOrder αᵒᵈᵒᵈ)

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