lift_relrank_comap_comap_eq_lift_relrank_of_le

English

If B ≤ f.fieldRange, then lift(relrank(A.comap f, B.comap f)) = lift(relrank A B).

Русский

Если B ≤ f.fieldRange, то поднятый relrank(A.comap f, B.comap f) равен поднятому relrank(A, B).

LaTeX

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

Lean4

theorem lift_relrank_comap_comap_eq_lift_relrank_of_le (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
    Cardinal.lift.{v} (relrank (A.comap f) (B.comap f)) = Cardinal.lift.{w} (relrank A B) := by
  simpa only [inf_of_le_left h] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

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