add_half_inf_sub_mem_Ioo — Mathlib

English

If v is in the open interval (l,u), then v + (v−l ∧ u−v)/2 remains in (l,u).

Русский

Если v лежит в открытом интервале (l,u), то v + (v−l ∧ u−v)/2 лежит в том же интервале.

LaTeX

$$$\text{If } v \in (l,u) \text{ then } v + \frac{(v-l) \land (u-v)}{2} \in (l,u).$$$

Lean4

theorem add_half_inf_sub_mem_Ioo {l u v : ℝ} (hv : v ∈ Set.Ioo l u) : v + ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u :=
  by
  have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hv.1, hv.2]
  constructor
  ·
    calc
      l < v := hv.1
      _ ≤ v + ((v - l) ⊓ (u - v)) / 2 := le_add_of_nonneg_right (by positivity)
  ·
    calc
      v + ((v - l) ⊓ (u - v)) / 2
      _ < v + ((v - l) ⊓ (u - v)) := by gcongr; exact half_lt_self (by positivity)
      _ ≤ v + (u - v) := by gcongr; exact inf_le_right
      _ = u := by abel

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