Theorem: TendstoUniformlyOn.mul_of_compact (RMT4/hurwitz.lean)

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 = ∅
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

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
State after:
no goals

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 neg =>
  replace h : K.Nonempty := Set.nonempty_iff_ne_empty.2 h
  have h2 : ContinuousOn (norm ∘ f) K := continuous_norm.comp_continuousOn hf
  have h3 : ContinuousOn (norm ∘ g) K := continuous_norm.comp_continuousOn hg
  obtain ⟨xf, _, h4⟩ : ∃ x ∈ K, ∀ y ∈ K, ‖f y‖ ≤ ‖f x‖ := hK.exists_forall_ge h h2
  obtain ⟨xg, _, h5⟩ : ∃ x ∈ K, ∀ y ∈ K, ‖g y‖ ≤ ‖g x‖ := hK.exists_forall_ge h h3
  exact hF.mul_of_bound hG h4 h5
State after:
no goals

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:
simpa only [h] using tendstoUniformlyOn_empty
State after:
no goals

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:
replace h : K.Nonempty := Set.nonempty_iff_ne_empty.2 h
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
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
⊢ TendstoUniformlyOn (F * G) (f * g) p K

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 : Set.Nonempty K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
have h2 : ContinuousOn (norm ∘ f) K := continuous_norm.comp_continuousOn hf
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
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
⊢ TendstoUniformlyOn (F * G) (f * g) p K

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 : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
have h3 : ContinuousOn (norm ∘ g) K := continuous_norm.comp_continuousOn hg
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
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
⊢ TendstoUniformlyOn (F * G) (f * g) p K

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 : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
obtain ⟨xf, _, h4⟩ : ∃ x ∈ K, ∀ y ∈ K, ‖f y‖ ≤ ‖f x‖ := hK.exists_forall_ge h h2
State after:
case intro.intro
𝕜 : 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 : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
xf : α
left✝ : xf ∈ K
h4 : ∀ y ∈ K, ‖f y‖ ≤ ‖f xf‖
⊢ TendstoUniformlyOn (F * G) (f * g) p K

State before:
case intro.intro
𝕜 : 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 : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
xf : α
left✝ : xf ∈ K
h4 : ∀ y ∈ K, ‖f y‖ ≤ ‖f xf‖
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
obtain ⟨xg, _, h5⟩ : ∃ x ∈ K, ∀ y ∈ K, ‖g y‖ ≤ ‖g x‖ := hK.exists_forall_ge h h3
State after:
case intro.intro.intro.intro
𝕜 : 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 : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
xf : α
left✝¹ : xf ∈ K
h4 : ∀ y ∈ K, ‖f y‖ ≤ ‖f xf‖
xg : α
left✝ : xg ∈ K
h5 : ∀ y ∈ K, ‖g y‖ ≤ ‖g xg‖
⊢ TendstoUniformlyOn (F * G) (f * g) p K

State before:
case intro.intro.intro.intro
𝕜 : 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 : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
xf : α
left✝¹ : xf ∈ K
h4 : ∀ y ∈ K, ‖f y‖ ≤ ‖f xf‖
xg : α
left✝ : xg ∈ K
h5 : ∀ y ∈ K, ‖g y‖ ≤ ‖g xg‖
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
exact hF.mul_of_bound hG h4 h5
State after:
no goals