mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero

English

If a,b,c,d are cospherical and ∠a p b = 0, ∠c p d = 0, then dist(a,p)dist(b,p) = dist(c,p)dist(d,p).

Русский

Если a,b,c,d кососферны и углы ∠a p b = 0, ∠c p d = 0, то расстояния по хордам равны произведениям.

LaTeX

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

Lean4

/-- **Intersecting Secants Theorem**. -/
theorem mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero {a b c d p : P} (h : Cospherical ({ a, b, c, d } : Set P))
    (hab : a ≠ b) (hcd : c ≠ d) (hapb : ∠ a p b = 0) (hcpd : ∠ c p d = 0) : dist a p * dist b p = dist c p * dist d p :=
  by
  apply collinear_of_angle_eq_zero at hapb
  apply collinear_of_angle_eq_zero at hcpd
  exact
    mul_dist_eq_mul_dist_of_cospherical h (hapb.mem_affineSpan_of_mem_of_ne (by simp) (by simp) (by simp) hab)
      (hcpd.mem_affineSpan_of_mem_of_ne (by simp) (by simp) (by simp) hcd)

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