Concluding the counting argument

In this file, we finish the counting argument.

Main declarations

• ConNF.card_tSet_le: There are at most μ-many t-sets at each level.

theorem ConNF.card_codingFunction [Params] [Level] [CoherentData] (β : TypeIndex) [LeLevel β] : Cardinal.mk (CodingFunction β) < Cardinal.mk μ

theorem ConNF.card_supportOrbit [Params] [Level] [CoherentData] (β : TypeIndex) [LeLevel β] : Cardinal.mk (SupportOrbit β) < Cardinal.mk μ

theorem ConNF.card_tSet_le [Params] [Level] [CoherentData] (β : TypeIndex) [LeLevel β] : Cardinal.mk (TSet β) ≤ Cardinal.mk μ

Note that we cannot prove the reverse implication because all of our hypotheses at this stage are about permutations, not objects.

theorem ConNF.card_tangle_le [Params] [Level] [CoherentData] (β : TypeIndex) [LeLevel β] : Cardinal.mk (Tangle β) ≤ Cardinal.mk μ