eqOn_comp_right_iff — Mathlib

English

The equality of compositions is equivalent to equality on the right after precomposing with f.

Русский

Равенство композиции эквивалентно равенству справа после прекомпозиции через f.

LaTeX

$$$ s.EqOn (g_1\circ f) (g_2\circ f) \iff (f''s).EqOn g_1 g_2 $$$

Lean4

theorem eqOn_comp_right_iff : s.EqOn (g₁ ∘ f) (g₂ ∘ f) ↔ (f '' s).EqOn g₁ g₂ :=
  (s.surjOn_image f).cancel_right <| s.mapsTo_image f

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