feat(logic/relation): auxiliary forall_exists_rel relation

[vihdzp]

This can be used to golf both the pre-game API and the ZFC set API.

Co-authored-by: @negiizhao [email protected]

---

[YaelDillies]

Do you know about relator.bi_total?

Suggested change

	/--
	`forall_exists_rel r s t` says that for every `s i` there is some `t j` such that `r (s i) (t j)`,
	and for every `t j` there is some `s i` such that `r (s i) (t j)`.
	This finds use as an auxilary definition when defining relations on quotients of families `ι → α` by
	extensionality.
	-/
	def forall_exists_rel {ι₁ ι₂ α₁ α₂ : Type*} (r : α₁ → α₂ → Prop) (s : ι₁ → α₁) (t : ι₂ → α₂) :=
	(∀ i, ∃ j, r (s i) (t j)) ∧ ∀ j, ∃ i, r (s i) (t j)
	/--
	`forall_exists_rel r s t` says that for every `s i` there is some `t j` such that `r (s i) (t j)`,
	and for every `t j` there is some `s i` such that `r (s i) (t j)`.
	This finds use as an auxilary definition when defining relations on quotients of families `ι → α` by
	extensionality.
	-/
	def forall_exists_rel {ι₁ ι₂ α₁ α₂ : Type*} (r : α₁ → α₂ → Prop) (s : ι₁ → α₁) (t : ι₂ → α₂) :=
	relator.bi_total $ λ i j, r (s i) (t j)

[vihdzp]

I didn't know about it. All of these lemmas could probably be turned into simpler lemmas for bi_total. I'll try to clean up the file and add these results.

[YaelDillies]

I think you don't need to introduce a new definition.