rank_comp_le — Mathlib

English

For linear maps f and g, the rank of their sum is bounded by the sum of their ranks.

Русский

Для линейных отображений f и g ранг их суммы ограничен суммой их рангов.

LaTeX

$$rank (f + g) ≤ rank f + rank g$$

Lean4

/-- The rank of the composition of two maps is less than the minimum of their ranks.

See `lift_rank_comp_le` for the universe-polymorphic version. -/
theorem rank_comp_le (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ min (rank f) (rank g) := by
  simpa only [Cardinal.lift_id] using lift_rank_comp_le g f

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