map_orderEmbOfFin_univ — Mathlib

English

The image of Finset.univ under the embedding s.orderEmbOfFin h, when mapped via toEmbedding, equals s.

Русский

Образ Finset.univ через вложение s.orderEmbOfFin h сопоставляется с s через toEmbedding.

LaTeX

$$$\mathrm{map}(s.orderEmbOfFin\,h).toEmbedding\,\mathrm{Finset.univ} = s$$$

Lean4

@[simp]
theorem map_orderEmbOfFin_univ (s : Finset α) {k : ℕ} (h : s.card = k) :
    Finset.map (s.orderEmbOfFin h).toEmbedding Finset.univ = s := by simp [map_eq_image]

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