Commit 2024-01-09 15:48 400ca883

View on Github →

chore(*): rename IsPwo to IsPWO (#9582) Rename Set.IsPwo → Set.IsPWO and Set.IsWf → Set.IsWF.

Estimated changes

added theorem Set.IsPWO.mul
deleted theorem Set.IsPwo.mul
added theorem Set.IsWF.min_mul
added theorem Set.IsWF.mul
deleted theorem Set.IsWf.min_mul
deleted theorem Set.IsWf.mul
added theorem Finsupp.isPWO
deleted theorem Finsupp.isPwo
added theorem Finset.isPWO_bUnion
added theorem Finset.isPWO_sup
deleted theorem Finset.isPwo_bUnion
deleted theorem Finset.isPwo_sup
added theorem Finset.isWF_bUnion
added theorem Finset.isWF_sup
deleted theorem Finset.isWf_bUnion
deleted theorem Finset.isWf_sup
added theorem Pi.isPWO
deleted theorem Pi.isPwo
added def Set.IsPWO
deleted def Set.IsPwo
added theorem Set.IsWF.le_min_iff
added theorem Set.IsWF.min_le
added theorem Set.IsWF.min_mem
added theorem Set.IsWF.min_union
added theorem Set.IsWF.mono
added def Set.IsWF
deleted theorem Set.IsWf.le_min_iff
deleted theorem Set.IsWf.min_le
deleted theorem Set.IsWf.min_mem
deleted theorem Set.IsWf.min_union
deleted theorem Set.IsWf.mono
deleted def Set.IsWf
added theorem Set.isPWO_empty
added theorem Set.isPWO_insert
added theorem Set.isPWO_of_finite
added theorem Set.isPWO_singleton
added theorem Set.isPWO_union
deleted theorem Set.isPwo_empty
deleted theorem Set.isPwo_insert
deleted theorem Set.isPwo_of_finite
deleted theorem Set.isPwo_singleton
deleted theorem Set.isPwo_union
added theorem Set.isWF_empty
added theorem Set.isWF_iff_isPWO
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
deleted theorem Set.isWf_empty
deleted theorem Set.isWf_iff_isPwo
deleted theorem Set.isWf_insert
deleted theorem Set.isWf_min_singleton
deleted theorem Set.isWf_singleton
deleted theorem Set.isWf_union
deleted theorem Set.isWf_univ_iff
added theorem WellFounded.isWF
deleted theorem WellFounded.isWf
deleted theorem HahnSeries.isPwo_support
deleted theorem HahnSeries.isWf_support