lift_rank_comp_le_right — Mathlib

English

The rank of the composition is bounded by the minimum of the ranks of the factors, after lifting to the appropriate universes.

Русский

Ранг композиции ограничен минимумом рангов факторов после подъёма в соответствующие вселенные.

LaTeX

$$rank (f ∘ g) ≤ min (rank f) (rank g)$$

Lean4

theorem lift_rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
    Cardinal.lift.{v'} (rank (f.comp g)) ≤ Cardinal.lift.{v''} (rank g) := by rw [rank, rank, LinearMap.range_comp];
  exact lift_rank_map_le _ _

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