image_symm_image — Mathlib

English

Let e be a bijection between α and β. Then for any subset S of β, the image of the inverse image of S under e.symm equals S.

Русский

Пусть e — биекция между α и β. Тогда для любого подмножества S ⊆ β образ прообраза S по e^{-1} равен S.

LaTeX

$$$ e '' (e^{-1}[S]) = S $$$

Lean4

@[simp]
theorem image_symm_image {α β} (e : α ≃ β) (s : Set β) : e '' (e.symm '' s) = s :=
  e.symm.symm_image_image s

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