WType.cardinal_mk_le_max_aleph0_of_finite
theorem WType.cardinal_mk_le_max_aleph0_of_finite :
∀ {α : Type u} {β : α → Type u} [inst : ∀ (a : α), Finite (β a)],
Cardinal.mk (WType β) ≤ max (Cardinal.mk α) Cardinal.aleph0
The theorem `WType.cardinal_mk_le_max_aleph0_of_finite` states that for any type `α` and a function `β` that maps from `α` to another type, if for all `a` in `α`, the type `β a` is finite, then the cardinality of the W-type generated by `β` is less than or equal to the maximum of the cardinality of `α` and `ℵ₀` (the smallest infinite cardinal, the cardinality of the set of natural numbers). In other words, when we have a family of finite sets indexed by `α`, the size of the W-type constructed from this family is bounded above by the larger of the size of `α` and the size of the set of natural numbers.
More concisely: If `α` is a type and `β : α → Type` is a function such that for all `a ∈ α`, the type `β a` is finite, then the cardinality of the W-type generated by `β` is less than or equal to max(card `α`, ℵ₀).
|
WType.cardinal_mk_le_max_aleph0_of_finite'
theorem WType.cardinal_mk_le_max_aleph0_of_finite' :
∀ {α : Type u} {β : α → Type v} [inst : ∀ (a : α), Finite (β a)],
Cardinal.mk (WType β) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk α)) Cardinal.aleph0
The theorem `WType.cardinal_mk_le_max_aleph0_of_finite'` states that for any type `α` and a function `β : α → Type v`, if for every `a : α`, `β a` is finite, then the cardinality of the well-ordered type generated by `β` (denoted as `WType β`) is at most the maximum of the cardinality of `α` and the cardinal of the smallest infinite set (`ℵ₀`). In mathematical terms, if `β a` is finite for every `a` in `α`, then the cardinality of the well-ordered type is less than or equal to the maximum of `|α|` and `ℵ₀`.
More concisely: If `β : α → Type v` has finite domains for all `α`, then the cardinality of `WType β` is at most the maximum of `|α|` and `ℵ₀`.
|
WType.cardinal_mk_le_of_le
theorem WType.cardinal_mk_le_of_le :
∀ {α : Type u} {β : α → Type u} {κ : Cardinal.{u}},
(Cardinal.sum fun a => κ ^ Cardinal.mk (β a)) ≤ κ → Cardinal.mk (WType β) ≤ κ
The theorem `WType.cardinal_mk_le_of_le` states that for any type `α`, any function `β` from `α` to a type, and any cardinal number `κ`, if the cardinality of the disjoint union of `κ` to the power of the cardinality of `β a` for each `a` in `α` (represented by `Cardinal.sum fun a => κ ^ Cardinal.mk (β a)`) is less than or equal to `κ`, then the cardinality of the well-founded tree type (`WType`) constructed from `β` is also less than or equal to `κ`. This is a statement about the relationship between the cardinalities of types, the cardinalities of disjoint unions of types, and the cardinalities of well-founded tree types.
More concisely: If the sum of the powers of a cardinal number κ, raised to the cardinality of each element in a type α, is less than or equal to κ, then the cardinality of the well-founded tree type constructed from a function from α to any type is also less than or equal to κ.
|
WType.cardinal_mk_le_of_le'
theorem WType.cardinal_mk_le_of_le' :
∀ {α : Type u} {β : α → Type v} {κ : Cardinal.{max u v}},
(Cardinal.sum fun a => κ ^ Cardinal.lift.{u, v} (Cardinal.mk (β a))) ≤ κ → Cardinal.mk (WType β) ≤ κ
The theorem `WType.cardinal_mk_le_of_le'` is stating that for any type `α`, any function `β` from `α` to some type, and any cardinal `κ`, if the cardinality of the disjoint union of `κ` raised to the cardinality of `β a` (where `a` is an element of `α`) is less than or equal to `κ`, then the cardinality of the W-type determined by `β` (which intuitively represents non-well-founded trees with branching given by `β`) is also less than or equal to `κ`. This theorem essentially provides a bound on the cardinality of W-types in terms of the cardinalities of their branching types.
More concisely: For any type `α`, function `β` from `α` to some type, and cardinal `κ`, if the cardinality of the disjoint union of `κ` raised to the power of the cardinality of `β(α)` is less than or equal to `κ`, then the cardinality of the W-type determined by `β` is also less than or equal to `κ`.
|