English
Equality-on on the range of a function f is equivalent to equality of the compositions with f: g1 ∘ f = g2 ∘ f if and only if g1 and g2 agree on range(f).
Русский
Согласие функций g1 и g2 на образе функции f эквивалентно равенству композиций: g1 ∘ f = g2 ∘ f тогда и только тогда, когда g1 и g2 согласны на image(f).
LaTeX
$$$ EqOn\\ g_1\\ g_2\\ (range\\ f) \\; \\iff \\; g_1 \\circ f = g_2 \\circ f $$$
Lean4
@[simp]
theorem eqOn_range {ι : Sort*} {f : ι → α} {g₁ g₂ : α → β} : EqOn g₁ g₂ (range f) ↔ g₁ ∘ f = g₂ ∘ f :=
forall_mem_range.trans <| funext_iff.symm