compl_mem_compls

Mathlib.Data.Finset.Sups

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

English

If a ∈ s, then aᶜ ∈ sᶜˢ.

Русский

Если a ∈ s, то aᶜ ∈ sᶜˢ.

LaTeX

$$$ a \\in s \\Rightarrow a^{\\complement} \\in s^{\\complement\\}\\!ˢ $$$

Lean4

theorem compl_mem_compls : a ∈ s → aᶜ ∈ sᶜˢ :=
  mem_map_of_mem _

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

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

Разделы

Аффилиация

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