Noncomputable Set Cardinality #
We define the cardinality of set s
as a term Set.encard s : ℕ∞
and a term Set.ncard s : ℕ
.
The latter takes the junk value of zero if s
is infinite. Both functions are noncomputable, and
are defined in terms of PartENat.card
(which takes a type as its argument); this file can be seen
as an API for the same function in the special case where the type is a coercion of a Set
,
allowing for smoother interactions with the Set
API.
Set.encard
never takes junk values, so is more mathematically natural than Set.ncard
, even
though it takes values in a less convenient type. It is probably the right choice in settings where
one is concerned with the cardinalities of sets that may or may not be infinite.
Set.ncard
has a nicer codomain, but when using it, Set.Finite
hypotheses are normally needed to
make sure its values are meaningful. More generally, Set.ncard
is intended to be used over the
obvious alternative Finset.card
when finiteness is 'propositional' rather than 'structural'.
When working with sets that are finite by virtue of their definition, then Finset.card
probably
makes more sense. One setting where Set.ncard
works nicely is in a type α
with [Finite α]
,
where every set is automatically finite. In this setting, we use default arguments and a simple
tactic so that finiteness goals are discharged automatically in Set.ncard
theorems.
Main Definitions #
Set.encard s
is the cardinality of the sets
as an extended natural number, with value⊤
ifs
is infinite.Set.ncard s
is the cardinality of the sets
as a natural number, provideds
is Finite. Ifs
is Infinite, thenSet.ncard s = 0
.toFinite_tac
is a tactic that tries to synthesize aSet.Finite s
argument withSet.toFinite
. This will work fors : Set α
where there is aFinite α
instance.
Implementation Notes #
The theorems in this file are very similar to those in Data.Finset.Card
, but with Set
operations
instead of Finset
. We first prove all the theorems for Set.encard
, and then derive most of the
Set.ncard
results as a consequence. Things are done this way to avoid reliance on the Finset
API
for theorems about infinite sets, and to allow for a refactor that removes or modifies Set.ncard
in the future.
Nearly all the theorems for Set.ncard
require finiteness of one or more of their arguments. We
provide this assumption with a default argument of the form (hs : s.Finite := by toFinite_tac)
,
where toFinite_tac
will find an s.Finite
term in the cases where s
is a set in a Finite
type.
Often, where there are two set arguments s
and t
, the finiteness of one follows from the other
in the context of the theorem, in which case we only include the ones that are needed, and derive
the other inside the proof. A few of the theorems, such as ncard_union_le
do not require
finiteness arguments; they are true by coincidence due to junk values.
The cardinality of a set as a term in ℕ∞
Equations
- s.encard = PartENat.withTopEquiv (PartENat.card ↑s)
Instances For
Alias of the reverse direction of Set.encard_eq_top_iff
.
Every set is either empty, infinite, or can have its encard
reduced by a removal. Intended
for well-founded induction on the value of encard
.
A tactic (for use in default params) that applies Set.toFinite
to synthesize a Set.Finite
term.
Equations
- Set.tacticToFinite_tac = Lean.ParserDescr.node `Set.tacticToFinite_tac 1024 (Lean.ParserDescr.nonReservedSymbol "toFinite_tac" false)
Instances For
A tactic useful for transferring proofs for encard
to their corresponding card
statements
Equations
- Set.tacticTo_encard_tac = Lean.ParserDescr.node `Set.tacticTo_encard_tac 1024 (Lean.ParserDescr.nonReservedSymbol "to_encard_tac" false)
Instances For
Explicit description of a set from its cardinality #
A Set
of a subsingleton type has cardinality at most one.
Alias of Set.ncard_le_ncard
.