Commit 2023-11-01 11:37 479779ea

View on Github →

feat: The lexicographic sum of two locally finite orders is locally finite (#6340) Forward-ports https://github.com/leanprover-community/mathlib/pull/11352

Estimated changes

Modified Mathlib/Data/Finset/Sum.lean

added theorem Finset.disjSum_eq_empty

Modified Mathlib/Data/Sum/Interval.lean

added theorem Finset.inl_mem_sumLexLift

added theorem Finset.inr_mem_sumLexLift

added theorem Finset.mem_sumLexLift

added def Finset.sumLexLift

added theorem Finset.sumLexLift_eq_empty

added theorem Finset.sumLexLift_inl_inl

added theorem Finset.sumLexLift_inl_inr

added theorem Finset.sumLexLift_inr_inl

added theorem Finset.sumLexLift_inr_inr

added theorem Finset.sumLexLift_mono

added theorem Finset.sumLexLift_nonempty

added theorem Sum.Lex.Icc_inl_inl

added theorem Sum.Lex.Icc_inl_inr

added theorem Sum.Lex.Icc_inr_inl

added theorem Sum.Lex.Icc_inr_inr

added theorem Sum.Lex.Ico_inl_inl

added theorem Sum.Lex.Ico_inl_inr

added theorem Sum.Lex.Ico_inr_inl

added theorem Sum.Lex.Ico_inr_inr

added theorem Sum.Lex.Ioc_inl_inl

added theorem Sum.Lex.Ioc_inl_inr

added theorem Sum.Lex.Ioc_inr_inl

added theorem Sum.Lex.Ioc_inr_inr

added theorem Sum.Lex.Ioo_inl_inl

added theorem Sum.Lex.Ioo_inl_inr

added theorem Sum.Lex.Ioo_inr_inl

added theorem Sum.Lex.Ioo_inr_inr