English
If a cardinal κ satisfies sum over a of κ^(β a) ≤ κ, then #(WType β) ≤ κ.
Русский
Если кардинал κ удовлетворяет сумме по a κ^(β a) ≤ κ, то #(WType β) ≤ κ.
LaTeX
$$$\big( \sum_{a:\alpha} κ^{\#(β a)} \big) \le κ \Rightarrow \#(WType(β)) \le κ.$$$
Lean4
/-- `WType` is encodable when `α` is an encodable fintype and for every `a : α`, `β a` is
encodable. -/
instance : Encodable (WType β) :=
by
haveI h' : ∀ n, Encodable (WType' β n) := fun n => Nat.rec encodable_zero encodable_succ n
let f : WType β → Σ n, WType' β n := fun t => ⟨t.depth, ⟨t, le_rfl⟩⟩
let finv : (Σ n, WType' β n) → WType β := fun p => p.2.1
have : ∀ t, finv (f t) = t := fun t => rfl
exact Encodable.ofLeftInverse f finv this
