relfinrank_comap_comap_eq_relfinrank_of_surjective

English

For a surjective f, the finite rank (nat-valued) of the preimages equals the finite rank of the originals: relfinrank(f^{-1}(A), f^{-1}(B)) = relfinrank(A,B).

Русский

Пусть f сюръективно. Тогда натуральный ранг прообразов равен рангу самих подполей: relfinrank(f^{-1}(A), f^{-1}(B)) = relfinrank(A,B).

LaTeX

$$$\\operatorname{relfinrank}(f^{-1}(A), f^{-1}(B)) = \\operatorname{relfinrank}(A,B)\\quad(\\text{при сюръективности } f).$$$

Lean4

theorem relfinrank_comap_comap_eq_relfinrank_of_surjective (f : L →+* 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))

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