relfinrank_comap_comap_eq_relfinrank_of_surjective

English

For surjective f, relfinrank(A.comap f, B.comap f) = relfinrank A B.

Русский

Для сюръективного f, relfinrank(A.comap f, B.comap f) = relfinrank A B.

LaTeX

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

Lean4

theorem relfinrank_comap_comap_eq_relfinrank_of_surjective (f : L →ₐ[F] E) (h : Function.Surjective f) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A B := by
  simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h))

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