Countably many classes met by a set

For a setoid s on α and a set K ⊆ α, there are two ways to count the classes of s that K meets: the quotient of K by the restriction s.comap (↑), or the image of K in the quotient by s. Mathlib's Setoid.comapQuotientEquiv puts the two in bijection, so one is countable exactly when the other is.

The quotient form is the one that comparison maps between quotients produce. The image form is monotone in K and is the natural one for "K meets countably many classes".

Main results

• Setoid.countable_quotient_comap_val_iff: the restriction of s to K has countably many classes exactly when K meets countably many classes of s.

theorem Setoid.countable_quotient_comap_val_iff {α : Type u_1} {s : Setoid α} {K : Set α} : Countable (Quotient (comap Subtype.val s)) ↔ (Quotient.mk s '' K).Countable

The restriction of a setoid s to a set K has countably many classes exactly when K meets countably many classes of s.