toFinset_compl

Mathlib.Data.Fintype.Sets

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

English

Complement commutes with toFinset: (sᶜ).toFinset = s.toFinsetᶜ.

Русский

Комплемент сохраняется через toFinset.

LaTeX

$$$(s^{c}).toFinset = (s.toFinset)^{c}$$$

Lean4

@[simp]
theorem toFinset_compl [Fintype α] [Fintype (sᶜ : Set _)] : sᶜ.toFinset = s.toFinsetᶜ :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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