instCountableQuotient — Mathlib

English

If α is countable, then the quotient by any relation r on α is countable.

Русский

Если α счётно, то фактор-множество α/ r счётно для любой отношения r.

LaTeX

$$$\forall \alpha\, [\operatorname{Countable}(\alpha)]\forall r:\alpha\to\alpha\to\operatorname{Prop},\ \operatorname{Countable}(\mathrm{Quot}(\alpha, r))$$$

Lean4

instance (priority := 500) [Countable α] {s : Setoid α} : Countable (Quotient s) :=
  (inferInstance : Countable (@Quot α _))

Похожие утверждения