case intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
hg : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
⊢ Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
hg : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g)
op : E → F → G
h_op : ∃ A, ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
⊢ Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
cases' h_op with A h_op
case intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (x : ℝ) in map (norm ∘ g) l, (fun x x_1 => x ≤ x_1) x C
⊢ Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
case intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
hg : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
⊢ Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
rcases hg with ⟨C, hC⟩
case intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
⊢ Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
case intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (x : ℝ) in map (norm ∘ g) l, (fun x x_1 => x ≤ x_1) x C
⊢ Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
rw [eventually_map] at hC
case intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
case intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
⊢ Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
rw [NormedCommGroup.tendsto_nhds_one] at hf⊢
case intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
case intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
intro ε ε₀
case intro.intro.intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
case intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
rcases exists_pos_mul_lt ε₀ (A * C) with ⟨δ, δ₀, hδ⟩
case h
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
⊢ ‖op (f i) (g i)‖ < ε
case intro.intro.intro.intro
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
filter_upwards [hf δ δ₀, hC]with i hf hg
case h
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
⊢ A * ‖f i‖ * ‖g i‖ < ε
case h
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
⊢ ‖op (f i) (g i)‖ < ε
refine' (h_op _ _).trans_lt _
case h.inl
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
hA : A ≤ 0
⊢ A * ‖f i‖ * ‖g i‖ < ε

case h.inr
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * ‖f i‖ * ‖g i‖ < ε
case h
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
⊢ A * ‖f i‖ * ‖g i‖ < ε
cases' le_total A 0 with hA hA
no goals
case h.inr
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * ‖f i‖ * ‖g i‖ < ε
calc
  A * ‖f i‖ * ‖g i‖ ≤ A * δ * C := by gcongr; exact hg
  _ = A * C * δ := (mul_right_comm _ _ _)
  _ < ε := hδ
no goals
case h.inl
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
hA : A ≤ 0
⊢ A * ‖f i‖ * ‖g i‖ < ε
exact (mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg hA <| norm_nonneg' _) <|
  norm_nonneg' _).trans_lt ε₀
case h₂
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ ‖g i‖ ≤ C
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * ‖f i‖ * ‖g i‖ ≤ A * δ * C
gcongr
no goals
case h₂
𝓕 : Type ?u.465533
𝕜 : Type ?u.465536
α : Type u_1
ι : Type ?u.465542
κ : Type ?u.465545
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ ‖g i‖ ≤ C
exact hg