feat(SetTheory/Cardinal): Δ-system lemma

[staroperator]

We prove the Δ-system lemma, which says for any regular cardinal θ and infinite cardinal κ < θ, if ∀ c < θ, c ^< κ < θ, any θ-sized family of sets whose cardinalities are less than κ must contain a θ-sized Δ-system (this condition is called Δ-system property for θ and κ, noted as Δ(θ, k)). As a special case, Δ(ℵ₁, ℵ₀) ensures any uncountable family of finite sets must contain an uncountable Δ-system.

---

• depends on: feat: Fodor's lemma #37685
• depends on: feat(Order/CompleteLatticeIntervals): ConditionallyCompleteLinearOrderBot for Set.Iio #38266

[github-actions]

PR summary c3e588b468

Import changes exceeding 2%

%	File
+8.15%	Mathlib.Order.IsNormal

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.IsNormal	405	438	+33 (+8.15%)

Import changes for all files

Files	Import difference
Mathlib.Order.DirSupClosed	1
Mathlib.Topology.Order.IsNormal	3
Mathlib.Order.IsNormal	33
Mathlib.Order.Club (new file)	745
Mathlib.SetTheory.Cardinal.DeltaSystem (new file)	746

---

Declarations diff

+ Cardinal.IsRegular.card_eq_of_isStationary
+ Cardinal.IsRegular.isStationary_setOf_cof_eq
+ DeltaSystemProperty
+ DeltaSystemProperty.exists_pairwise_eq
+ DeltaSystemProperty.mono
+ DirSupClosed.mem_iff_of_antisymmRel
+ DirSupClosed.mem_imp_of_antisymmRel
+ DirSupClosed.of_isEmpty
+ DirSupClosedOn.of_isEmpty
+ DirSupInacc.mem_iff_of_antisymmRel
+ DirSupInacc.of_isEmpty
+ DirSupInaccOn.of_isEmpty
+ IsClub
+ IsClub.biInter
+ IsClub.ciSup_mem
+ IsClub.csSup_mem
+ IsClub.diag
+ IsClub.iInter
+ IsClub.inter
+ IsClub.isLUB_mem
+ IsClub.nonempty
+ IsClub.of_isEmpty
+ IsClub.sInter
+ IsClub.univ
+ IsLowerSet.dirSupInaccOn
+ IsStationary
+ IsStationary.inter_isClub
+ IsStationary.mono
+ IsStationary.nonempty
+ IsStationary.not_bddAbove
+ IsStationary.of_not_isCofinal_compl
+ IsStationary.univ
+ IsUpperSet.dirSupClosedOn
+ Order.IsNormal.isClub_fixedPoints
+ Set.Iio.coe_iInf
+ Set.Iio.coe_iSup
+ Set.Iio.coe_sInf
+ Set.Iio.coe_sSup
+ Set.Iio.conditionallyCompleteLinearOrderBot
+ Uncountable.exists_pairwise_inter_eq_finset
+ _root_.Order.cof_cardinal
+ _root_.Order.cof_ordinal
+ bddAbove_Iio_of_lt_cof
+ bddAbove_range_Iio_of_lt_cof
+ bddAbove_range_toType_of_lt_cof
+ bddAbove_toType_of_lt_cof
+ coe_bot
+ coe_sup
+ deltaSystemProperty_aleph0
+ deltaSystemProperty_aux
+ deltaSystemProperty_of_powerlt_lt
+ dirSupClosedOn_Iic
+ dirSupClosedOn_Ioi
+ dirSupClosedOn_iff_forall_sSup
+ dirSupClosedOn_singleton
+ dirSupClosed_Ioi
+ dirSupClosed_singleton
+ dirSupInaccOn_Iic
+ dirSupInaccOn_iff_forall_sSup
+ dirSupInacc_Iic
+ exists_isStationary_preimage_singleton
+ exists_isStationary_preimage_singleton_of_cardinalMk_range_lt_cof
+ exists_pairwise_inter_eq_finset
+ iSup_iterate_mem_fixedPoints
+ infinite_pigeonhole_card_range
+ instance [Lattice α] [IsLinearOrder α (· ≤ ·)] {a : α} : Lattice (Iio a)
+ instance {o : Ordinal} : WellFoundedLT (Set.Iio o) := ToType.mk.toOrderEmbedding.wellFoundedLT
+ isClub_Ioi
+ isClub_almost_fixed_points
+ isClub_empty_iff
+ isGreatest_Ioi_top
+ isLUB_congr_of_antisymmRel
+ isStationary_univ_iff
+ lift_powerlt
+ mk_Iio_Iio_ord_eq
+ mk_Iio_Iio_ord_lt
+ mk_bounded_set_le_powerlt
+ mk_bounded_subset_le_powerlt
+ mk_range_le_powerlt
+ noMaxOrder_Iio_ord
+ orderBot
+ powerlt_eq_zero_iff
+ powerlt_le_powerlt
+ powerlt_le_powerlt_right
+ powerlt_mono_right
+ powerlt_one
+ semilatticeSup

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[vihdzp]

Can you merge master?

[vihdzp]

Ordinal.ToType has its use cases, but I don't think this is one of them. Why not just use Iio θ.ord?

[staroperator]

I change to Iio now, but the order instance and lemmas are missing. I have made #38266 for this.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: Fodor's lemma #37685
• feat(Order/CompleteLatticeIntervals): ConditionallyCompleteLinearOrderBot for Set.Iio #38266
  By Dependent Issues (🤖). Happy coding!

[staroperator]

I have reproved the Δ-system lemma via Fodor's lemma (following Kunen's 2011 edition), which is much easier to read than the previous elementary proof. (I thought this should golf a lot, but seems not.)

[vihdzp]

I'll take a closer look at this PR once all the dependents are taken care of.