English
The map EReal → ENNReal given by toENNReal is continuous.
Русский
Отображение EReal в ENNReal через toENNReal непрерывно.
LaTeX
$$$ Continuous\ EReal\toENNReal $$$
Lean4
theorem continuous_toENNReal : Continuous EReal.toENNReal :=
by
refine continuous_iff_continuousAt.mpr fun x ↦ ?_
by_cases h_top : x = ⊤
· simp only [ContinuousAt, h_top, toENNReal_top]
refine ENNReal.tendsto_nhds_top fun n ↦ ?_
filter_upwards [eventually_gt_nhds (coe_lt_top n)] with y hy
exact toENNReal_coe (x := n) ▸ toENNReal_lt_toENNReal (coe_ennreal_nonneg _) hy
refine ContinuousOn.continuousAt ?_ (compl_singleton_mem_nhds_iff.mpr h_top)
refine (continuousOn_of_forall_continuousAt fun x hx ↦ ?_).congr (fun _ h ↦ toENNReal_of_ne_top h)
by_cases h_bot : x = ⊥
· refine tendsto_nhds_of_eventually_eq ?_
rw [h_bot, nhds_bot_basis.eventually_iff]
simpa [toReal_bot, ENNReal.ofReal_zero, ENNReal.ofReal_eq_zero, true_and] using ⟨0, fun _ hx ↦ toReal_nonpos hx.le⟩
refine
ENNReal.continuous_ofReal.continuousAt.comp' <|
continuousOn_toReal.continuousAt <| (toFinite _).isClosed.compl_mem_nhds ?_
simp_all only [mem_compl_iff, mem_singleton_iff, mem_insert_iff, or_self, not_false_eq_true]
