Set that descends to a quotient

Stream: Is there code for X?

[Brendan Seamas Murphy]

Say we have α : Sort*, r : α → α → Prop (known to be an equivalence relation), and S : Set α. What's the mathlib-idomatic way to say that S is a union of equivalence classes of r, i.e. that S is the preimage of some Set (Quot r)? I'm also happy to assume α, r are given as a setoid instead separately

[Brendan Seamas Murphy]

One way we could write it is as (r ⇒ Iff) (. ∈ S) (. ∈ S) or (r ⇒ (. → .)) (. ∈ S) (. ∈ S), but I've never used ⇒ or any of the Relator stuff and it's a bit of a mystery to me

[Adam Topaz]

Those spellings all look hard to understand or even parse. Can you just say that the set is the premiage of its image?

[Brendan Seamas Murphy]

That works, but it would be nice to get a definitional equality with ∀ x y, r x y → (x ∈ S ↔ y ∈ S) or ∀ x y, r x y → x ∈ S → y ∈ S since this type is directly "about" α and can applied to terms of type α to get something useful

(I agree re: the ⇒ things)

[Brendan Seamas Murphy]

Also, I think the word I was looking for to desrcibe these sets is "saturated". At least this is what was used for describing the quotient topology when I first learned topology

[Adam Topaz]

I would just use those. “For all x,y, r x y implies x in S implies y in S” sounds reasonable.

[Terence Tao]

If you are willing to use Setoids, ⟨r, h⟩ ≤ Setoid.ker S works (where h is a proof of Equivalence r).

[Brendan Seamas Murphy]

I think that would give = instead of iff

[Junyan Xu]

(r ⇒ (. ∈ S → . ∈ S)) should also work right?

"saturated" is too ambiguous IMO, see here for two different meanings in the context of monoids.