wbtw

Mathlib.Geometry.Euclidean.Sphere.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanGeometry.Sphere.IsDiameter.wbtw

English

If s.IsDiameter p1 p2 and radius ≠ 0, then Sbtw_R(p1, s.center, p2).

Русский

Если s — диаметр между p1 и p2 и радиус не нулевой, то 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 wbtw (h : s.IsDiameter p₁ p₂) : Wbtw ℝ p₁ s.center p₂ :=
  by
  rw [← h.midpoint_eq_center]
  exact wbtw_midpoint _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru