image_orderEmbOfFin_univ

Mathlib.Data.Finset.Sort

URI: https://scilib.ai/kg/mathlib#Finset.image_orderEmbOfFin_univ

← MathLib Explorer

English

The image of Finset.univ under the order-embedding s.orderEmbOfFin h is exactly s.

Русский

Образ Finset.univ через порядок-встраивание s.orderEmbOfFin h равен s.

LaTeX

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

Lean4

@[simp]
theorem image_orderEmbOfFin_univ (s : Finset α) {k : ℕ} (h : s.card = k) :
    Finset.image (s.orderEmbOfFin h) Finset.univ = s :=
  by
  apply Finset.coe_injective
  simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru