Stream: general

Topic: exists_of_not_forall_not

Kevin Buzzard (Mar 10 2018 at 14:49):

I am a classical guy. Is example (α : Type) (P : α → Prop) : (¬ (∀ a : α, ¬ P a)) → (∃ a : α, P a) := sorry already in Lean or mathlib?

Andrew Ashworth (Mar 10 2018 at 14:59):

some variant is in mathlib, see not_forall and the lemmas near it in logic/basic.lean

Kevin Buzzard (Mar 10 2018 at 15:52):

Thanks. My mistake was searching for exists_of rather than concentrating on not_forall...

Chris Hughes (Mar 10 2018 at 16:31):

Thanks. My mistake was searching for exists_of rather than concentrating on not_forall...

I thought the convention was that lemmas should be named after their conclusion.

Kevin Buzzard (Mar 10 2018 at 17:12):

Yes but the lemma in the library was an iff ;-)

Last updated: May 12 2021 at 23:13 UTC