piLTProj_intro

Mathlib.Order.DirectedInverseSystem

URI: https://scilib.ai/kg/mathlib#InverseSystem.piLTProj_intro

English

For a given l placed below i, piLTProj h f equals the evaluation at the projection point.

Русский

Для заданного l, лежащего ниже i, piLTProj h f равен вычислению на точке проекции.

LaTeX

$$$\\piLTProj\\; h\\; f\\; l = f\\; \\langle l.val, h \\rangle$$$

Lean4

theorem piLTProj_intro {l : Iio j} {f : piLT X j} (hl : l < i) : f l = piLTProj h f ⟨l, hl⟩ :=
  rfl

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

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

Разделы

Аффилиация

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