orderEmbOfFin_mem

Mathlib.Data.Finset.Sort

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

English

For every i ∈ Fin k, the image s.orderEmbOfFin h i belongs to s.

Русский

Для любого i ∈ Fin k образ изображения s.orderEmbOfFin h i принадлежит s.

LaTeX

$$$s.orderEmbOfFin\,h\,i \in s$$$

Lean4

@[simp]
theorem orderEmbOfFin_mem (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) : s.orderEmbOfFin h i ∈ s :=
  (s.orderIsoOfFin h i).2

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

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

Разделы

Аффилиация

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