card_le — Mathlib

English

The cardinality of L.Term α is bounded by a max of aleph-null and the sum of encodable symbols.

Русский

Кардинал множества термов L.Term α ограничен максимумом между aleph-null и суммой кодируемых символов.

LaTeX

$$cardinal bound: #(L.Term α) ≤ max aleph0 #(α ⊕ (Σ i, L.Functions i))$$

Lean4

theorem card_le : #(L.Term α) ≤ max ℵ₀ #(α ⊕ (Σ i, L.Functions i)) :=
  lift_le.1 (_root_.trans Term.encoding.card_le_card_list (lift_le.2 (mk_list_le_max _)))

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