lift_relrank_comap_comap_eq_lift_relrank_of_le

English

As above, the lift-relrank-comap-comap-inf relation holds: lift(relrank(A.comap f, B.comap f)) = lift(relrank(A, B ⊓ f.fieldRange)).

Русский

Как выше: подъём relrank(A.comap f, B.comap f) равен подъёму relrank(A, B ⊓ f.fieldRange).

LaTeX

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

Lean4

theorem lift_relrank_comap_comap_eq_lift_relrank_of_le (f : L →+* E) (h : B ≤ f.fieldRange) :
    lift.{v} (relrank (A.comap f) (B.comap f)) = 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

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