English
For a sphere S and points p,q in P, the inclusion of the corresponding orthRadius subspaces satisfies s.orthRadius(p) ≤ s.orthRadius(q) if and only if either p = q or q = center of S.
Русский
Для сферы S и точек p, q в пространстве P выполняется: если s.orthRadius(p) ⊆ s.orthRadius(q), то либо p = q, либо q = центр S.
LaTeX
$$$ s.orthRadius(p) \\leq s.orthRadius(q) \\iff p = q \\lor q = s.center $$$
Lean4
theorem orthRadius_le_orthRadius_iff {s : Sphere P} {p q : P} :
s.orthRadius p ≤ s.orthRadius q ↔ p = q ∨ q = s.center :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· have h' := direction_le h
simp only [direction_orthRadius] at h'
have h'' := Submodule.orthogonal_le h'
simp only [Submodule.orthogonal_orthogonal, Submodule.span_singleton_le_iff_mem,
Submodule.mem_span_singleton] at h''
rcases h'' with ⟨r, hr⟩
have hp : p ∈ s.orthRadius q := h (s.self_mem_orthRadius p)
rw [mem_orthRadius_iff_inner_left, ← vsub_sub_vsub_cancel_right p q s.center, ← hr, inner_sub_left,
real_inner_smul_left, real_inner_smul_right, ← mul_assoc, ← sub_mul, mul_eq_zero] at hp
rcases hp with hp | hp
· nth_rw 1 [← one_mul r] at hp
rw [← sub_mul, mul_eq_zero] at hp
rcases hp with hp | rfl
· rw [sub_eq_zero] at hp
rw [← hp, one_smul, vsub_left_cancel_iff] at hr
exact .inl hr
· rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hr
exact .inr hr
· simp only [inner_self_eq_zero, vsub_eq_zero_iff_eq] at hp
rw [hp, vsub_self, smul_zero, eq_comm, vsub_eq_zero_iff_eq] at hr
exact .inr hr
· rcases h with rfl | rfl <;> simp
