mapOfSurjective_eq_mapGen — Mathlib

English

If c ≤ ker f and f is surjective, then the congruence mapGen f coincides with mapOfSurjective f h hf.

Русский

Если c ≤ ker f и f сюрьективно, тогда отображение mapGen f совпадает с mapOfSurjective f h hf.

LaTeX

$$$c.mapGen f = c.mapOfSurjective f h hf$$$

Lean4

/-- A specialization of 'the smallest congruence relation containing a congruence relation `c`
equals `c`'. -/
@[to_additive /-- A specialization of 'the smallest additive congruence relation containing
    an additive congruence relation `c` equals `c`'. -/
    ]
theorem mapOfSurjective_eq_mapGen {c : Con M} {f : F} (h : ker f ≤ c) (hf : Surjective f) :
    c.mapGen f = c.mapOfSurjective f h hf := by rw [← conGen_of_con (c.mapOfSurjective f h hf)]; rfl

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