card_le_card_list — Mathlib

English

Let e be an encoding of α with an injective encoding into lists over Γ. Then the cardinality of α is no larger than the cardinality of List(Γ).

Русский

Пусть имеется кодирование α в List(Γ) с инъективным отображением. Тогда кардинал α не превосходит кардинал List(Γ).

LaTeX

$$$\operatorname{lift}\#\alpha \le \operatorname{lift}\#(\mathrm{List}(\Gamma))$$$

Lean4

theorem card_le_card_list {α : Type u} (e : Encoding.{u, v} α) : Cardinal.lift.{v} #α ≤ Cardinal.lift.{u} #(List e.Γ) :=
  Cardinal.lift_mk_le'.2 ⟨⟨e.encode, e.encode_injective⟩⟩

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