R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
⊢ IsOpen {x | IsUnit x}
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ IsOpen {x | IsUnit x}
nontriviality R
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
⊢ ∀ (x : R), x ∈ {x | IsUnit x} → ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ {x | IsUnit x}
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
⊢ IsOpen {x | IsUnit x}
apply Metric.isOpen_iff.mpr
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
⊢ ∃ ε, ε > 0 ∧ Metric.ball (↑x) ε ⊆ {x | IsUnit x}
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
⊢ ∀ (x : R), x ∈ {x | IsUnit x} → ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ {x | IsUnit x}
rintro _ ⟨x, rfl⟩
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
y : R
hy : y ∈ Metric.ball ↑x ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
⊢ ∃ ε, ε > 0 ∧ Metric.ball (↑x) ε ⊆ {x | IsUnit x}
refine' ⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ _⟩
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
y : R
hy : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
y : R
hy : y ∈ Metric.ball ↑x ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}
rw [mem_ball_iff_norm] at hy
no goals
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
y : R
hy : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}
exact (x.ofNearby y hy).isUnit