English
Continuation of the statement that multiplication on ℕ∞ is continuous in the ENat topology.
Русский
Продолжение того, что умножение на ℕ∞ непрерывно в топологии ENat.
LaTeX
$$$$\\text{ContinuousMul}(\\mathbb{N}_{\\infty}).$$$$
Lean4
instance : ContinuousMul ℕ∞ where
continuous_mul :=
have key (a : ℕ∞) : ContinuousAt (· * ·).uncurry (a, ⊤) :=
by
rcases (zero_le a).eq_or_lt with rfl | ha
· simp [ContinuousAt, nhds_prod_eq]
· simp only [ContinuousAt, Function.uncurry, mul_top ha.ne']
refine tendsto_nhds_top_mono continuousAt_snd ?_
filter_upwards [continuousAt_fst (lt_mem_nhds ha)] with (x, y) (hx : 0 < x)
exact le_mul_of_one_le_left (zero_le y) (Order.one_le_iff_pos.2 hx)
continuous_iff_continuousAt.2 <|
Prod.forall.2 fun
| (a : ℕ∞), ⊤ => key a
| ⊤, (b : ℕ∞) =>
((key b).comp_of_eq (continuous_swap.tendsto (⊤, b)) rfl).congr <| .of_forall fun _ ↦ mul_comm ..
| (a : ℕ), (b : ℕ) => by simp [ContinuousAt, nhds_prod_eq, tendsto_pure_nhds]
