next_π₂ — Mathlib

English

For fixed i1, the next-π map acts compatibly with a relation h on i2: c12.next(π(i1,i2)) = π(i1,i2').

Русский

При фиксированном i1 отображение next через π совместимо с отношением h на i2: c12.next(π(i1,i2)) = π(i1,i2').

LaTeX

$$$\\forall i_1\\in I_1\\; \\forall {i_2,i_2'\\in I_2}\\; (c_2.Rel(i_2,i_2')) \\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₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') : c₁₂.next (π c₁ c₂ c₁₂ ⟨i₁, i₂⟩) = π c₁ c₂ c₁₂ ⟨i₁, i₂'⟩ :=
  c₁₂.next_eq' (rel_π₂ c₁ c₁₂ i₁ h)

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