Commit 2023-02-01 04:09 4ca8a4f8

View on Github →

feat: port Order.WellFoundedSet (#1975)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/WellFoundedSet.lean

added theorem Finset.isPwo_bUnion

added theorem Finset.isPwo_sup

added theorem Finset.isWf_bUnion

added theorem Finset.isWf_sup

added theorem Finset.partiallyWellOrderedOn_bUnion

added theorem Finset.partiallyWellOrderedOn_sup

added theorem Finset.wellFoundedOn_bUnion

added theorem Finset.wellFoundedOn_sup

added theorem IsAntichain.finite_of_partiallyWellOrderedOn

added theorem IsAntichain.partiallyWellOrderedOn_iff

added theorem Pi.isPwo

added theorem Set.IsPwo.image_of_monotone

added theorem Set.IsPwo.image_of_monotoneOn

added def Set.IsPwo

added theorem Set.IsWf.insert

added theorem Set.IsWf.le_min_iff

added theorem Set.IsWf.min_le

added theorem Set.IsWf.min_le_min_of_subset

added theorem Set.IsWf.min_mem

added theorem Set.IsWf.min_union

added theorem Set.IsWf.mono

added def Set.IsWf

added def Set.PartiallyWellOrderedOn.IsBadSeq

added def Set.PartiallyWellOrderedOn.IsMinBadSeq

added theorem Set.PartiallyWellOrderedOn.exists_min_bad_of_exists_bad

added theorem Set.PartiallyWellOrderedOn.exists_monotone_subseq

added theorem Set.PartiallyWellOrderedOn.iff_forall_not_isBadSeq

added theorem Set.PartiallyWellOrderedOn.iff_not_exists_isMinBadSeq

added theorem Set.PartiallyWellOrderedOn.image_of_monotone_on

added theorem Set.PartiallyWellOrderedOn.mono

added theorem Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂

added theorem Set.PartiallyWellOrderedOn.union

added theorem Set.PartiallyWellOrderedOn.wellFoundedOn

added def Set.PartiallyWellOrderedOn

added theorem Set.Subsingleton.partiallyWellOrderedOn

added theorem Set.WellFoundedOn.acc_iff_wellFoundedOn

added theorem Set.WellFoundedOn.insert

added theorem Set.WellFoundedOn.subset

added theorem Set.WellFoundedOn.union

added def Set.WellFoundedOn

added theorem Set.isPwo_empty

added theorem Set.isPwo_iff_exists_monotone_subseq

added theorem Set.isPwo_insert

added theorem Set.isPwo_of_finite

added theorem Set.isPwo_singleton

added theorem Set.isPwo_union

added theorem Set.isWf_empty

added theorem Set.isWf_iff_isPwo

added theorem Set.isWf_iff_no_descending_seq

added theorem Set.isWf_insert

added theorem Set.isWf_min_singleton

added theorem Set.isWf_singleton

added theorem Set.isWf_union

added theorem Set.isWf_univ_iff

added theorem Set.partiallyWellOrderedOn_empty

added theorem Set.partiallyWellOrderedOn_iff_exists_monotone_subseq

added theorem Set.partiallyWellOrderedOn_iff_finite_antichains

added theorem Set.partiallyWellOrderedOn_insert

added theorem Set.partiallyWellOrderedOn_singleton

added theorem Set.partiallyWellOrderedOn_union

added theorem Set.wellFoundedOn_empty

added theorem Set.wellFoundedOn_iff

added theorem Set.wellFoundedOn_iff_no_descending_seq

added theorem Set.wellFoundedOn_insert

added theorem Set.wellFoundedOn_singleton

added theorem Set.wellFoundedOn_union

added theorem WellFounded.isWf