addNSMul_zero

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#Set.Icc.addNSMul_zero

English

The zeroth term of addNSMul is a.

Русский

0-й член последовательности addNSMul равен a.

LaTeX

$$addNSMul h δ 0 = a$$

Lean4

theorem addNSMul_zero : addNSMul h δ 0 = a := by rw [addNSMul, zero_smul, add_zero, projIcc_left]

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

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

Разделы

Аффилиация

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