Theorems · Definition · geometry

Affine.Simplex.PointsWithCircumcenterIndex.casesOn

{n : ℕ} →
  {motive : Affine.Simplex.PointsWithCircumcenterIndex n → Sort u} →
    (t : Affine.Simplex.PointsWithCircumcenterIndex n) →
      ((a : Fin (n + 1)) → motive (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a)) →
        motive Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex → motive t

Defined in: Mathlib.Geometry.Euclidean.Circumcenter
Cited by: 7 results in Mathlib
Foundations: Depth 10 from the axioms · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Affine.Simplex.PointsWithCircumcenterIndexstatement and proof · cited by 20

Cited by11

Results whose statement or proof uses this declaration.

Affine.Simplex.sum_pointsWithCircumcenterproof · cited by 7
Affine.Simplex.PointsWithCircumcenterIndex.ctorIdxproof · cited by 3
Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenterproof · cited by 2
Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_subproof · cited by 2
Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenterproof · cited by 2
Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenterproof · cited by 1
Affine.Simplex.sum_pointWeightsWithCircumcenterproof · cited by 1
Affine.Simplex.PointsWithCircumcenterIndex.ctorElimproof · cited by 0
Affine.Simplex.PointsWithCircumcenterIndex.noConfusionproof · cited by 0
Affine.Simplex.PointsWithCircumcenterIndex.noConfusionTypeproof · cited by 0
Affine.Simplex.sum_circumcenterWeightsWithCircumcenterproof · cited by 0