lift_relrank_comap_comap_eq_lift_relrank_of_surjective

English

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

Русский

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

LaTeX

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

Lean4

theorem lift_relrank_comap_comap_eq_lift_relrank_of_surjective (f : L →ₐ[F] E) (h : Function.Surjective f) :
    Cardinal.lift.{v} (relrank (A.comap f) (B.comap f)) = Cardinal.lift.{w} (relrank A B) :=
  lift_relrank_comap_comap_eq_lift_relrank_of_le A B f fun x _ ↦ h x

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