instWellFoundedLT — Mathlib

English

If α has a linear order and is well-founded in LT, then WithBot α is well-founded in LT.

Русский

Если у α имеется линейный порядок и он хорошо-подчинен (well-founded) по LT, то WithBot α также хорошо-подчинен по LT.

LaTeX

$$$[LT \alpha] \; [WellFoundedLT \alpha] \Rightarrow WellFoundedLT(WithBot \alpha)$$$

Lean4

instance instWellFoundedLT [LT α] [WellFoundedLT α] : WellFoundedLT (WithBot α) where
  wf :=
    .intro fun
      | ⊥ => ⟨_, by simp⟩
      | (a : α) =>
        (wellFounded_lt.1 a).rec fun _ _ ih ↦
          .intro _ fun
            | ⊥, _ => ⟨_, by simp⟩
            | (b : α), hlt => ih _ (coe_lt_coe.1 hlt)

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