length_pos

Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

URI: https://scilib.ai/kg/mathlib#OrderedFinpartition.length_pos

English

If n > 0, then c.length > 0.

Русский

Если n > 0, то c.length > 0.

LaTeX

$$$0 < n \\Rightarrow 0 < c.length$$$

Lean4

theorem length_pos (h : 0 < n) : 0 < c.length :=
  Nat.zero_lt_of_lt (c.index ⟨0, h⟩).2

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

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

Разделы

Аффилиация

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