eq_image_iff_symm_image_eq — Mathlib

English

Let e be a bijection between α and β. For any subsets s ⊆ α and t ⊆ β, t equals the image of s under e if and only if the inverse image of t under e equals s.

Русский

Пусть e — биекция между α и β. Для любых подмножеств s ⊆ α и t ⊆ β выполняется: t является образом s через e тогда и только тогда, когда прообраз t по e равен s.

LaTeX

$$$ t = e[s] \iff e^{-1}[t] = s $$$

Lean4

theorem eq_image_iff_symm_image_eq {α β} (e : α ≃ β) (s : Set α) (t : Set β) : t = e '' s ↔ e.symm '' t = s :=
  (e.symm.injective.image_injective.eq_iff' (e.symm_image_image s)).symm

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