English
For all x and compact s with δ ≥ 0, closedBall x δ · s = x · cthickening δ s.
Русский
Для любого x и компактного s с δ ≥ 0 выполняется closedBall x δ · s = x · cthickening δ s.
LaTeX
$$$\operatorname{closedBall}(x, \delta) \cdot s = x \cdot \operatorname{cthickening}(\delta, s)$$$
Lean4
/-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on
`x * M`. -/
@[to_additive /-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on
`x + S`. -/
]
noncomputable def groupSeminorm : GroupSeminorm (M ⧸ S)
where
toFun x := infDist 1 {m : M | (m : M ⧸ S) = x}
map_one' := infDist_zero_of_mem (by simp)
mul_le' x
y := by
simp only [infDist_eq_iInf]
have := (norm_aux x).to_subtype
have := (norm_aux y).to_subtype
refine le_ciInf_add_ciInf ?_
rintro ⟨a, rfl⟩ ⟨b, rfl⟩
refine ciInf_le_of_le ⟨0, forall_mem_range.2 fun _ ↦ dist_nonneg⟩ ⟨a * b, rfl⟩ ?_
simpa using norm_mul_le' _ _
inv'
x :=
eq_of_forall_le_iff fun r ↦ by
simp only [le_infDist (norm_aux _)]
exact (Equiv.inv _).forall_congr (by simp [← inv_eq_iff_eq_inv])
