mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi

English

If four points a,b,c,d are cospherical and the apex p lies on both AB and CD with ∠APB = ∠CPD = π, then the chord products are equal.

Русский

Если a,b,c,d кососферны и точка p лежит на AB и CD, а значения углов ∠APB и ∠CPD равны π, то произведения расстояний по хордам равны.

LaTeX

$$Cospherical({a,b,c,d}) ∧ ∠a p b = π ∧ ∠c p d = π ⇒ dist(a,p)dist(b,p) = dist(c,p)dist(d,p)$$

Lean4

/-- **Intersecting Chords Theorem**. -/
theorem mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi {a b c d p : P} (h : Cospherical ({ a, b, c, d } : Set P))
    (hapb : ∠ a p b = π) (hcpd : ∠ c p d = π) : dist a p * dist b p = dist c p * dist d p :=
  by
  rw [EuclideanGeometry.angle_eq_pi_iff_sbtw] at hapb hcpd
  exact mul_dist_eq_mul_dist_of_cospherical h hapb.wbtw.mem_affineSpan hcpd.wbtw.mem_affineSpan

Похожие утверждения