forall_mem_empty

Mathlib.Data.Set.Basic

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

English

For every predicate p on α, the statement that p(x) holds for all x in the empty set is equivalent to True.

Русский

Для любого p : α → Prop высказывание ∀ x ∈ ∅, p(x) эквивалентно True.

LaTeX

$$$\bigl(\forall x \in \emptyset, p(x)\bigr) \Leftrightarrow \mathrm{True}$$$

Lean4

theorem forall_mem_empty {p : α → Prop} : (∀ x ∈ (∅ : Set α), p x) ↔ True :=
  iff_true_intro fun _ => False.elim

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

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

Разделы

Аффилиация

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