English
In a linearly ordered commutative group equipped with the order topology, the group operations are continuous with respect to the given topology, so the group is a topological group.
Русский
В линейно упорядоченной коммутативной группе, оснащённой топологией по порядку, операции группы непрерывны, поэтому она является топологической группой.
LaTeX
$$$\text{If } G ext{ is a linearly ordered commutative group with an order topology, then } G \text{ is a topological group.}$$$
Lean4
@[to_additive]
instance (priority := 100) toIsTopologicalGroup : IsTopologicalGroup G
where
continuous_mul :=
by
simp only [continuous_iff_continuousAt, Prod.forall, ContinuousAt, LinearOrderedCommGroup.tendsto_nhds]
intro a b ε hε
rcases dense_or_discrete 1 ε with ⟨δ, hδ₁, hδε⟩ | ⟨-, hε_min⟩
· filter_upwards [(eventually_mabs_div_lt _ hδ₁).prod_nhds (eventually_mabs_div_lt _ (one_lt_div'.mpr hδε))]
rintro ⟨c, d⟩ ⟨hc, hd⟩
calc
|c * d / (a * b)|ₘ = |(c / a) * (d / b)|ₘ := by rw [div_mul_div_comm]
_ ≤ |c / a|ₘ * |d / b|ₘ := mabs_mul_le ..
_ < δ * (ε / δ) := (mul_lt_mul_of_lt_of_lt hc hd)
_ = ε := mul_div_cancel ..
· have (x : G) : ∀ᶠ y in 𝓝 x, y = x :=
(eventually_mabs_div_lt _ hε).mono fun y hy ↦ mabs_div_le_one.mp <| hε_min _ hy
filter_upwards [(this _).prod_nhds (this _)]
simp [hε]
continuous_inv :=
continuous_iff_continuousAt.2 fun a ↦
LinearOrderedCommGroup.tendsto_nhds.2 fun ε ε0 ↦
(eventually_mabs_div_lt a ε0).mono fun x hx ↦ by rwa [inv_div_inv, mabs_div_comm]
