card_le_card_of_le — Mathlib

English

If N ≤ O are submodules and b is a basis of O, b' a basis of N, then card ι' ≤ card ι.

Русский

Если N ≤ O — подмодули, и b базис O, b' базис N, то |ι'| ≤ |ι|.

LaTeX

$$|\\iota'| \\le |\\iota|$$

Lean4

theorem card_le_card_of_le {N O : Submodule R M} (hNO : N ≤ O) [Fintype ι] (b : Basis ι R O) [Fintype ι']
    (b' : Basis ι' R N) : Fintype.card ι' ≤ Fintype.card ι :=
  b.card_le_card_of_linearIndependent (b'.linearIndependent.map_injOn (inclusion hNO) (N.inclusion_injective _).injOn)

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