relrank_mul_relrank_eq_inf_relrank

English

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

Русский

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

LaTeX

$$$A \\le B \\implies A.{\\rm relrank}(B \\sqcap C) \\cdot B.{\\rm relrank}(C) = A.{\\rm relrank}(C).$$$

Lean4

theorem relrank_mul_relrank_eq_inf_relrank (h : B ≤ C) : relrank A B * relrank B C = (A ⊓ B).relrank C := by
  simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

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