image_preimage — Mathlib

English

For a uniform equivalence h, the image of the preimage equals the original set.

Русский

Для равномерного эквивалентного отображения h образ предобраза равен исходному множеству.

LaTeX

$$$\\forall {\\alpha \;\\beta} [UniformSpace \\alpha] [UniformSpace \\beta] (h : \\alpha \\simeq_u \\beta) (s : Set \\alpha),\\; image(preimage(h, s)) = s$$$

Lean4

@[simp]
theorem image_preimage (h : α ≃ᵤ β) (s : Set β) : h '' (h ⁻¹' s) = s :=
  h.toEquiv.image_preimage s

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