rank_lt_of_rel — Mathlib

English

Given a relation r and an element b with Acc r b, if a is related to b (r a b), then rank_r(a) < rank_r(b).

Русский

Пусть есть отношение r и элемент b с Acc r b. Если a связано с b (r a b), то rank_r(a) < rank_r(b).

LaTeX

$$$r(a,b) \Rightarrow \operatorname{rank}_r(a) < \operatorname{rank}_r(b)$$$

Lean4

/-- if `r a b` then the rank of `a` is less than the rank of `b`. -/
theorem rank_lt_of_rel (hb : Acc r b) (h : r a b) : (hb.inv h).rank < hb.rank :=
  (Order.lt_succ _).trans_le <| by
    rw [hb.rank_eq]
    exact Ordinal.le_iSup _ (⟨a, h⟩ : { a // r a b })

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