case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ≤ approx (Nat.zero + 1) c x

case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ approx (n + 1) c x
c : CU X
⊢ approx (Nat.succ n) c x ≤ approx (Nat.succ n + 1) c x
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ approx n c x ≤ approx (n + 1) c x
induction' n with n ihn generalizing c
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ indicator (c.Uᶜ) 1 x ≤ indicator ((left c).Uᶜ) 1 x
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ≤ approx (Nat.zero + 1) c x
simp only [approx, right_U, right_le_midpoint]
no goals
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ indicator (c.Uᶜ) 1 x ≤ indicator ((left c).Uᶜ) 1 x
exact (approx_mem_Icc_right_left c 0 x).2
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ approx (n + 1) c x
c : CU X
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) ≤
    midpoint ℝ (approx (n + 1) (left c) x) (approx (n + 1) (right c) x)
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ approx (n + 1) c x
c : CU X
⊢ approx (Nat.succ n) c x ≤ approx (Nat.succ n + 1) c x
rw [approx, approx]
no goals
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ approx (n + 1) c x
c : CU X
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) ≤
    midpoint ℝ (approx (n + 1) (left c) x) (approx (n + 1) (right c) x)
exact midpoint_le_midpoint (ihn _) (ihn _)