# Cardinality of a set with a countable cover #

Assume that a set `t`

is eventually covered by a countable family of sets, all with
cardinality `≤ a`

. Then `t`

itself has cardinality at most `a`

. This is proved in
`Cardinal.mk_subtype_le_of_countable_eventually_mem`

.

Versions are also given when `t = univ`

, and with `= a`

instead of `≤ a`

.

If a set `t`

is eventually covered by a countable family of sets, all with cardinality at
most `a`

, then the cardinality of `t`

is also bounded by `a`

.
Superseded by `mk_le_of_countable_eventually_mem`

which does not assume
that the indexing set lives in the same universe.

If a set `t`

is eventually covered by a countable family of sets, all with cardinality at
most `a`

, then the cardinality of `t`

is also bounded by `a`

.

If a space is eventually covered by a countable family of sets, all with cardinality at
most `a`

, then the cardinality of the space is also bounded by `a`

.

If a space is eventually covered by a countable family of sets, all with cardinality `a`

,
then the cardinality of the space is also `a`

.