left_ne_right_iff_radius_pos — Mathlib

English

If s.IsDiameter p1 p2, then Wbtw_R(p1, s.center, p2).

Русский

Если s — диаметр между p1 и p2, то p1, центр, p2 образуют отношение Wbtw.

LaTeX

$$s.IsDiameter(p_1,p_2) \\Rightarrow Wbtw(\\mathbb{R}, p_1, s.center, p_2)$$

Lean4

theorem left_ne_right_iff_radius_pos (h : s.IsDiameter p₁ p₂) : p₁ ≠ p₂ ↔ 0 < s.radius :=
  by
  rw [h.left_ne_right_iff_radius_ne_zero, lt_iff_le_and_ne]
  simp [radius_nonneg_of_mem h.left_mem, eq_comm]

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