sub_half_inf_sub_mem_Ioo — Mathlib

English

If v is in (l,u), then v − (v−l ∧ u−v)/2 lies in (l,u).

Русский

Если v ∈ (l,u), то v − (v−l ∧ u−v)/2 ∈ (l,u).

LaTeX

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

Lean4

theorem sub_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 - (v - l) := by abel
      _ ≤ v - ((v - l) ⊓ (u - v)) := by gcongr; exact inf_le_left
      _ < v - ((v - l) ⊓ (u - v)) / 2 := by gcongr; exact half_lt_self (by positivity)
  ·
    calc
      v - ((v - l) ⊓ (u - v)) / 2
      _ ≤ v := by
        rw [sub_le_iff_le_add]
        exact le_add_of_nonneg_right (by positivity)
      _ < u := hv.2

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