card_fin_lt_of_le — Mathlib

English

For m ≤ n, the set { i : Fin n | i < m } has cardinality m.

Русский

Для m ≤ n множество { i : Fin n | i < m } имеет кардинальность m.

LaTeX

$$$m \le n \Rightarrow \operatorname{card} \{ i : \mathrm{Fin}(n) \; | \; i < m \} = m$$$

Lean4

theorem card_fin_lt_of_le {m n : ℕ} (h : m ≤ n) : Fintype.card { i : Fin n // i < m } = m :=
  by
  conv_rhs => rw [← Fintype.card_fin m]
  apply Fintype.card_congr
  exact
    { toFun := fun ⟨⟨i, _⟩, hi⟩ ↦ ⟨i, hi⟩
      invFun := fun ⟨i, hi⟩ ↦ ⟨⟨i, lt_of_lt_of_le hi h⟩, hi⟩ }

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