image_congr — Mathlib

English

If two functions f and g coincide on s (as sets), then their images of s are equal: image f s = image g s.

Русский

Если f и g совпадают на s (как на множестве), то их образы множества s совпадают: image f s = image g s.

LaTeX

$$$\\text{Set.EqOn } f g \; s \\Rightarrow \\operatorname{image}(f,s) = \\operatorname{image}(g,s)$$$

Lean4

theorem image_congr (h : (s : Set α).EqOn f g) : Finset.image f s = Finset.image g s :=
  by
  ext
  simp_rw [mem_image, ← bex_def]
  exact exists₂_congr fun x hx => by rw [h hx]

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