English
For congruences c ≤ d on M, and x in M, the induced map c.map d h x equals c.lift d.mk' with the witness derived from h.
Русский
Для конгруэнций c ≤ d и элемента x по M, индуцированное отображение c.map d h x равно c.lift d.mk' с доказательством на основе h.
LaTeX
$$$c.map d h x = c.lift d.mk' (fun _ _ hc => d.eq.2 (h hc)) x$$$
Lean4
/-- Given congruence relations `c, d` on a monoid such that `d` contains `c`, the definition of
the homomorphism from the quotient by `c` to the quotient by `d` induced by `d`'s quotient map. -/
@[to_additive /-- Given additive congruence relations `c, d` on an `AddMonoid` such that `d`
contains `c`, the definition of the homomorphism from the quotient by `c` to the quotient by `d`
induced by `d`'s quotient map. -/
]
theorem map_apply {c d : Con M} (h : c ≤ d) (x) : c.map d h x = c.lift d.mk' (fun _ _ hc => d.eq.2 <| h hc) x :=
rfl
