sbtw — Mathlib

English

If s.IsDiameter p1 p2 and radius ≠ 0, then sbtw holds.

Русский

Если диаметр непуст, то выполняется sbtw.

LaTeX

$$s.IsDiameter(p_1,p_2) \Rightarrow s.radius \neq 0 \Rightarrow Sbtw(\\mathbb{R}, p_1, s.center, p_2)$$

Lean4

protected theorem sbtw (h : s.IsDiameter p₁ p₂) (hr : s.radius ≠ 0) : Sbtw ℝ p₁ s.center p₂ :=
  by
  rw [← h.midpoint_eq_center]
  exact sbtw_midpoint_of_ne _ (h.left_ne_right_iff_radius_ne_zero.2 hr)

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