pred_eq_of_not_isMin — Mathlib

English

For any j and i ∈ Ici(j), if i is not minimal, then Order.pred i equals the pair with the underlying value and a proof.

Русский

Для любого j и i ∈ Ici(j), если i не минимален, то Order.pred i равна паре с основанным значением и доказательством.

LaTeX

$$$\\neg \\mathrm{IsMin}(i) \\Rightarrow \\mathrm{Order.pred}\,i = \\langle \\mathrm{Order.pred} i.1, \\text{proof} \\rangle$$$

Lean4

theorem pred_eq_of_not_isMin [PredOrder J] {j : J} {i : Set.Ici j} (hi : ¬IsMin i) :
    Order.pred i =
      ⟨Order.pred i.1, by
        rw [← coe_pred_of_not_isMin hi]
        apply Subtype.coe_prop⟩ :=
  by
  ext
  simp only [coe_pred_of_not_isMin hi]

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