Commit 2023-07-17 00:18 4a7628dc

View on Github →

feat: prod.lex is well-founded (#5943) Match https://github.com/leanprover-community/mathlib/pull/18665

Estimated changes

Modified Mathlib.lean

Created Mathlib/Init/Data/Sigma/Lex.lean

added theorem PSigma.lex_wf

Modified Mathlib/Order/WellFounded.lean

added theorem WellFounded.mono

added theorem WellFounded.onFun

Modified Mathlib/Order/WellFoundedSet.lean

added theorem Set.WellFoundedOn.mono'

added theorem Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber

added theorem Set.WellFoundedOn.sigma_lex_of_wellFoundedOn_fiber

added theorem Set.wellFoundedOn_image

added theorem Set.wellFoundedOn_range

added theorem Set.wellFoundedOn_univ

added theorem WellFounded.prod_lex_of_wellFoundedOn_fiber

added theorem WellFounded.sigma_lex_of_wellFoundedOn_fiber

added theorem WellFounded.wellFoundedOn