relfinrank_mul_relfinrank_eq_inf_relfinrank

English

If B ≤ C, then relfinrank A B · relfinrank B C = (A ⊓ B).relfinrank C.

Русский

Если B ≤ C, то relfinrank A B умножить на relfinrank B C равно (A ⊓ B).relfinrank C.

LaTeX

$$$\\text{If } B \\le C,\\; \\operatorname{relfinrank}(A,B) \\cdot \\operatorname{relfinrank}(B,C) = (A \\cap B).\\operatorname{relfinrank}(C).$$$

Lean4

theorem relfinrank_mul_relfinrank_eq_inf_relfinrank (h : B ≤ C) :
    relfinrank A B * relfinrank B C = (A ⊓ B).relfinrank C := by
  simpa using congr(toNat $(relrank_mul_relrank_eq_inf_relrank A h))

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