English
For any f: α → β, any U ⊆ β×β, and x ∈ α, the ball around x with preimage of U equals the preimage of the ball around f(x) with U: UniformSpace.ball x (Prod.map f f)⁻¹' U = f⁻¹' UniformSpace.ball (f x) U.
Русский
Для отображения f: α → β, множества U ⊆ β×β и точки x ∈ α, окружность вокруг x с помощью предобразного множества U равна предобразному множесту шара вокруг f(x) с U.
LaTeX
$$$\mathrm{UniformSpace.ball}\, x ( (\\Prod.map f f)^{-1}' U) = f^{-1}' \mathrm{UniformSpace.ball} (f x) U$$$
Lean4
theorem ball_preimage {f : α → β} {U : Set (β × β)} {x : α} :
UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U :=
by
ext : 1
simp only [UniformSpace.ball, mem_preimage, Prod.map_apply]
