ballSubgroup — Mathlib

English

The ballSubgroup c is defined as the subgroup associated to the UpperSet Ioi c.

Русский

ballSubgroup c задаётся как подгруппа, соответствующая верхнему множеству Ioi c.

LaTeX

$$$\\text{ballSubgroup}(c) := \\text{subgroup}(\\text{UpperSet.Ioi } c)$$$

Lean4

/-- An open ball defined by `MulArchimedeanClass.subgroup` of `UpperSet.Ioi c`.
For `c = ⊤`, we assign the junk value `⊥`. -/
@[to_additive /-- An open ball defined by `ArchimedeanClass.addSubgroup` of `UpperSet.Ioi c`.
    For `c = ⊤`, we assign the junk value `⊥`. -/
    ]
noncomputable abbrev ballSubgroup (c : MulArchimedeanClass M) :=
  subgroup (UpperSet.Ioi c)

Похожие утверждения