neZero_length

Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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

English

If n is nonzero, then c.length is nonzero: NeZero n ⇒ NeZero c.length.

Русский

Если n не равно нулю, то и длина разбиения не равна нулю.

LaTeX

$$$[\\text{NeZero } n] \\Rightarrow \\mathrm{NeZero}(c.length)$$$

Lean4

theorem neZero_length [NeZero n] (c : OrderedFinpartition n) : NeZero c.length :=
  ⟨(c.length_pos pos').ne'⟩

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

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

Разделы

Аффилиация

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