rank_add_le — Mathlib

English

The rank of the composition g ∘ f is bounded by the rank of f in the lifted sense.

Русский

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

LaTeX

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

Lean4

theorem rank_add_le (f g : V →ₗ[K] V') : rank (f + g) ≤ rank f + rank g :=
  calc
    rank (f + g) ≤ Module.rank K (LinearMap.range f ⊔ LinearMap.range g : Submodule K V') :=
      by
      refine Submodule.rank_mono ?_
      exact
        LinearMap.range_le_iff_comap.2 <|
          eq_top_iff'.2 fun x =>
            show f x + g x ∈ (LinearMap.range f ⊔ LinearMap.range g : Submodule K V') from
              mem_sup.2 ⟨_, ⟨x, rfl⟩, _, ⟨x, rfl⟩, rfl⟩
    _ ≤ rank f + rank g := Submodule.rank_add_le_rank_add_rank _ _

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