preimage_congr — Mathlib

English

If two functions agree pointwise, their preimages of any set are equal.

Русский

Если две функции совпадают по значению на каждом аргументе, их обратные образы множества совпадают.

LaTeX

$$$(\forall x, f(x) = g(x)) \Rightarrow f^{-1}(S) = g^{-1}(S).$$$

Lean4

theorem preimage_congr {f g : α → β} {s : Set β} (h : ∀ x : α, f x = g x) : f ⁻¹' s = g ⁻¹' s :=
  by
  congr with x
  simp [h]

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