exists_iff — Mathlib

English

For any predicate p : Prop → Prop, the statement ∃ h, p h is equivalent to p False ∨ p True.

Русский

Для любого p : Prop → Prop верно: существует h, p(h) эквивалентно p(False) ∨ p(True).

LaTeX

$$$(\exists h, p(h)) \iff (p(\text{False}) \lor p(\text{True}))$$$

Lean4

theorem exists_iff {p : Prop → Prop} : (∃ h, p h) ↔ p False ∨ p True :=
  ⟨fun ⟨h₁, h₂⟩ ↦
    by_cases (fun H : h₁ ↦ .inr <| by simpa only [H] using h₂) (fun H ↦ .inl <| by simpa only [H] using h₂), fun h ↦
    h.elim (.intro _) (.intro _)⟩

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