Theorem Prop.exists

Modification history

2026-09-17 12:30

Mathlib/Basic/Logic/Basic.lean

chore(Basic/Logic): deduplicate `Prop.exists` and `Prop.forall` (#43381) …

Modified Prop.exists View on Github →

2022-12-15 09:57

Mathlib/Logic/Lemmas.lean

feat: `(∀ p, f p) ↔ f true ∧ f false` (#1031) …

Added Prop.exists View on Github →