English
In a densely ordered ring, if s is strictly convex and x,y ∈ s with the open segment between x and y lying in the frontier of s, then x = y.
Русский
В плотнопорядковой кольцевой системе, если s строго выпукло и x,y ∈ s, а открытый отрезок между x и y лежит на границе s, то x = y.
LaTeX
$$$\StrictConvex 𝕜 s \rightarrow x \in s \rightarrow y \in s \rightarrow (openSegment 𝕜 x y \subset frontier s) \rightarrow x = y$$$
Lean4
theorem eq_of_openSegment_subset_frontier [IsOrderedRing 𝕜] [Nontrivial 𝕜] [DenselyOrdered 𝕜] (hs : StrictConvex 𝕜 s)
(hx : x ∈ s) (hy : y ∈ s) (h : openSegment 𝕜 x y ⊆ frontier s) : x = y :=
by
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
classical
by_contra hxy
exact
(h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, rfl⟩).2
(hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel _ _)
