length_le_chainHeight_of_mem_subchain

Mathlib.Order.Height

URI: https://scilib.ai/kg/mathlib#Set.length_le_chainHeight_of_mem_subchain

English

If l ∈ s.subchain, then length(l) ≤ s.chainHeight in ENat.

Русский

Если l ∈ s.subchain, то длина l не превосходит s.chainHeight (в ENat).

LaTeX

$$$ \\text{length}(l)^{↑} \\le s.chainHeight. $$$

Lean4

theorem length_le_chainHeight_of_mem_subchain (hl : l ∈ s.subchain) : ↑l.length ≤ s.chainHeight :=
  le_chainHeight_iff.mpr ⟨l, hl, rfl⟩

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

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

Разделы

Аффилиация

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