exists_of_not_forall_not

Stream: general

[Kevin Buzzard]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Chris Hughes]

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]

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