relfinrank_map_map — Mathlib

English

Relfinrank is preserved under the map operation: relfinrank(A.map f, B.map f) = relfinrank(A,B).

Русский

Relfinrank сохраняется под отображением: relfinrank(A.map f, B.map f) = relfinrank(A,B).

LaTeX

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

Lean4

theorem relfinrank_map_map (f : E →ₐ[F] L) : relfinrank (A.map f) (B.map f) = relfinrank A B := by
  simpa using congr(toNat $(lift_relrank_map_map A B f))

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