predOrder — Mathlib

English

PredOrder on locally finite linear orders is defined via the dual of succ.

Русский

PredOrder на локально конечных линейных порядках определяется через дуальность succ.

LaTeX

$$$\\text{PredOrder}(\\iota) := \\text{SuccOrder}(\\iota^{op})^{op}$$$

Lean4

/-- A locally finite order is a `PredOrder`.
This is not an instance, because its `succ` field conflicts with computable `PredOrder` structures
on `ℕ` and `ℤ`. -/
noncomputable def predOrder [LocallyFiniteOrder ι] : PredOrder ι :=
  letI := succOrder (ι := ιᵒᵈ)
  inferInstanceAs (PredOrder ιᵒᵈᵒᵈ)

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