∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (x : Urysohns.CU P) (x_1 : X) (n : ℕ),
  Urysohns.CU.approx n.succ x x_1 = midpoint ℝ (Urysohns.CU.approx n x.left x_1) (Urysohns.CU.approx n x.right x_1)