internlm/Lean-Github huggingface dataset:
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
⊢ ‖F i x * (g x - G i x)‖ < ε / 2
Tactic:
rw [norm_mul]
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
⊢ ‖F i x‖ * ‖g x - G i x‖ < ε / 2
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
⊢ ‖F i x‖ * ‖g x - G i x‖ < ε / 2
Tactic:
by_cases h : F i x = 0
Proof state after:
case pos
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : F i x = 0
⊢ ‖F i x‖ * ‖g x - G i x‖ < ε / 2

case neg
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : ¬F i x = 0
⊢ ‖F i x‖ * ‖g x - G i x‖ < ε / 2
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : F i x = 0
⊢ ‖F i x‖ * ‖g x - G i x‖ < ε / 2
Tactic:
case pos => simp [h, half_pos hε]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : ¬F i x = 0
⊢ ‖F i x‖ * ‖g x - G i x‖ < ε / 2
Tactic:
case neg =>
  convert mul_lt_mul' (hf x hx) (hG x hx) (norm_nonneg _) hMf using 1
  field_simp [hMf.ne.symm]; ring
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : F i x = 0
⊢ ‖F i x‖ * ‖g x - G i x‖ < ε / 2
Tactic:
simp [h, half_pos hε]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : ¬F i x = 0
⊢ ‖F i x‖ * ‖g x - G i x‖ < ε / 2
Tactic:
convert mul_lt_mul' (hf x hx) (hG x hx) (norm_nonneg _) hMf using 1
Proof state after:
case h.e'_4
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : ¬F i x = 0
⊢ ε / 2 = Mf * (ε / (2 * Mf))
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
case h.e'_4
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : ¬F i x = 0
⊢ ε / 2 = Mf * (ε / (2 * Mf))
Tactic:
field_simp [hMf.ne.symm]
Proof state after:
case h.e'_4
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : ¬F i x = 0
⊢ ε * (2 * Mf) = Mf * ε * 2
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
case h.e'_4
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h2 : ‖(f x - F i x) * g x‖ < ε / 2
h : ¬F i x = 0
⊢ ε * (2 * Mf) = Mf * ε * 2
Tactic:
ring
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
have h1 : ∀ᶠ i in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1 := by
  simp_rw [Metric.tendstoUniformlyOn_iff, dist_eq_norm] at hF
  filter_upwards [hF 1 zero_lt_one] with i hF x hx
  have : ‖F i x‖ ≤ ‖f x - F i x‖ + ‖f x‖ := by
    simpa [← norm_neg (F i x - f x)] using norm_add_le (F i x - f x) (f x)
  linarith [hF x hx, hf x hx]
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
have h2 : ∀ᶠ i in p, ∀ x ∈ s, ‖G i x‖ ≤ mg + 1 := by
  simp_rw [Metric.tendstoUniformlyOn_iff, dist_eq_norm] at hG
  filter_upwards [hG 1 zero_lt_one] with i hG x hx
  have : ‖G i x‖ ≤ ‖g x - G i x‖ + ‖g x‖ := by
    simpa [← norm_neg (G i x - g x)] using norm_add_le (G i x - g x) (g x)
  linarith [hG x hx, hg x hx]
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
h2 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg + 1
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
h2 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg + 1
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
exact hF.mul_of_le hG h1 h2
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
Tactic:
simp_rw [Metric.tendstoUniformlyOn_iff, dist_eq_norm] at hF
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
hF : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
hF : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
Tactic:
filter_upwards [hF 1 zero_lt_one] with i hF x hx
Proof state after:
case h
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
i : ι
hF : ∀ x ∈ s, ‖f x - F i x‖ < 1
x : α
hx : x ∈ s
⊢ ‖F i x‖ ≤ mf + 1
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
case h
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
i : ι
hF : ∀ x ∈ s, ‖f x - F i x‖ < 1
x : α
hx : x ∈ s
⊢ ‖F i x‖ ≤ mf + 1
Tactic:
have : ‖F i x‖ ≤ ‖f x - F i x‖ + ‖f x‖ := by
  simpa [← norm_neg (F i x - f x)] using norm_add_le (F i x - f x) (f x)
Proof state after:
case h
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
i : ι
hF : ∀ x ∈ s, ‖f x - F i x‖ < 1
x : α
hx : x ∈ s
this : ‖F i x‖ ≤ ‖f x - F i x‖ + ‖f x‖
⊢ ‖F i x‖ ≤ mf + 1
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
case h
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
i : ι
hF : ∀ x ∈ s, ‖f x - F i x‖ < 1
x : α
hx : x ∈ s
this : ‖F i x‖ ≤ ‖f x - F i x‖ + ‖f x‖
⊢ ‖F i x‖ ≤ mf + 1
Tactic:
linarith [hF x hx, hf x hx]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
i : ι
hF : ∀ x ∈ s, ‖f x - F i x‖ < 1
x : α
hx : x ∈ s
⊢ ‖F i x‖ ≤ ‖f x - F i x‖ + ‖f x‖
Tactic:
simpa [← norm_neg (F i x - f x)] using norm_add_le (F i x - f x) (f x)
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg + 1
Tactic:
simp_rw [Metric.tendstoUniformlyOn_iff, dist_eq_norm] at hG
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
hG : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg + 1
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
hG : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg + 1
Tactic:
filter_upwards [hG 1 zero_lt_one] with i hG x hx
Proof state after:
case h
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
i : ι
hG : ∀ x ∈ s, ‖g x - G i x‖ < 1
x : α
hx : x ∈ s
⊢ ‖G i x‖ ≤ mg + 1
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
case h
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
i : ι
hG : ∀ x ∈ s, ‖g x - G i x‖ < 1
x : α
hx : x ∈ s
⊢ ‖G i x‖ ≤ mg + 1
Tactic:
have : ‖G i x‖ ≤ ‖g x - G i x‖ + ‖g x‖ := by
  simpa [← norm_neg (G i x - g x)] using norm_add_le (G i x - g x) (g x)
Proof state after:
case h
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
i : ι
hG : ∀ x ∈ s, ‖g x - G i x‖ < 1
x : α
hx : x ∈ s
this : ‖G i x‖ ≤ ‖g x - G i x‖ + ‖g x‖
⊢ ‖G i x‖ ≤ mg + 1
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
case h
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
i : ι
hG : ∀ x ∈ s, ‖g x - G i x‖ < 1
x : α
hx : x ∈ s
this : ‖G i x‖ ≤ ‖g x - G i x‖ + ‖g x‖
⊢ ‖G i x‖ ≤ mg + 1
Tactic:
linarith [hG x hx, hg x hx]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_bound
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
i : ι
hG : ∀ x ∈ s, ‖g x - G i x‖ < 1
x : α
hx : x ∈ s
⊢ ‖G i x‖ ≤ ‖g x - G i x‖ + ‖g x‖
Tactic:
simpa [← norm_neg (G i x - g x)] using norm_add_le (G i x - g x) (g x)
Proof state after:
no goals
Theorem: TendstoUniformlyOn.inv_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p K
Tactic:
apply hF.inv
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ 𝓟 (f '' K) ⊓ 𝓝 0 = ⊥
Theorem: TendstoUniformlyOn.inv_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ 𝓟 (f '' K) ⊓ 𝓝 0 = ⊥
Tactic:
rw [inf_comm, inf_principal_eq_bot]
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ (f '' K)ᶜ ∈ 𝓝 0
Theorem: TendstoUniformlyOn.inv_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ (f '' K)ᶜ ∈ 𝓝 0
Tactic:
exact (hK.image_of_continuousOn hf).isClosed.compl_mem_nhds (λ ⟨z, h1, h2⟩ => hfz z h1 h2)
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
by_cases h : K = ∅
Proof state after:
case pos
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : K = ∅
⊢ TendstoUniformlyOn (F * G) (f * g) p K

case neg
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : ¬K = ∅
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : K = ∅
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
case pos => simpa only [h] using tendstoUniformlyOn_empty
Proof state after:
no goals