rel_π₂ — Mathlib

English

If i2 is related to i2' in the second index set, then π(i1,i2) and π(i1,i2') are related in c12 for any fixed i1.

Русский

Если i2 связано с i2' во втором наборе индексов, то для фиксированного i1 пары π(i1,i2) и π(i1,i2') связаны в c12.

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}.Rel(\\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 rel_π₂ (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') : c₁₂.Rel (π c₁ c₂ c₁₂ ⟨i₁, i₂⟩) (π c₁ c₂ c₁₂ ⟨i₁, i₂'⟩) :=
  TotalComplexShape.rel₂ i₁ h

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