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‖ < ε
⊢ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖(f * g) x - (F * G) n x‖ < ε
Tactic:
intro ε hε
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
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖(f * g) x - (F * G) n x‖ < ε
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
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖(f * g) x - (F * G) n x‖ < ε
Tactic:
filter_upwards [hf, hF (ε / (2 * Mg)) (by positivity), hG (ε / (2 * Mf)) (by positivity)] with i hf hF 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 : ℝ
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
⊢ ‖(f * g) x - (F * G) i x‖ < ε
Theorem: TendstoUniformlyOn.mul_of_le
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 : ℝ
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
⊢ ‖(f * g) x - (F * G) i x‖ < ε
Tactic:
have h2 : ‖(f x - F i x) * g x‖ < ε / 2 := by
  rw [norm_mul]
  by_cases h : g x = 0
  case pos => simp [h, half_pos hε]
  case neg =>
    convert mul_lt_mul (hF x hx) (h1 x hx) (norm_pos_iff.mpr h) (by positivity) using 1
    simp only [div_mul, mul_div_cancel, hMg.ne.symm, Ne.def, not_false_iff]
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 : ℝ
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 * g) x - (F * G) i x‖ < ε
Theorem: TendstoUniformlyOn.mul_of_le
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 : ℝ
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 * g) x - (F * G) i x‖ < ε
Tactic:
have h3 : ‖F i x * (g x - G i x)‖ < ε / 2 := by
  rw [norm_mul]
  by_cases h : F i x = 0
  case pos => simp [h, half_pos hε]
  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:
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 : ℝ
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
h3 : ‖F i x * (g x - G i x)‖ < ε / 2
⊢ ‖(f * g) x - (F * G) i x‖ < ε
Theorem: TendstoUniformlyOn.mul_of_le
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 : ℝ
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
h3 : ‖F i x * (g x - G i x)‖ < ε / 2
⊢ ‖(f * g) x - (F * G) i x‖ < ε
Tactic:
simp_rw [Pi.mul_apply, lxyab]
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 : ℝ
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
h3 : ‖F i x * (g x - G i x)‖ < ε / 2
⊢ ‖(f x - F i x) * g x + F i x * (g x - G i x)‖ < ε
Theorem: TendstoUniformlyOn.mul_of_le
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 : ℝ
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
h3 : ‖F i x * (g x - G i x)‖ < ε / 2
⊢ ‖(f x - F i x) * g x + F i x * (g x - G i x)‖ < ε
Tactic:
exact (norm_add_le _ _).trans_lt (add_halves' ε ▸ add_lt_add h2 h3)
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 : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
⊢ 0 < Mf
Tactic:
positivity
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 : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
⊢ 0 < Mg
Tactic:
positivity
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 : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
Tactic:
filter_upwards [hf] with i hF x hx using (hF x hx).trans ((le_abs_self mf).trans (lt_add_one _).le)
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 : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ 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
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
Tactic:
filter_upwards [hg] with i hG x hx using (hG x hx).trans ((le_abs_self mg).trans (lt_add_one _).le)
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 : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
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
⊢ ∀ x ∈ s, ‖g x‖ ≤ Mg
Tactic:
intro 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
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
x : α
hx : x ∈ s
⊢ ‖g x‖ ≤ Mg
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 : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
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
x : α
hx : x ∈ s
⊢ ‖g x‖ ≤ Mg
Tactic:
refine le_of_tendsto ((continuous_norm.tendsto (g x)).comp (hG.tendsto_at 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
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
x : α
hx : x ∈ s
⊢ ∀ᶠ (c : ι) in p, ((fun a => ‖a‖) ∘ fun n => G n x) c ≤ Mg
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 : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
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
x : α
hx : x ∈ s
⊢ ∀ᶠ (c : ι) in p, ((fun a => ‖a‖) ∘ fun n => G n x) c ≤ Mg
Tactic:
filter_upwards [hg] with i hg using hg x hx
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
⊢ ε / (2 * Mg) > 0
Tactic:
positivity
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
⊢ ε / (2 * Mf) > 0
Tactic:
positivity
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
⊢ ‖(f x - F i x) * g 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
⊢ ‖f x - F i x‖ * ‖g 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
⊢ ‖f x - F i x‖ * ‖g x‖ < ε / 2
Tactic:
by_cases h : g 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
h : g x = 0
⊢ ‖f x - F i x‖ * ‖g 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
h : ¬g x = 0
⊢ ‖f x - F i x‖ * ‖g 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
h : g x = 0
⊢ ‖f x - F i x‖ * ‖g 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
h : ¬g x = 0
⊢ ‖f x - F i x‖ * ‖g x‖ < ε / 2
Tactic:
case neg =>
  convert mul_lt_mul (hF x hx) (h1 x hx) (norm_pos_iff.mpr h) (by positivity) using 1
  simp only [div_mul, mul_div_cancel, hMg.ne.symm, Ne.def, not_false_iff]
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
h : g x = 0
⊢ ‖f x - F i x‖ * ‖g 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
h : ¬g x = 0
⊢ ‖f x - F i x‖ * ‖g x‖ < ε / 2
Tactic:
convert mul_lt_mul (hF x hx) (h1 x hx) (norm_pos_iff.mpr h) (by positivity) 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
h : ¬g x = 0
⊢ ε / 2 = ε / (2 * Mg) * Mg
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
h : ¬g x = 0
⊢ ε / 2 = ε / (2 * Mg) * Mg
Tactic:
simp only [div_mul, mul_div_cancel, hMg.ne.symm, Ne.def, not_false_iff]
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
h : ¬g x = 0
⊢ 0 ≤ ε / (2 * Mg)
Tactic:
positivity
Proof state after:
no goals