isInitSeg_initSeg

Mathlib.Combinatorics.Colex

URI: https://scilib.ai/kg/mathlib#Finset.Colex.isInitSeg_initSeg

← MathLib Explorer

English

IsInitSeg (initSeg s) (card s).

Русский

IsInitSeg( initSeg s ) (card s).

LaTeX

$$$IsInitSeg(initSeg(s), card(s))$$$

Lean4

theorem isInitSeg_initSeg : IsInitSeg (initSeg s) #s :=
  by
  refine ⟨fun t ht => (mem_initSeg.1 ht).1.symm, fun t₁ t₂ ht₁ ht₂ ↦ mem_initSeg.2 ⟨ht₂.2.symm, ?_⟩⟩
  rw [mem_initSeg] at ht₁
  exact ht₂.1.le.trans ht₁.2

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

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

Разделы

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

Аффилиация

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