lift_relrank_map_map — Mathlib

English

For f: E →ₐ[F] L, the lifted relrank of (A.map f) against (B.map f) equals the lifted relrank of A against B.

Русский

Для f: E →ₐ[F] L, поднятый relrank (A.map f) против (B.map f) равен поднятому relrank(A,B).

LaTeX

$$$\operatorname{lift}(\operatorname{relrank}(A.map f, B.map f)) = \operatorname{lift}(\operatorname{relrank}(A, B))$$$

Lean4

theorem lift_relrank_map_map (f : E →ₐ[F] L) :
    Cardinal.lift.{v} (relrank (A.map f) (B.map f)) = Cardinal.lift.{w} (relrank A B) := by
  rw [← lift_relrank_comap, comap_map]

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