English
The lift on the quotient composed with the base function equals the base function on representatives: Con.liftOn (x : c.Quotient) f h = f x.
Русский
Подъем на фактор через функцию совпадает с самой функцией на представителях: Con.liftOn (x : c.Quotient) f h = f x.
LaTeX
$$$Con.liftOn (x : c.Quotient)\\ f\\ h = f x$$$
Lean4
/-- Definition of the function on the quotient by a congruence relation `c` induced by a function
that is constant on `c`'s equivalence classes. -/
@[to_additive (attr := simp) /-- Definition of the function on the quotient by an additive
congruence relation `c` induced by a function that is constant on `c`'s equivalence classes. -/
]
protected theorem liftOn_coe {β} (c : Con M) (f : M → β) (h : ∀ a b, c a b → f a = f b) (x : M) :
Con.liftOn (x : c.Quotient) f h = f x :=
rfl
