prev_π₂ — Mathlib

English

Similarly to next, the prev map along π commutes with the relation on i2: prev(π(i1,i2')) = π(i1,i2).

Русский

Аналогично следующему, предыдущее отображение через π совместимо с отношением на i2: prev(π(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}.prev(\\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 prev_π₂ (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') : c₁₂.prev (π c₁ c₂ c₁₂ ⟨i₁, i₂'⟩) = π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ :=
  c₁₂.prev_eq' (rel_π₂ c₁ c₁₂ i₁ h)

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