forall_or_exists_not — Mathlib

English

For any predicate P on α, either P holds for all elements, or there exists an element where P fails.

Русский

Для любого предиката P на α либо P выполняется для всех элементов, либо существует элемент, для которого P ложно.

LaTeX

$$$$\\left(\\forall a, P(a)\\right) \\lor \\exists a, \\neg P(a).$$$$

Lean4

theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬P a := by rw [← not_forall]; exact em _

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