X : Type u_1
M : Type ?u.349183
R : Type u_2
𝕜 : Type ?u.349189
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
⊢ ContinuousAt (fun x => ↑((fun x => IsUnit.unit (_ : IsUnit (↑f x))) x)⁻¹) x
X : Type u_1
M : Type ?u.349183
R : Type u_2
𝕜 : Type ?u.349189
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
⊢ Continuous fun x => IsUnit.unit (_ : IsUnit (↑f x))
refine'
  continuous_induced_rng.2
    (Continuous.prod_mk f.continuous
      (MulOpposite.continuous_op.comp (continuous_iff_continuousAt.mpr fun x => _)))
X : Type u_1
M : Type ?u.349183
R : Type u_2
𝕜 : Type ?u.349189
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse ↑(IsUnit.unit (_ : IsUnit (↑f x)))
⊢ ContinuousAt (fun x => ↑((fun x => IsUnit.unit (_ : IsUnit (↑f x))) x)⁻¹) x
X : Type u_1
M : Type ?u.349183
R : Type u_2
𝕜 : Type ?u.349189
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
⊢ ContinuousAt (fun x => ↑((fun x => IsUnit.unit (_ : IsUnit (↑f x))) x)⁻¹) x
have := NormedRing.inverse_continuousAt (h x).unit
X : Type u_1
M : Type ?u.349183
R : Type u_2
𝕜 : Type ?u.349189
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse ↑(IsUnit.unit (_ : IsUnit (↑f x)))
⊢ ContinuousAt (fun x => ↑(IsUnit.unit (_ : IsUnit (↑f x)))⁻¹) x
X : Type u_1
M : Type ?u.349183
R : Type u_2
𝕜 : Type ?u.349189
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse ↑(IsUnit.unit (_ : IsUnit (↑f x)))
⊢ ContinuousAt (fun x => ↑((fun x => IsUnit.unit (_ : IsUnit (↑f x))) x)⁻¹) x
simp only
X : Type u_1
M : Type ?u.349183
R : Type u_2
𝕜 : Type ?u.349189
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse (↑f x)
⊢ ContinuousAt (fun x => Ring.inverse (↑f x)) x
X : Type u_1
M : Type ?u.349183
R : Type u_2
𝕜 : Type ?u.349189
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse ↑(IsUnit.unit (_ : IsUnit (↑f x)))
⊢ ContinuousAt (fun x => ↑(IsUnit.unit (_ : IsUnit (↑f x)))⁻¹) x
simp only [← Ring.inverse_unit, IsUnit.unit_spec] at this ⊢
no goals
X : Type u_1
M : Type ?u.349183
R : Type u_2
𝕜 : Type ?u.349189
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse (↑f x)
⊢ ContinuousAt (fun x => Ring.inverse (↑f x)) x
exact this.comp (f.continuousAt x)