English
Closed balls around 1 of positive radius in a normed group with ultrametric norm are open subgroups.
Русский
Закрытые окрестности вокруг 1 с положительным радиусом образуют открытые подгруппы.
LaTeX
$$$\\text{OpenSubgroup}(S) \\text{ for } \\overline{B}(1,r)\\text{ with } r>0$$$
Lean4
/-- In a group with an ultrametric norm, closed balls around 1 of positive radius are open subgroups.
-/
@[to_additive /-- In an additive group with an ultrametric norm, closed balls around 0 of positive
radius are open subgroups. -/
]
def closedBall_openSubgroup {r : ℝ} (hr : 0 < r) : OpenSubgroup S
where
carrier := Metric.closedBall (1 : S) r
mul_mem' {x} {y} hx
hy := by
simp only [Metric.mem_closedBall, dist_eq_norm_div, div_one] at hx hy ⊢
exact (norm_mul_le_max x y).trans (max_le hx hy)
one_mem' := Metric.mem_closedBall_self hr.le
inv_mem' := by simp only [mem_closedBall, dist_one_right, norm_inv', imp_self, implies_true]
isOpen' := IsUltrametricDist.isOpen_closedBall _ hr.ne'
