From 3b3901b824ce64f023930bd46c73ce7b2f1cd37d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 9 Jul 2024 02:31:04 +1000 Subject: [PATCH] chore: forward and backward directions of not_exists (#4688) These are added in Batteries. --- src/Init/PropLemmas.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index 8ac66a2ccc..726654ce72 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -253,6 +253,9 @@ end forall_congr @[simp] theorem not_exists : (¬∃ x, p x) ↔ ∀ x, ¬p x := exists_imp +theorem forall_not_of_not_exists (h : ¬∃ x, p x) : ∀ x, ¬p x := not_exists.mp h +theorem not_exists_of_forall_not (h : ∀ x, ¬p x) : ¬∃ x, p x := not_exists.mpr h + theorem forall_and : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := ⟨fun h => ⟨fun x => (h x).1, fun x => (h x).2⟩, fun ⟨h₁, h₂⟩ x => ⟨h₁ x, h₂ x⟩⟩