relfinrank_eq_toNat_relrank — Mathlib

English

The Nat version of the relative rank equals the nat value of the cardinal relative rank: relfinrank A B = toNat (relrank A B).

Русский

Nat-версия относительного ранга равна значению Nat кардинала relrank A B: relfinrank A B = toNat (relrank A B).

LaTeX

$$$\\mathrm{relfinrank}\\,A\\,B = \\operatorname{toNat}(\\mathrm{relrank}\\,A\\,B)$$$

Lean4

theorem relfinrank_eq_toNat_relrank : relfinrank A B = toNat (relrank A B) :=
  rfl

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