eq_condition — Mathlib

English

For morphisms f, f' : j ⟶ j' in a cofiltered category, the canonical equation eqHom f f' ≫ f = eqHom f f' ≫ f' holds.

Русский

Для морфизмов f, f' : j ⟶ j' в кофильтрованной категории выполняется равенство eqHom f f' ≫ f = eqHom f f' ≫ f'.

LaTeX

$$$$ \\mathrm{eqHom}(f,f') \\;\\gg\\; f \;=\\; \\mathrm{eqHom}(f,f') \\;\\gg\\; f'. $$$$

Lean4

/-- `eq_condition f f'`, for morphisms `f f' : j ⟶ j'`, is the proof that
`eqHom f f' ≫ f = eqHom f f' ≫ f'`.
-/
@[reassoc] -- Not `@[simp]` as it does not fire.

theorem eq_condition {j j' : C} (f f' : j ⟶ j') : eqHom f f' ≫ f = eqHom f f' ≫ f' :=
  (IsCofilteredOrEmpty.cone_maps f f').choose_spec.choose_spec

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