Theorem: duals_lim_tendsto_maxLog_norm (Ray/Hartogs/Duals.lean)

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
b : ℝ
x : E
⊢ Filter.Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) x‖)) atTop (𝓝 (maxLog b ‖x‖))
Tactic:
rw [maxLog_norm_eq_duals_iSup]
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
b : ℝ
x : E
⊢ Filter.Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) x‖)) atTop (𝓝 (⨆ n, maxLog b ‖(duals n) x‖))

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
b : ℝ
x : E
⊢ Filter.Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) x‖)) atTop (𝓝 (⨆ n, maxLog b ‖(duals n) x‖))
Tactic:
exact Csupr.has_lim _ (duals_bddAbove (monotone_maxLog _) _)
State after:
no goals