Triangle interior and its circumsphere

Stream: mathlib4

[Gaolei He]

Any idea of proving that a point P inside a triangle is also inside the triangle's circumsphere?
Here's the lean code statement

import Mathlib
open Affine Module

variable {V : Type*} {Pt : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
  [NormedAddTorsor V Pt] [Fact (finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)]

lemma mem_interior_triangle_imp_power_neg
  {A B C P : Pt} (hABC : AffineIndependent ℝ ![A, B, C])
  (h_triABC : triABC = (⟨_, hABC⟩ : Triangle ℝ Pt))
  (hP : P ∈ triABC.interior) (hΓ : Γ = triABC.circumsphere):
  Γ.power P < 0 := by

  sorry

[Jovan Gerbscheid]

This sounds like a special case of some convexity result. If a set S (in this case {A, B, C}) is a subset of a ball, (or disc) then the convex hull of S is also a subset of the sphere. I don't know where to find this lemma though :sweat_smile:

[Joseph Myers]

For two points in an affine space for a strictly convex space, the relevant results are docs#Sbtw.dist_lt_max_dist and docs#Wbtw.dist_le_max_dist which are both deduced from docs#norm_combo_lt_of_ne for two vectors in a strictly convex space. I suggest adding versions of all three lemmas to mathlib for an affine combination (with nonnegative weights) of any finite number of points or vectors (note that for strict inequality, it suffices that at least two of the weights are positive, you don't need all of them positive); those could be deduced from the two-point or two-vector lemmas by induction.

[Joseph Myers]

I found I wanted something like this for my work on IMO 2024 P4. #31452 now has what I think are the right convexity statements about convex combinations in strictly convex sets and spaces (depends on #31450 and #31451).