English
Let G be a topological group which is first-countable. Then there exists a sequence of neighborhoods of the identity, indexed by natural numbers, u0, u1, u2, …, such that each un is a neighborhood of 1, the sequence is antitone (u_{n+1} ⊆ u_n for all n), and for every n we have u_{n+1} · u_{n+1} ⊆ u_n.
Русский
Пусть G — топологическая группа, первая счётность существует. Тогда существует последовательность окрестностей тождества 1: u0, u1, u2, …, такая что каждое un является окрестностью 1, последовательность антитонна (u_{n+1} ⊆ u_n для всех n), и для каждого n выполняется u_{n+1} · u_{n+1} ⊆ u_n.
LaTeX
$$$\text{Let } G \text{ be a first-countable topological group. Then there exists } (u_n)_{n\in\mathbb{N}} \text{ with } \forall n, \, u_n \text{ is a neighborhood of } 1 \text{ and } u_{n+1} \cdot u_{n+1} \subseteq u_n.$$$
Lean4
/-- Any first countable topological group has an antitone neighborhood basis `u : ℕ → Set G` for
which `(u (n + 1)) ^ 2 ⊆ u n`. The existence of such a neighborhood basis is a key tool for
`QuotientGroup.completeSpace` -/
@[to_additive /-- Any first countable topological additive group has an antitone neighborhood basis
`u : ℕ → set G` for which `u (n + 1) + u (n + 1) ⊆ u n`.
The existence of such a neighborhood basis is a key tool for `QuotientAddGroup.completeSpace` -/
]
theorem exists_antitone_basis_nhds_one [FirstCountableTopology G] :
∃ u : ℕ → Set G, (𝓝 1).HasAntitoneBasis u ∧ ∀ n, u (n + 1) * u (n + 1) ⊆ u n :=
by
rcases (𝓝 (1 : G)).exists_antitone_basis with ⟨u, hu, u_anti⟩
have := ((hu.prod_nhds hu).tendsto_iff hu).mp (by simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G))
simp only [and_self_iff, mem_prod, and_imp, Prod.forall, Prod.exists, forall_true_left] at this
have event_mul : ∀ n : ℕ, ∀ᶠ m in atTop, u m * u m ⊆ u n :=
by
intro n
rcases this n with ⟨j, k, -, h⟩
refine atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => ?_⟩
rintro - ⟨a, ha, b, hb, rfl⟩
exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)
obtain ⟨φ, -, hφ, φ_anti_basis⟩ := HasAntitoneBasis.subbasis_with_rel ⟨hu, u_anti⟩ event_mul
exact ⟨u ∘ φ, φ_anti_basis, fun n => hφ n.lt_succ_self⟩
