English
Icc x y is contained in the segment 𝕜 x y for all x,y.
Русский
Icc x y содержится в сегменте 𝕜 x y для любых x,y.
LaTeX
$$$ \mathrm{Icc}(x,y) \subseteq \mathrm{segment}_{\mathbb{k}}(x,y) $$$
Lean4
/-- A point is in an `Ico` iff it can be expressed as a semistrict convex combination of the
endpoints. -/
theorem mem_Ico (h : x < y) : z ∈ Ico 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 (Ico_subset_Icc_self hz)
obtain rfl | ha' := ha.eq_or_lt
· rw [zero_add] at hab
rw [hab, one_mul, zero_mul, zero_add] at hz
exact (hz.2.ne rfl).elim
· exact ⟨a, b, ha', hb, hab, rfl⟩
· rintro ⟨a, b, ha, hb, hab, rfl⟩
obtain rfl | hb' := hb.eq_or_lt
· rw [add_zero] at hab
rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]
· exact Ioo_subset_Ico_self ((Convex.mem_Ioo h).2 ⟨a, b, ha, hb', hab, rfl⟩)
