coe_pred_of_not_isMin — Mathlib

English

Let J be a partially ordered type. If i ∈ Ici(j) is not minimal, then the predecessor of i equals the pair of the predecessor of i.1 with a proof.

Русский

Пусть J — частично упорядоченный тип. Если i ∈ Ici(j) не минимален, то предшествующий i равен паре, состоящей из предшествующего i.1 и доказательства.

LaTeX

$$$[\\text{PredOrder } J] \\Rightarrow (\\mathrm{Order.pred}\,i).1 = \\mathrm{Order.pred}\,i.1$ под условием $\\neg \\mathrm{IsMin}(i)$$$

Lean4

theorem coe_pred_of_not_isMin [PredOrder J] {j : J} {i : Set.Ici j} (hi : ¬IsMin i) :
    (Order.pred i).1 = Order.pred i.1 := by
  rw [coe_pred_of_mem]
  apply Order.le_pred_of_lt
  exact lt_of_le_of_ne (α := Set.Ici j) bot_le (Ne.symm (by simpa using hi))

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