English
Let G be a nonarchimedean group with T2 separation. For any distinct a,b ∈ G, there exists an open subgroup V of G such that the left cosets aV and bV are disjoint.
Русский
Пусть G — неархимедова группа с эффектом простого разделения T2. Для любых различных a,b ∈ G существует открытая подгруппа V в G такая, что левые косеты aV и bV непересекаются.
LaTeX
$$$\forall a,b \in G, a \neq b \Rightarrow \exists V \in \mathrm{OpenSubgroup}(G): (a \cdot V) \cap (b \cdot V) = \emptyset$$$
Lean4
@[to_additive]
theorem exists_openSubgroup_separating {a b : G} (h : a ≠ b) :
∃ V : OpenSubgroup G, Disjoint (a • (V : Set G)) (b • V) :=
by
obtain ⟨u, v, _, open_v, mem_u, mem_v, dis⟩ := t2_separation (h ∘ inv_mul_eq_one.mp)
obtain ⟨V, hV⟩ := is_nonarchimedean v (open_v.mem_nhds mem_v)
use V
simp only [Disjoint, Set.le_eq_subset, Set.bot_eq_empty, Set.subset_empty_iff]
intro x mem_aV mem_bV
by_contra! con
obtain ⟨s, hs⟩ := con
have hsa : s ∈ a • (V : Set G) := mem_aV hs
have hsb : s ∈ b • (V : Set G) := mem_bV hs
rw [mem_leftCoset_iff] at hsa hsb
refine dis.subset_compl_right mem_u (hV ?_)
simpa [mul_assoc] using mul_mem hsa (inv_mem hsb)
