map_def

Mathlib.Order.DirectedInverseSystem

URI: https://scilib.ai/kg/mathlib#DirectLimit.map_def

English

Explicitly, the value of map on elements from the same index i agrees with ih: map i x y equals ih i x y.

Русский

Явно: для элементов из одного индекса i отображение map_def даёт ih i x y.

LaTeX

$$$\\mathrm{map\\_def}\\; (i\\; x\\; y) : \\mathrm{map\\_2}\\; \\text{...} = \\mathrm{ih\\_i}(x,y)$$$

Lean4

theorem map_def (x) : map f₁ f₂ ih compat ⟦x⟧ = ⟦⟨x.1, ih x.1 x.2⟩⟧ :=
  rfl

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

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

Разделы

Аффилиация

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