max_eq_o_cons_tail'

Mathlib.Topology.Category.Profinite.Nobeling.Successor

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.Products.max_eq_o_cons_tail'

← MathLib Explorer

English

The head of a maximal product equals term I ho.

Русский

Голова максимального продукта равна term I ho.

LaTeX

$$$ l.head! = term I ho $$$

Lean4

theorem max_eq_o_cons_tail' [Inhabited I] (l : Products I) (hl : l.val ≠ []) (hlh : l.val.head! = term I ho)
    (hlc : List.IsChain (· > ·) (term I ho :: l.Tail.val)) : l = ⟨term I ho :: l.Tail.val, hlc⟩ := by
  simp_rw [← max_eq_o_cons_tail ho l hl hlh, Subtype.coe_eta]

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

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

Разделы

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

Аффилиация

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