isEmpty_subtype

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#isEmpty_subtype

English

The subtype {x ∈ α | p x} is empty iff ∀ x, ¬p x.

Русский

Подтип {x ∈ α | p x} пуст тогда и только тогда, когда ∀ x, ¬p x.

LaTeX

$$IsEmpty(\\Subtype\\{p\\}) \\leftrightarrow \\forall x:\\alpha, \\neg p(x)$$

Lean4

theorem isEmpty_subtype (p : α → Prop) : IsEmpty (Subtype p) ↔ ∀ x, ¬p x := by
  simp only [← not_nonempty_iff, nonempty_subtype, not_exists]

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

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

Разделы

Аффилиация

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