closedBallSubgroup_top

Mathlib.Algebra.Order.Archimedean.Class

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

English

The map a ↦ ballSubgroup a is Antitone with respect to the Archimedean-class order.

Русский

Отображение a ↦ ballSubgroup a антиодино по порядку Архимедеанских классов.

LaTeX

$$Antitone (ballSubgroup)$$

Lean4

@[to_additive (attr := simp)]
theorem closedBallSubgroup_top : closedBallSubgroup (M := M) ⊤ = ⊥ :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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