relfinrank_comap_comap_eq_relfinrank_inf

English

Relfinrank of A.comap f and B.comap f equals relfinrank of A and B ⊓ f.fieldRange.

Русский

Relfinrank(A.comap f, B.comap f) = relfinrank(A, B ⊓ f.fieldRange).

LaTeX

$$$ \operatorname{relfinrank}(A.comap f, B.comap f) = \operatorname{relfinrank}(A, B \cap f.fieldRange)$$$

Lean4

theorem relfinrank_comap_comap_eq_relfinrank_inf (f : L →+* E) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A (B ⊓ f.fieldRange) := by
  simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_inf A B f))

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