case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ 0 ≤ approx Nat.zero c x

case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ approx (Nat.succ n) c x
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ 0 ≤ approx n c x
induction' n with n ihn generalizing c
no goals
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ 0 ≤ approx Nat.zero c x
exact indicator_nonneg (fun _ _ => zero_le_one) _
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ 2⁻¹ • (approx n (left c) x + approx n (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), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ approx (Nat.succ n) c x
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv]
no goals
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ 2⁻¹ • (approx n (left c) x + approx n (right c) x)
refine' mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg _ _) <;> apply ihn