Basic set_of lemmas

Stream: Is there code for X?

[Vincent Beffara]

Do we have these?

example {α : Type*} {P : α → Prop} (h : {x : α | P x} = ∅) (x : α) : ¬ P x :=
(h.symm ▸ set.not_mem_empty x : x ∉ {x : α | P x})

example {α : Type*} {P : α → Prop} (h : {x : α | P x} = set.univ) (x : α) : P x :=
(h.symm ▸ set.mem_univ x : x ∈ {x : α | P x})

(They both should also essentially be congr_fun h.)

[Yaël Dillies]

docs#set.eq_univ_iff_forall_mem

[Vincent Beffara]

Actually, docs#set.eq_univ_iff_forall and docs#set.eq_empty_iff_forall_not_mem - thanks!