finrank_range_le_card — Mathlib

English

The rank of the range of a map b is bounded by the domain size: (Set.range b).finrank ≤ card(domain).

Русский

Ранг образа отображения b ограничен размерностью области определения: finrank(Set.range b) ≤ card( domain ).

LaTeX

$$$ \\operatorname{finrank} R (\\operatorname{Set.range} b) ≤ Fintype.card ι. $$$

Lean4

theorem finrank_range_le_card {ι : Type*} [Fintype ι] (b : ι → M) : (Set.range b).finrank R ≤ Fintype.card ι := by
  classical
  refine (finrank_span_le_card _).trans ?_
  rw [Set.toFinset_range]
  exact Finset.card_image_le

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