coe_compl

Mathlib.Data.Finset.BooleanAlgebra

URI: https://scilib.ai/kg/mathlib#Finset.coe_compl

English

The coercion of the complement matches the complement of the coercion as sets: ↑s^c = (↑s)^c.

Русский

Переобразование дополнения сохраняет дополнение множества: ↑s^c = (↑s)^c.

LaTeX

$$$\uparrow s^{c} = (\uparrow s)^{c}$$$

Lean4

@[simp, norm_cast]
theorem coe_compl (s : Finset α) : ↑sᶜ = (↑s : Set α)ᶜ :=
  Set.ext fun _ => mem_compl

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

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

Разделы

Аффилиация

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