countable_functions — Mathlib

English

If L.Symbols is countable, then the set of all function symbols across all arities is countable.

Русский

Если множества символов функций языка являются счётными, то множество всех символов функций по всем аргументациям счётно.

LaTeX

$$$Countable\left(\sum_{l} L.Functions(l)\right)$$$

Lean4

instance countable_functions [h : Countable L.Symbols] : Countable (Σ l, L.Functions l) :=
  @Function.Injective.countable _ _ h _ Sum.inl_injective

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