exists_compls_iff

Mathlib.Data.Finset.Sups

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

English

There exists a in sᶜˢ with p a iff there exists a in s with p(aᶜ).

Русский

Существует a в sᶜˢ с свойством p а ровно тогда, когда существует a в s с свойством p(aᶜ).

LaTeX

$$$ (\\exists a \\in s^{\\complement\\}\\!ˢ) p(a) \\iff (\\exists a \\in s) p(a^{\\complement}) $$$

Lean4

theorem exists_compls_iff {p : α → Prop} : (∃ a ∈ sᶜˢ, p a) ↔ ∃ a ∈ s, p aᶜ := by aesop

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

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

Разделы

Аффилиация

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