internlm/Lean-Github huggingface dataset:
Theorem: Asymptotics.isLittleO_const_fst_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
ly : Filter E
⊢ (fun x => c) =o[atBot ×ˢ ly] Prod.fst
Tactic:
refine ly.eq_or_neBot.casesOn (fun h ↦ by simp [h]) (fun _ ↦ ?_)
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atBot ×ˢ ly] Prod.fst
Theorem: Asymptotics.isLittleO_const_fst_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atBot ×ˢ ly] Prod.fst
Tactic:
show ((fun _ ↦ c) ∘ Prod.fst) =o[atBot ×ˢ ly] (id ∘ Prod.fst)
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ ((fun x => c) ∘ Prod.fst) =o[atBot ×ˢ ly] (id ∘ Prod.fst)
Theorem: Asymptotics.isLittleO_const_fst_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ ((fun x => c) ∘ Prod.fst) =o[atBot ×ˢ ly] (id ∘ Prod.fst)
Tactic:
rewrite [← isLittleO_map, map_fst_prod]
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atBot] id
Theorem: Asymptotics.isLittleO_const_fst_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atBot] id
Tactic:
exact isLittleO_const_id_atBot2 c
Proof state after:
no goals
Theorem: Asymptotics.isLittleO_const_fst_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
ly : Filter E
h : ly = ⊥
⊢ (fun x => c) =o[atBot ×ˢ ly] Prod.fst
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Asymptotics.isLittleO_const_snd_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
⊢ (fun x => c) =o[lx ×ˢ atBot] Prod.snd
Tactic:
refine lx.eq_or_neBot.casesOn (fun h ↦ by simp [h]) (fun _ ↦ ?_)
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[lx ×ˢ atBot] Prod.snd
Theorem: Asymptotics.isLittleO_const_snd_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[lx ×ˢ atBot] Prod.snd
Tactic:
show ((fun _ ↦ c) ∘ Prod.snd) =o[lx ×ˢ atBot] (id ∘ Prod.snd)
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ ((fun x => c) ∘ Prod.snd) =o[lx ×ˢ atBot] (id ∘ Prod.snd)
Theorem: Asymptotics.isLittleO_const_snd_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ ((fun x => c) ∘ Prod.snd) =o[lx ×ˢ atBot] (id ∘ Prod.snd)
Tactic:
rewrite [← isLittleO_map, map_snd_prod]
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[atBot] id
Theorem: Asymptotics.isLittleO_const_snd_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[atBot] id
Tactic:
exact isLittleO_const_id_atBot2 c
Proof state after:
no goals
Theorem: Asymptotics.isLittleO_const_snd_atBot
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
h : lx = ⊥
⊢ (fun x => c) =o[lx ×ˢ atBot] Prod.snd
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Asymptotics.isLittleO_const_fst_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
⊢ (fun x => c) =o[atTop ×ˢ ly] Prod.fst
Tactic:
refine ly.eq_or_neBot.casesOn (fun h ↦ by simp [h]) (fun _ ↦ ?_)
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atTop ×ˢ ly] Prod.fst
Theorem: Asymptotics.isLittleO_const_fst_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atTop ×ˢ ly] Prod.fst
Tactic:
show ((fun _ ↦ c) ∘ Prod.fst) =o[atTop ×ˢ ly] (id ∘ Prod.fst)
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ ((fun x => c) ∘ Prod.fst) =o[atTop ×ˢ ly] (id ∘ Prod.fst)
Theorem: Asymptotics.isLittleO_const_fst_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ ((fun x => c) ∘ Prod.fst) =o[atTop ×ˢ ly] (id ∘ Prod.fst)
Tactic:
rewrite [← isLittleO_map, map_fst_prod]
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atTop] id
Theorem: Asymptotics.isLittleO_const_fst_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atTop] id
Tactic:
exact isLittleO_const_id_atTop2 c
Proof state after:
no goals
Theorem: Asymptotics.isLittleO_const_fst_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
h : ly = ⊥
⊢ (fun x => c) =o[atTop ×ˢ ly] Prod.fst
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Asymptotics.isLittleO_const_snd_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
lx : Filter E
⊢ (fun x => c) =o[lx ×ˢ atTop] Prod.snd
Tactic:
refine lx.eq_or_neBot.casesOn (fun h ↦ by simp [h]) (fun _ ↦ ?_)
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[lx ×ˢ atTop] Prod.snd
Theorem: Asymptotics.isLittleO_const_snd_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[lx ×ˢ atTop] Prod.snd
Tactic:
show ((fun _ ↦ c) ∘ Prod.snd) =o[lx ×ˢ atTop] (id ∘ Prod.snd)
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ ((fun x => c) ∘ Prod.snd) =o[lx ×ˢ atTop] (id ∘ Prod.snd)
Theorem: Asymptotics.isLittleO_const_snd_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ ((fun x => c) ∘ Prod.snd) =o[lx ×ˢ atTop] (id ∘ Prod.snd)
Tactic:
rewrite [← isLittleO_map, map_snd_prod]
Proof state after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[atTop] id
Theorem: Asymptotics.isLittleO_const_snd_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[atTop] id
Tactic:
exact isLittleO_const_id_atTop2 c
Proof state after:
no goals
Theorem: Asymptotics.isLittleO_const_snd_atTop
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
lx : Filter E
h : lx = ⊥
⊢ (fun x => c) =o[lx ×ˢ atTop] Prod.snd
Tactic:
simp [h]
Proof state after:
no goals
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
⊢ IsBigOWith (sSup (norm '' (C '' s)) / ‖c‖) (𝓟 s ×ˢ l)
    (fun x =>
      match x with
      | (i, _x) => C i)
    fun x => c
Tactic:
refine isBigOWith_iff.mpr <| eventually_of_mem ?_ (fun x hx ↦ ?_) (U := s ×ˢ Set.univ)
Proof state after:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
⊢ s ×ˢ Set.univ ∈ 𝓟 s ×ˢ l

case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s)) / ‖c‖ * ‖c‖
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact
Proof state before:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
⊢ s ×ˢ Set.univ ∈ 𝓟 s ×ˢ l
Tactic:
exact prod_mem_prod (mem_principal_self s) univ_mem
Proof state after:
no goals
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s)) / ‖c‖ * ‖c‖
Tactic:
rw [div_mul_cancel₀ _ hc]
Proof state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s))
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s))
Tactic:
replace hs := hs.image_of_continuousOn hf |>.image continuous_norm
Proof state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s))
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s))
Tactic:
have h_sSup := hs.isLUB_sSup <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x.1, hx.1⟩
Proof state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sSup : IsLUB ((fun a => ‖a‖) '' (C '' s)) (sSup ((fun a => ‖a‖) '' (C '' s)))
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s))
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sSup : IsLUB ((fun a => ‖a‖) '' (C '' s)) (sSup ((fun a => ‖a‖) '' (C '' s)))
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s))
Tactic:
exact h_sSup.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx.1
Proof state after:
no goals
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
⊢ IsBigOWith (‖c‖ / sInf (norm '' (C '' s))) (𝓟 s ×ˢ l) (fun x => c) fun x =>
    match x with
    | (i, _x) => C i
Tactic:
refine isBigOWith_iff.mpr <| eventually_of_mem ?_ (fun x hx ↦ ?_) (U := s ×ˢ Set.univ)
Proof state after:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
⊢ s ×ˢ Set.univ ∈ 𝓟 s ×ˢ l

case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖c‖ ≤
    ‖c‖ / sInf (norm '' (C '' s)) *
      ‖match x with
        | (i, _x) => C i‖
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev
Proof state before:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
⊢ s ×ˢ Set.univ ∈ 𝓟 s ×ˢ l
Tactic:
exact prod_mem_prod (mem_principal_self s) univ_mem
Proof state after:
no goals
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖c‖ ≤
    ‖c‖ / sInf (norm '' (C '' s)) *
      ‖match x with
        | (i, _x) => C i‖
Tactic:
rewrite [mul_comm_div]
Proof state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))
Tactic:
replace hs := hs.image_of_continuousOn hf |>.image continuous_norm
Proof state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))
Tactic:
have h_sInf := hs.isGLB_sInf <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x.1, hx.1⟩
Proof state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))
Tactic:
refine le_mul_of_one_le_right (norm_nonneg c) <| (one_le_div ?_).mpr <|
  h_sInf.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx.1
Proof state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
⊢ 0 < sInf (norm '' (C '' s))
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
⊢ 0 < sInf (norm '' (C '' s))
Tactic:
obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty
Proof state after:
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < sInf (norm '' (C '' s))