English
The nth approximation is defined by 0-th as the indicator of the complement of U, and the (n+1)-th as the midpoint of the previous approximations on the left and right pieces.
Русский
n-я аппроксимация определяется как индикатор дополнения U для n=0, далее как середина между значениями слева и справа для n+1.
LaTeX
$$$approx(0,c,x) = \\mathbf{1}_{c.U^{c}}(x),\\quad approx(n+1,c,x) = \\text{midpoint}(approx(n,c.left,x), approx(n,c.right,x)).$$$
Lean4
/-- `n`-th approximation to a continuous function `f : X → ℝ` such that `f = 0` on `c.C` and `f = 1`
outside of `c.U`. -/
noncomputable def approx : ℕ → CU P → X → ℝ
| 0, c, x => indicator c.Uᶜ 1 x
| n + 1, c, x => midpoint ℝ (approx n c.left x) (approx n c.right x)
