English
The neighborhood basis at any nonzero point can be taken as singleton neighborhoods around that point.
Русский
Базис окрестностей любого не нулевого момента может состоять из одиночных окрестностей вокруг него.
LaTeX
$$$\mathcal{N}(x) \text{ has basis } \{\{x\}\}$ for $x \neq 0$$$
Lean4
/-- The topology on a linearly ordered group with zero element adjoined makes it a topological
monoid. -/
@[nolint defLemma]
scoped instance (priority := 100) : ContinuousMul Γ₀ where
continuous_mul := by
simp only [continuous_iff_continuousAt, ContinuousAt]
rintro ⟨x, y⟩
wlog hle : x ≤ y generalizing x y
· have := (this y x (le_of_not_ge hle)).comp (continuous_swap.tendsto (x, y))
simpa only [mul_comm, Function.comp_def, Prod.swap] using this
rcases eq_or_ne x 0 with (rfl | hx) <;> [rcases eq_or_ne y 0 with (rfl | hy); skip]
· rw [zero_mul]
refine
((hasBasis_nhds_zero.prod_nhds hasBasis_nhds_zero).tendsto_iff hasBasis_nhds_zero).2 fun γ hγ =>
⟨(γ, 1), ⟨hγ, one_ne_zero⟩, ?_⟩
rintro ⟨x, y⟩ ⟨hx : x < γ, hy : y < 1⟩
exact (mul_lt_mul'' hx hy zero_le' zero_le').trans_eq (mul_one γ)
· rw [zero_mul, nhds_prod_eq, nhds_of_ne_zero hy, prod_pure, tendsto_map'_iff]
refine (hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero).2 fun γ hγ => ?_
refine ⟨γ / y, div_ne_zero hγ hy, fun x hx => ?_⟩
calc
x * y < γ / y * y := mul_lt_mul_of_pos_right hx (zero_lt_iff.2 hy)
_ = γ := div_mul_cancel₀ _ hy
· have hy : y ≠ 0 := ((zero_lt_iff.mpr hx).trans_le hle).ne'
rw [nhds_prod_eq, nhds_of_ne_zero hx, nhds_of_ne_zero hy, prod_pure_pure]
exact pure_le_nhds (x * y)
