case intro
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖↑f x‖ ≤ C}
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
h : Nonempty α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖↑f x‖ ≤ C}
obtain ⟨a⟩ := h
case intro
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C} = sInf {C | ∀ (x : α), ‖↑f x‖ ≤ C}
case intro
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖↑f x‖ ≤ C}
rw [norm_eq]
case intro.e_a
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
⊢ {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C} = {C | ∀ (x : α), ‖↑f x‖ ≤ C}
case intro
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C} = sInf {C | ∀ (x : α), ‖↑f x‖ ≤ C}
congr
case intro.e_a.h
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
x✝ : ℝ
⊢ x✝ ∈ {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C} ↔ x✝ ∈ {C | ∀ (x : α), ‖↑f x‖ ≤ C}
case intro.e_a
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
⊢ {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C} = {C | ∀ (x : α), ‖↑f x‖ ≤ C}
ext
case intro.e_a.h
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
x✝ : ℝ
⊢ (∀ (x : α), ‖↑f x‖ ≤ x✝) → 0 ≤ x✝
case intro.e_a.h
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
x✝ : ℝ
⊢ x✝ ∈ {C | 0 ≤ C ∧ ∀ (x : α), ‖↑f x‖ ≤ C} ↔ x✝ ∈ {C | ∀ (x : α), ‖↑f x‖ ≤ C}
simp only [mem_setOf_eq, and_iff_right_iff_imp]
no goals
case intro.e_a.h
F : Type ?u.993399
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
a : α
x✝ : ℝ
⊢ (∀ (x : α), ‖↑f x‖ ≤ x✝) → 0 ≤ x✝
exact fun h' => le_trans (norm_nonneg (f a)) (h' a)