Cardinal.mk_subtype_le_of_countable_eventually_mem
theorem Cardinal.mk_subtype_le_of_countable_eventually_mem :
∀ {α : Type u} {ι : Type v} {a : Cardinal.{u}} [inst : Countable ι] {f : ι → Set α} {l : Filter ι} [inst : l.NeBot]
{t : Set α}, (∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) ≤ a) → Cardinal.mk ↑t ≤ a
This theorem states that for any type `α` and any index type `ι`, if a set `t` of type `α` is eventually covered by a countable family of sets, each indexed by `ι` and with cardinality at most `a`, then the cardinality of the set `t` is also bounded by `a`. The coverage of the set `t` by the family of sets is understood in the sense of a filter `l` on `ι`: for each element `x` in `t`, there is an index `i` in the filter `l` such that `x` belongs to the set indexed by `i`. The assumption that `l` is not the bottom filter ensures that this covering condition is nontrivial.
More concisely: If a set `t` of type `α` is eventually covered by a countable family of sets indexed by `ι`, each of cardinality at most `a`, and the covering is through a non-bottom filter on `ι`, then the cardinality of `t` is bounded by `a`.
|
Cardinal.mk_le_of_countable_eventually_mem
theorem Cardinal.mk_le_of_countable_eventually_mem :
∀ {α : Type u} {ι : Type v} {a : Cardinal.{u}} [inst : Countable ι] {f : ι → Set α} {l : Filter ι} [inst : l.NeBot],
(∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) ≤ a) → Cardinal.mk α ≤ a
The theorem `Cardinal.mk_le_of_countable_eventually_mem` states that, for any type `α`, any type `ι`, and any cardinal number `a` where `ι` is countable; given a function `f` from `ι` to the set of `α` and a filter `l` on `ι` that is not bottom, if every element `x` of type `α` is eventually in `f i` for some `i` in `l`, and if the cardinality of every set `f i` is less than or equal to `a`, then the cardinality of `α` is also less than or equal to `a`. In simple terms, if a space can eventually be covered by a countable collection of sets, each with cardinality at most `a`, then the cardinality of the entire space is also at most `a`.
More concisely: If a countable filter covers a set with each element eventually belonging to a subset of cardinality at most `a`, then the cardinality of the set is less than or equal to `a`.
|
Cardinal.mk_subtype_le_of_countable_eventually_mem_aux
theorem Cardinal.mk_subtype_le_of_countable_eventually_mem_aux :
∀ {α ι : Type u} {a : Cardinal.{u}} [inst : Countable ι] {f : ι → Set α} {l : Filter ι} [inst : l.NeBot]
{t : Set α}, (∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) ≤ a) → Cardinal.mk ↑t ≤ a
This theorem states that if there is a set `t` of some type `α`, which is eventually contained within a countable family of sets `f` indexed by `ι`, with each of these sets having a cardinality at most `a`, then the cardinality of `t` itself is also bounded by `a`. Here, "eventually" is defined with respect to a filter `l` on the indexing set `ι`. This theorem has been superseded by `mk_le_of_countable_eventually_mem`, which removes the requirement for the indexing set `ι` to be in the same universe.
More concisely: If a set `t` of type `α` is eventually contained in a countable family `{f(i)}` indexed by `ι` such that the cardinality of each `f(i)` is at most `a`, then the cardinality of `t` is also bounded by `a`.
|
Cardinal.mk_of_countable_eventually_mem
theorem Cardinal.mk_of_countable_eventually_mem :
∀ {α : Type u} {ι : Type v} {a : Cardinal.{u}} [inst : Countable ι] {f : ι → Set α} {l : Filter ι} [inst : l.NeBot],
(∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) = a) → Cardinal.mk α = a
This theorem states that if we have a space of type `α` which is eventually covered by a countable family of sets indexed by `ι`, where each of these sets has cardinality `a`, then the cardinality of the space is also `a`. The family of sets is represented by the function `f : ι → Set α`. The notion of "eventually" is captured by the filter `l : Filter ι`, which is non-bottom (`l.NeBot`). The condition that every point `x` in the space `α` is eventually in the set `f i` is expressed by `∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i`, and the condition that each set `f i` has cardinality `a` is expressed by `∀ (i : ι), Cardinal.mk ↑(f i) = a`.
More concisely: If `α` is a set, `ι` is a countable index set, `l` is a non-empty filter on `ι`, `f : ι → Set α` is a function, and for all `x : α` there exists an `i` in `l` such that `x` is in `f i`, and for all `i` in `í`, `Card(f i) = a`, then `Cardinal.mk ↑α = a`.
|