preimage_image — Mathlib

English

Let h: α ≃ᵤ β be a uniform equivalence. Then the preimage of the image of a set s equals s.

Русский

Пусть h: α ≃ᵤ β — равномерное эквивалентство. Тогда предобраз образа множества s равен s.

LaTeX

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

Lean4

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

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