English
The image of the sphere under inversion with center c and radius R is the union of the center c and the perpBisector of c and inv(c,R)y translated to the inverted center.
Русский
Образ сферы под инверсией с центром c и радиусом R — это объединение точки c и перп биссектора c и inv(c,R)y, сдвинутого к инвертированному центру.
LaTeX
$$$$ \mathrm{image}(\mathrm{inversion}(c,R), \mathrm{sphere}(y, \operatorname{dist}(y,c))) = \mathrm{insert}\, c (\perpBisector(c, \mathrm{inversion}(c,R)\,y)). $$$$
Lean4
/-- The Monge point of an (n+2)-simplex, in terms of
`pointsWithCircumcenter`. -/
theorem mongePoint_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ} (s : Simplex ℝ P (n + 2)) :
s.mongePoint =
(univ : Finset (PointsWithCircumcenterIndex (n + 2))).affineCombination ℝ s.pointsWithCircumcenter
(mongePointWeightsWithCircumcenter n) :=
by
rw [mongePoint_eq_smul_vsub_vadd_circumcenter, centroid_eq_affineCombination_of_pointsWithCircumcenter,
circumcenter_eq_affineCombination_of_pointsWithCircumcenter, affineCombination_vsub, ← LinearMap.map_smul,
weightedVSub_vadd_affineCombination]
congr with i
rw [Pi.add_apply, Pi.smul_apply, smul_eq_mul, Pi.sub_apply]
cases i <;>
simp_rw [centroidWeightsWithCircumcenter, circumcenterWeightsWithCircumcenter,
mongePointWeightsWithCircumcenter] <;>
rw [add_tsub_assoc_of_le (by decide : 1 ≤ 2), (by decide : 2 - 1 = 1)]
· rw [if_pos (mem_univ _), sub_zero, add_zero, card_fin]
field_simp
· simp [field]
ring
