orderEmbOfCardLe_mem

Mathlib.Data.Finset.Sort

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

← MathLib Explorer

English

If k ≤ card(s) and a ∈ Fin k, then orderEmbOfCardLe s h a ∈ s.

Русский

При k ≤ |s| и любом a ∈ Fin k верно, что orderEmbOfCardLe s h a ∈ s.

LaTeX

$$orderEmbOfCardLe\,s\,h\,a \in s$$

Lean4

theorem orderEmbOfCardLe_mem (s : Finset α) {k : ℕ} (h : k ≤ s.card) (a) : orderEmbOfCardLe s h a ∈ s := by
  simp only [orderEmbOfCardLe, RelEmbedding.coe_trans, Finset.orderEmbOfFin_mem, Function.comp_apply]

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

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

Разделы

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

Аффилиация

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