Ceva's theorem.

This file proves various versions of Ceva's theorem in a NormedAddTorsor.

References

• https://en.wikipedia.org/wiki/Ceva%27s_theorem

theorem Affine.Triangle.prod_dist_eq_prod_dist_of_mem_line_of_mem_line {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [NormedField 𝕜] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {t : Triangle 𝕜 P} {p : Fin 3 → P} {p' : P} (hp : ∀ (i : Fin 3), p i ∈ affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (hp' : ∀ (i : Fin 3), p' ∈ affineSpan 𝕜 {t.points i, p i}) : ∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i) = ∏ i : Fin 3, dist (p i) (t.points (i + 2))

Ceva's theorem for a triangle, expressed in terms of multiplying distances.

theorem Affine.Triangle.prod_dist_div_dist_eq_one_of_mem_line_of_mem_line {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [NormedField 𝕜] [NormedSpace 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] {t : Triangle 𝕜 P} {p : Fin 3 → P} {p' : P} (hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)) (hp : ∀ (i : Fin 3), p i ∈ affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (hp' : ∀ (i : Fin 3), p' ∈ affineSpan 𝕜 {t.points i, p i}) : ∏ i : Fin (2 + 1), dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2)) = 1

Ceva's theorem for a triangle, expressed using division of distances.