lift_rank_comp_le — Mathlib

English

The rank of the composition f ∘ g is bounded by the minimum of the ranks of f and g (universe-adjusted).

Русский

Ранг композиции f ∘ g ограничен минимумом рангов f и g (с учётом переноса по вселенной).

LaTeX

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

Lean4

/-- The rank of the composition of two maps is less than the minimum of their ranks. -/
theorem lift_rank_comp_le (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
    Cardinal.lift.{v'} (rank (f.comp g)) ≤ min (Cardinal.lift.{v'} (rank f)) (Cardinal.lift.{v''} (rank g)) :=
  le_min (Cardinal.lift_le.mpr <| rank_comp_le_left _ _) (lift_rank_comp_le_right _ _)

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