Commit 2023-10-07 16:42 fe7a9982

View on Github →

feat: lemmas about accumulate/partialSups/biUnion (#7562) From the Kolmogorov extension theorem project.

Estimated changes

Modified Mathlib/Data/Nat/Lattice.lean

added theorem Nat.iInf_le_succ'

added theorem Nat.iInf_le_succ

added theorem Nat.iSup_le_succ'

added theorem Nat.iSup_le_succ

added theorem Set.biInter_le_succ'

added theorem Set.biInter_le_succ

added theorem Set.biUnion_le_succ'

added theorem Set.biUnion_le_succ

Modified Mathlib/Data/Set/Accumulate.lean

added theorem Set.accumulate_subset_iUnion

Modified Mathlib/Order/PartialSups.lean

added theorem partialSups_apply_mono