compClosure_eq_self — Mathlib

English

Under Congruence assumptions, for any X,Y and morphisms f,g: X ⟶ Y, CompClosure r f g holds exactly when r f g holds.

Русский

При условии существования конгруэнции r, для любых f,g: X ⟶ Y, CompClosure r f g эквивалентно r f g.

LaTeX

$$$\forall X,Y:\; \mathrm{Hom}_C(X,Y),\; \forall f,g:\; X\to Y,\; CompClosure(r,f,g) \iff r f g.$$$

Lean4

@[simp]
theorem compClosure_eq_self [h : Congruence r] : CompClosure r = r :=
  by
  ext
  simp only [compClosure_iff_self]

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