English
If r is an equivalence and f is surjective and ker(f) respects r, then Map r f f is an equivalence.
Русский
Если r — эквивалентность, f сюръективно, и ядро f сохраняет r, то Map r f f — эквивалентность.
LaTeX
$$$\forall r:\alpha\to\alpha\to \mathrm{Prop},\; \mathrm{Equivalence}(r) \to \forall f:\alpha\to \beta,\; \mathrm{Surjective}(f) \to (\forall x,y, f x = f y \Rightarrow r x y) \Rightarrow \mathrm{Equivalence}(\mathrm{Map}(r,f,f))$$$
Lean4
theorem map_equivalence {r : α → α → Prop} (hr : Equivalence r) (f : α → β) (hf : f.Surjective)
(hf_ker : ∀ x y, f x = f y → r x y) : Equivalence (Relation.Map r f f)
where
refl := map_reflexive hr.reflexive hf
symm := @(map_symmetric hr.symmetric _)
trans :=
@(map_transitive hr.transitive hf_ker)
-- TODO: state this using `≤`, after adjusting imports.
