preimage_perpBisector — Mathlib

English

If f is an isometry, then the preimage under f of the perpBisector of f(p1),f(p2) equals the perpBisector of p1,p2.

Русский

Если f — изометрия, то предобраз f-биссектора от f(p1),f(p2) совпадает с бисектором p1,p2.

LaTeX

$$$f^{-1}(\perpBisector(f(p_1),f(p_2))) = \perpBisector(p_1,p_2)$$$

Lean4

theorem preimage_perpBisector {f : P → P'} (h : Isometry f) (p₁ p₂ : P) :
    f ⁻¹' (perpBisector (f p₁) (f p₂)) = perpBisector p₁ p₂ := by ext x; simp [mem_perpBisector_iff_dist_eq, h.dist_eq]

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