preimage_singleton_false

Mathlib.Data.Set.Image

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

English

For any predicate p, the preimage of {False} under p equals {a | ¬p(a)}.

Русский

Для любого предиката p, предобраз {False} равен множеству {a | ¬p(a)}.

LaTeX

$$$ p^{-1}({False}) = \\{ a \\mid \\neg p(a) \\}. $$$

Lean4

@[simp]
theorem preimage_singleton_false (p : α → Prop) : p ⁻¹' { False } = {a | ¬p a} := by ext; simp

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

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

Разделы

Аффилиация

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