next_π₁ — Mathlib

English

The next-index function respects the π-map: applying next to the pair (i1,i2) with i1 related to i1' yields the same result as using i1'.

Русский

Функция следующего индекса сохраняет отображение π: применение next к ⟨i1,i2⟩ даёт такое же значение, как если бы использовали ⟨i1',i2⟩, если i1 связано с i1'.

LaTeX

$$$\\forall {i_1,i_1'\\in I_1}\\; (c_1.Rel(i_1,i_1')) \\Rightarrow c_{12}.next(\\pi(c_1,c_2,c_{12})(\\langle i_1,i_2\\rangle))=\\pi(c_1,c_2,c_{12})(\\langle i_1',i_2\\rangle)$$$

Lean4

theorem next_π₁ {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) : c₁₂.next (π c₁ c₂ c₁₂ ⟨i₁, i₂⟩) = π c₁ c₂ c₁₂ ⟨i₁', i₂⟩ :=
  c₁₂.next_eq' (rel_π₁ c₂ c₁₂ h i₂)

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