exists — Mathlib

English

In propositional logic, for any predicate f on propositions, (exists p, f(p)) is equivalent to f(True) or f(False).

Русский

В пропозициональной логике для любого предиката f на propositions, (существует p, f(p)) эквивалентно f(True) или f(False).

LaTeX

$$$ \exists p, f(p) \iff f(True) \lor f(False) $$$

Lean4

theorem «exists» {f : Prop → Prop} : (∃ p, f p) ↔ f True ∨ f False :=
  ⟨fun ⟨p, h⟩ ↦ by refine (em p).imp ?_ ?_ <;> intro H <;> convert h <;> simp [H], by rintro (h | h) <;> exact ⟨_, h⟩⟩

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