encodableCountableBasis — Mathlib

English

If α is second-countable, then the countable basis is encodable (there exists a coding for its elements).

Русский

Если α второй счётности, то счётный базис кодируем; существует кодировка его элементов.

LaTeX

$$$\text{Encodable}(\text{countableBasis}(\alpha).\text{Elem})$$$

Lean4

instance encodableCountableBasis [SecondCountableTopology α] : Encodable (countableBasis α) :=
  (countable_countableBasis α).toEncodable

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