map_valEmbedding_univ — Mathlib

English

Under the standard embedding of Fin n into natural numbers, the image of all elements is {0,1,...,n-1}.

Русский

Под стандартным вложением Fin n в натуральные числа образ всей множества Fin n равен {0,1,...,n-1}.

LaTeX

$$$ \\mathrm{Finset.map}(\\mathrm{Fin.valEmbedding}, \\mathrm{Finset.univ}) = \\mathrm{Finset.Iio}(n) $$$

Lean4

theorem map_valEmbedding_univ : (Finset.univ : Finset (Fin n)).map Fin.valEmbedding = Iio n :=
  by
  ext
  simp [orderIsoSubtype.symm.surjective.exists, OrderIso.symm]

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