condition — Mathlib

English

Let K be a multifork of a multicospan I. For every b in the index J, the two composites K.ι (J.fst b) followed by I.fst b and K.ι (J.snd b) followed by I.snd b are equal. In other words, the two legs of the multifork commute with the corresponding arrows of I.

Русский

Пусть K является мультфорком для мультиспана I. Для каждого b из индекса J два отображения K.ι (J.fst b) ; I.fst b и K.ι (J.snd b) ; I.snd b совпадают. Другими словами, две ветви мультфорка коммутируют с соответствующими стрелками I.

LaTeX

$$$\forall b,\ K.\iota (J.fst\,b) \; \circ\; I.fst\,b = K.\iota (J.snd\,b) \; \circ\; I.snd\,b$$$

Lean4

@[reassoc (attr := simp)]
theorem condition (b) : K.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b := by
  rw [← app_right_eq_ι_comp_fst, ← app_right_eq_ι_comp_snd]

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