preimage_setOf_dist — Mathlib

English

For an isometry f, for any x and predicate p on distances, f^{-1} of {y | p(dist(y, f(x)))} equals {y | p(dist(y, x))}.

Русский

Для изометрии f и любого x и predication p по расстоянию выполняется равенство прообраза множества {y | p(dist(y, f(x)))} и множества {y | p(dist(y, x))}.

LaTeX

$$$\forall x\,\forall p:\, \mathbb{R} \to \mathrm{Prop},\ f^{-1}(\{y\mid p(\mathrm{dist}(y, f(x)))\}) = \{y\mid p(\mathrm{dist}(y, x))\}$$$

Lean4

theorem preimage_setOf_dist (hf : Isometry f) (x : α) (p : ℝ → Prop) :
    f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)} := by simp [hf.dist_eq]

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