iccLeftChart_extend_zero

Mathlib.Geometry.Manifold.Instances.Real

URI: https://scilib.ai/kg/mathlib#iccLeftChart_extend_zero

English

For x<y, and p in Icc(x,y), the extension at 0 equals p_0 − x.

Русский

Для x<y и p ∈ Icc(x,y) расширение на 0 равно p_0 − x.

LaTeX

$$$\\forall x,y \\in \\mathbb{R}, [hxy: x

Lean4

theorem iccLeftChart_extend_zero {p : Set.Icc x y} : (IccLeftChart x y).extend (𝓡∂ 1) p 0 = p.val - x :=
  rfl

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

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

Разделы

Аффилиация

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