no goals
α : Type u_1
β : Type ?u.297892
E : Type u_3
F : Type u_2
G : Type ?u.297901
E' : Type ?u.297904
F' : Type ?u.297907
G' : Type ?u.297910
E'' : Type ?u.297913
F'' : Type ?u.297916
G'' : Type ?u.297919
R : Type ?u.297922
R' : Type ?u.297925
𝕜 : Type ?u.297928
𝕜' : Type ?u.297931
inst✝¹⁴ : Norm E
inst✝¹³ : Norm F
inst✝¹² : Norm G
inst✝¹¹ : SeminormedAddCommGroup E'
inst✝¹⁰ : SeminormedAddCommGroup F'
inst✝⁹ : SeminormedAddCommGroup G'
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedAddCommGroup F''
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : SeminormedRing R
inst✝⁴ : SeminormedRing R'
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
_x : α
⊢ 0 ≤ ‖1‖
simp only [norm_one, zero_le_one]
no goals
α : Type u_1
β : Type ?u.297892
E : Type u_3
F : Type u_2
G : Type ?u.297901
E' : Type ?u.297904
F' : Type ?u.297907
G' : Type ?u.297910
E'' : Type ?u.297913
F'' : Type ?u.297916
G'' : Type ?u.297919
R : Type ?u.297922
R' : Type ?u.297925
𝕜 : Type ?u.297928
𝕜' : Type ?u.297931
inst✝¹⁴ : Norm E
inst✝¹³ : Norm F
inst✝¹² : Norm G
inst✝¹¹ : SeminormedAddCommGroup E'
inst✝¹⁰ : SeminormedAddCommGroup F'
inst✝⁹ : SeminormedAddCommGroup G'
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedAddCommGroup F''
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : SeminormedRing R
inst✝⁴ : SeminormedRing R'
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖1‖ ≤ ‖f x‖) ↔ ∀ (n : ℕ), True → ∀ᶠ (x : α) in l, ‖f x‖ ∈ Ici ↑n
simp only [norm_one, mul_one, true_imp_iff, mem_Ici]