Library Coq.Logic.Classical_Pred_Type
Classical Predicate Logic on Type
de Morgan laws for quantifiers
Lemma not_all_not_ex :
forall P:U ->
Prop, ~ (
forall n:U, ~
P n) ->
exists n :
U,
P n.
Lemma not_all_ex_not :
forall P:U ->
Prop, ~ (
forall n:U,
P n) ->
exists n :
U, ~
P n.
Lemma not_ex_all_not :
forall P:U ->
Prop, ~ (
exists n :
U,
P n) ->
forall n:U, ~
P n.
Lemma not_ex_not_all :
forall P:U ->
Prop, ~ (
exists n :
U, ~
P n) ->
forall n:U,
P n.
Lemma ex_not_not_all :
forall P:U ->
Prop, (
exists n :
U, ~
P n) -> ~ (
forall n:U,
P n).
Lemma all_not_not_ex :
forall P:U ->
Prop, (
forall n:U, ~
P n) -> ~ (
exists n :
U,
P n).
End Generic.