English
If s = s1 and signs = signs1, then s.exsphere signs = s1.exsphere signs1.
Русский
Если s = s1 и signs = signs1, то s.exsphere signs = s1.exsphere signs1.
LaTeX
$$s.exsphere signs = s1.exsphere signs1 whenever s = s1 and signs = signs1$$
Lean4
/-- The exsphere with signs determined by the given set of indices (for the empty set, this is
the insphere; for a singleton set, this is the exsphere opposite a vertex). This is only
meaningful if `s.ExcenterExists`; otherwise, it is a sphere of radius zero at some arbitrary
point. -/
def exsphere (signs : Finset (Fin (n + 1))) : Sphere P
where
center := Finset.univ.affineCombination ℝ s.points (s.excenterWeights signs)
radius := |(∑ i, s.excenterWeightsUnnorm signs i)⁻¹|
