mem_Ioo — Mathlib

English

For h: x < y, z ∈ Ioo x y iff there exist a,b with 0 < a, 0 < b, a+b=1 and a x + b y = z.

Русский

Для h: x < y верно: z ∈ Ioo x y тогда и только тогда существуют a,b с 0<a, 0<b, a+b=1 и z = a x + b y.

LaTeX

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

Lean4

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

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