mem_Icc — Mathlib

English

A point z lies in the Icc x y if and only if there exist a,b ≥ 0 with a+b=1 such that z = a x + b y.

Русский

Точка z принадлежит Icc x y тогда и только тогда существуют a,b ≥ 0 такие, что a+b=1 и z = a x + b y.

LaTeX

$$$ z \in Icc(x,y) \iff \exists a,b, 0 \le a \land 0 \le b \land a+b=1 \land a x + b y = z $$$

Lean4

/-- A point is in an `Icc` iff it can be expressed as a convex combination of the endpoints. -/
theorem mem_Icc (h : x ≤ y) : z ∈ Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z := by
  simp only [← segment_eq_Icc h, segment, mem_setOf_eq, smul_eq_mul, exists_and_left]

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