compl_def

Mathlib.GroupTheory.GroupAction.SubMulAction

URI: https://scilib.ai/kg/mathlib#SubMulAction.compl_def

English

The carrier of the complement of p equals the complement of its carrier in M.

Русский

Носитель дополнения p равен дополнению его носителя в M.

LaTeX

$$$ \\operatorname{carrier}(s^c) = (s : \\mathrm{Set} M)^c $$$

Lean4

@[to_additive]
theorem compl_def (s : SubMulAction R M) : sᶜ.carrier = (s : Set M)ᶜ :=
  rfl

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

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

Разделы

Аффилиация

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