F : Type ?u.1008073
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ dist f 0 < M ↔ ∀ (x : α), dist (↑f x) 0 < M
F : Type ?u.1008073
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖↑f x‖ < M
simp_rw [norm_def, ← dist_zero_right]
no goals
F : Type ?u.1008073
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ dist f 0 < M ↔ ∀ (x : α), dist (↑f x) 0 < M
exact dist_lt_iff_of_compact M0