case pos
𝓕 : Type ?u.1269284
𝕜 : Type ?u.1269287
α : Type ?u.1269290
ι : Type u_1
κ : Type ?u.1269296
E : Type ?u.1269299
F : Type ?u.1269302
G : Type ?u.1269305
π : ι → Type u_2
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedGroup (π i)
inst✝¹ : SeminormedGroup E
f x : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
hr : 0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

case neg
𝓕 : Type ?u.1269284
𝕜 : Type ?u.1269287
α : Type ?u.1269290
ι : Type u_1
κ : Type ?u.1269296
E : Type ?u.1269299
F : Type ?u.1269302
G : Type ?u.1269305
π : ι → Type u_2
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedGroup (π i)
inst✝¹ : SeminormedGroup E
f x : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
hr : ¬0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
𝓕 : Type ?u.1269284
𝕜 : Type ?u.1269287
α : Type ?u.1269290
ι : Type u_1
κ : Type ?u.1269296
E : Type ?u.1269299
F : Type ?u.1269302
G : Type ?u.1269305
π : ι → Type u_2
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedGroup (π i)
inst✝¹ : SeminormedGroup E
f x : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
by_cases hr : 0 ≤ r
no goals
case pos
𝓕 : Type ?u.1269284
𝕜 : Type ?u.1269287
α : Type ?u.1269290
ι : Type u_1
κ : Type ?u.1269296
E : Type ?u.1269299
F : Type ?u.1269302
G : Type ?u.1269305
π : ι → Type u_2
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedGroup (π i)
inst✝¹ : SeminormedGroup E
f x : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
hr : 0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
exact pi_norm_le_iff_of_nonneg' hr
no goals
case neg
𝓕 : Type ?u.1269284
𝕜 : Type ?u.1269287
α : Type ?u.1269290
ι : Type u_1
κ : Type ?u.1269296
E : Type ?u.1269299
F : Type ?u.1269302
G : Type ?u.1269305
π : ι → Type u_2
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedGroup (π i)
inst✝¹ : SeminormedGroup E
f x : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
hr : ¬0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
exact
  iff_of_false (fun h => hr <| (norm_nonneg' _).trans h) fun h =>
    hr <| (norm_nonneg' _).trans <| h <| Classical.arbitrary _