image_congr — Mathlib

English

If f and g agree on every element of s, then their images of s are equal: f''s = g''s.

Русский

Если функции f и g согласованы на каждом элементе множества s, то их образы множества s совпадают: f''s = g''s.

LaTeX

$$$ (\\forall a \\in s, f(a) = g(a)) \\Rightarrow f''s = g''s. $$$

Lean4

@[congr]
theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a ∈ s, f a = g a) : f '' s = g '' s := by aesop

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