mem_closedBallSubgroup_iff

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#MulArchimedeanClass.mem_closedBallSubgroup_iff

English

If c ≠ top, then a ∈ closedBallSubgroup c iff c ≤ mk a.

Русский

Если c ≠ верх, то a ∈ closedBallSubgroup c тогда и только тогда, когда c ≤ mk a.

LaTeX

$$$(c \\neq \\top) \\Rightarrow (a \\in closedBallSubgroup c \\iff c \\le mk(a))$$$

Lean4

@[to_additive]
theorem mem_closedBallSubgroup_iff {a : M} {c : MulArchimedeanClass M} : a ∈ closedBallSubgroup c ↔ c ≤ mk a := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru