instWellFoundedGT — Mathlib

English

If α has LT and WellFoundedGT, then WithBot α is well-founded for GT as well.

Русский

Если у α есть LT и WellFoundedGT, то WithBot α также хорошо-founded по GT.

LaTeX

$$$[LT \alpha] [WellFoundedGT \alpha] \Rightarrow WellFoundedGT(WithBot \alpha)$$$

Lean4

instance _root_.WithBot.instWellFoundedGT [LT α] [WellFoundedGT α] : WellFoundedGT (WithBot α) where
  wf :=
    have acc_some (a : α) : Acc ((· > ·) : WithBot α → WithBot α → Prop) a :=
      (wellFounded_gt.1 a).rec fun _ _ ih =>
        .intro _ fun
          | (b : α), hlt => ih _ (coe_lt_coe.1 hlt)
    .intro fun
      | (a : α) => acc_some a
      | ⊥ =>
        .intro _ fun
          | (b : α), _ => acc_some b

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