cardinalMk_le_max_aleph0_of_finite

English

If each β a is finite, then #(WType β) ≤ max (#α, aleph0).

Русский

Если для каждого a β a конечно, то #(WType β) ≤ max(#α, aleph0).

LaTeX

$$$\#(WType(β)) \le \max(\#α, \aleph_0).$$$

Lean4

/-- If, for any `a : α`, `β a` is finite, then the cardinality of `WType β`
is at most the maximum of the cardinality of `α` and `ℵ₀` -/
theorem cardinalMk_le_max_aleph0_of_finite [∀ a, Finite (β a)] : #(WType β) ≤ max #α ℵ₀ :=
  cardinalMk_le_max_aleph0_of_finite'.trans_eq <| by rw [lift_id]

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