English
Open balls around 1 of positive radius in a group with ultrametric norm are open subgroups.
Русский
Открытые окрестности вокруг 1 положительного радиуса в группе с ультраметрической нормой образуют открытые подгруппы.
LaTeX
$$$\\text{OpenSubgroup}(S) \\quad\\text{(ball around 1 of radius } r>0)$$$
Lean4
/-- In a group with an ultrametric norm, open balls around 1 of positive radius are open subgroups.
-/
@[to_additive /-- In an additive group with an ultrametric norm, open balls around 0 of
positive radius are open subgroups. -/
]
def ball_openSubgroup {r : ℝ} (hr : 0 < r) : OpenSubgroup S
where
carrier := Metric.ball (1 : S) r
mul_mem' {x} {y} hx
hy := by
simp only [Metric.mem_ball, dist_eq_norm_div, div_one] at hx hy ⊢
exact (norm_mul_le_max x y).trans_lt (max_lt hx hy)
one_mem' := Metric.mem_ball_self hr
inv_mem' := by simp only [Metric.mem_ball, dist_one_right, norm_inv', imp_self, implies_true]
isOpen' := Metric.isOpen_ball
