univ

Mathlib.GroupTheory.GroupAction.Blocks

URI: https://scilib.ai/kg/mathlib#MulAction.IsBlock.univ

← MathLib Explorer

English

The full set is a block: IsBlock G (univ : Set X).

Русский

Полное множество является блоком: IsBlock G (univ : Set X).

LaTeX

$$$ \\text{IsBlock } G (\\mathrm{univ} : \\mathrm{Set} \\; X). $$$

Lean4

/-- The full set is a block. -/
@[to_additive (attr := simp) /-- The full set is a block. -/
    ]
theorem univ : IsBlock G (univ : Set X) :=
  IsFixedBlock.univ.isBlock

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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