prev_π₁ — Mathlib

English

The previous-index map along π corresponds to the reversed role: applying prev to ⟨i1',i2⟩ recovers ⟨i1,i2⟩ when i1 ~ i1'.

Русский

Предыдущее отображение через π возвращает ⟨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}.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₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) : c₁₂.prev (π c₁ c₂ c₁₂ ⟨i₁', i₂⟩) = π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ :=
  c₁₂.prev_eq' (rel_π₁ c₂ c₁₂ h i₂)

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