compl_inv

Mathlib.Algebra.Group.Pointwise.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.compl_inv

English

Inverse commutes with set-theoretic complement: (s^c)^{-1} = (s^{-1})^c.

Русский

Обратное commute с дополнением множества: (s^c)^{-1} = (s^{-1})^c.

LaTeX

$$$ (s^{c})^{-1} = (s^{-1})^{c} $$$

Lean4

@[to_additive (attr := simp)]
theorem compl_inv : sᶜ⁻¹ = s⁻¹ᶜ :=
  preimage_compl

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

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

Разделы

Аффилиация

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