rel_π₁ — Mathlib

English

If i1 is related to i1' in the first index set by c1, then the two indices obtained by pairing with any i2 via π lie in the same relation in c12: c12.Rel(π(i1,i2), π(i1',i2)).

Русский

Если элементы i1 и i1' связаны в первом множестве индексов, то пары (i1,i2) и (i1',i2), полученные через отображение π, занимают связанные позиции в c12.

LaTeX

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

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