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

$$$ B \le C \Rightarrow \operatorname{relfinrank} A B \cdot \operatorname{relfinrank} B C = (A \cap B).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))

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