neZero_partSize

Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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

English

For every i in Fin c.length, c.partSize(i) ≠ 0.

Русский

Для каждого i из Fin(c.length) величина c.partSize(i) не равна нулю.

LaTeX

$$$\\forall i:\\mathrm{Fin}(c.length),\\; \\mathrm{NeZero}(c.partSize(i))$$$

Lean4

theorem neZero_partSize (c : OrderedFinpartition n) (i : Fin c.length) : NeZero (c.partSize i) :=
  .of_pos (c.partSize_pos i)

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

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

Разделы

Аффилиация

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