English
For any c, n, x, the value approx n c x lies between the right and left approximations: c.right.approx n x ≤ approx n c x ≤ c.left.approx n x.
Русский
Для любых c, n, x значение approx n c x лежит между правой и левой аппроксимацией: c.right.approx n x ≤ approx n c x ≤ c.left.approx n x.
LaTeX
$$$approx(n,c,x) \\in [c.right.approx n x,\\; c.left.approx n x]$$$
Lean4
theorem approx_mem_Icc_right_left (c : CU P) (n : ℕ) (x : X) :
c.approx n x ∈ Icc (c.right.approx n x) (c.left.approx n x) := by
induction n generalizing c with
| zero =>
exact ⟨le_rfl, indicator_le_indicator_of_subset (compl_subset_compl.2 c.left_U_subset) (fun _ => zero_le_one) _⟩
| succ n ihn =>
simp only [approx, mem_Icc]
refine ⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩ <;> apply approx_le_approx_of_U_sub_C
exacts [subset_closure, subset_closure]
