eqOn_range — Mathlib

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

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