English
If x ≠ y, openSegment 𝕜 x y equals Ioo(min{x,y}, max{x,y}).
Русский
Если x ≠ y, то openSegment 𝕜 x y равно Ioo(min{x,y}, max{x,y}).
LaTeX
$$$ x \neq y \implies openSegment_{\mathbb{k}}(x,y) = Ioo(\min\{x,y\}, \max\{x,y\}) $$$
Lean4
/-- A point is in an `Ioc` iff it can be expressed as a semistrict convex combination of the
endpoints. -/
theorem mem_Ioc (h : x < y) : z ∈ Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z :=
by
refine ⟨fun hz => ?_, ?_⟩
· obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ioc_subset_Icc_self hz)
obtain rfl | hb' := hb.eq_or_lt
· rw [add_zero] at hab
rw [hab, one_mul, zero_mul, add_zero] at hz
exact (hz.1.ne rfl).elim
· exact ⟨a, b, ha, hb', hab, rfl⟩
· rintro ⟨a, b, ha, hb, hab, rfl⟩
obtain rfl | ha' := ha.eq_or_lt
· rw [zero_add] at hab
rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]
· exact Ioo_subset_Ioc_self ((Convex.mem_Ioo h).2 ⟨a, b, ha', hb, hab, rfl⟩)
