coe_compl — Mathlib

English

The underlying set of the complement equals the complement of the underlying set.

Русский

Основанное множество дополнения равно дополнению исходного множества.

LaTeX

$$$$ ((s^c : L.DefinableSet A α) : Set(α \\to M)) = (s : Set(α \\to M))^c. $$$$

Lean4

@[simp, norm_cast]
theorem coe_compl (s : L.DefinableSet A α) : ((sᶜ : L.DefinableSet A α) : Set (α → M)) = (s : Set (α → M))ᶜ :=
  rfl

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