Merge remote-tracking branch 'origin/master' into test/add_remove_mer…

…ge_conflict_label_in_ci
leanprover-community · Jan 22, 2025 · b60df39 · b60df39
2 parents 96f6113 + 2cb1216
commit b60df39
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 5 deletions.
diff --git a/Mathlib/Order/WellFoundedSet.lean b/Mathlib/Order/WellFoundedSet.lean
@@ -505,9 +505,13 @@ protected theorem IsWF.isPWO (hs : s.IsWF) : s.IsPWO := by
   simp only [forall_mem_range, not_lt] at hm
   exact ⟨m, m + 1, by omega, hm _⟩
 
-/-- In a linear order, the predicates `Set.IsWF` and `Set.IsPWO` are equivalent. -/
+/-- In a linear order, the predicates `Set.IsPWO` and `Set.IsWF` are equivalent. -/
+theorem isPWO_iff_isWF : s.IsPWO ↔ s.IsWF :=
+  ⟨IsPWO.isWF, IsWF.isPWO⟩
+
+@[deprecated isPWO_iff_isWF (since := "2025-01-21")]
 theorem isWF_iff_isPWO : s.IsWF ↔ s.IsPWO :=
-  ⟨IsWF.isPWO, IsPWO.isWF⟩
+  isPWO_iff_isWF.symm
 
 /--
 If `α` is a linear order with well-founded `<`, then any set in it is a partially well-ordered set.
@@ -668,6 +672,9 @@ theorem BddBelow.wellFoundedOn_lt : BddBelow s → s.WellFoundedOn (· < ·) :=
 theorem BddAbove.wellFoundedOn_gt : BddAbove s → s.WellFoundedOn (· > ·) :=
   fun h => h.dual.wellFoundedOn_lt
 
+theorem BddBelow.isWF : BddBelow s → IsWF s :=
+  BddBelow.wellFoundedOn_lt
+
 end LocallyFiniteOrder
 
 namespace Set.PartiallyWellOrderedOn

diff --git a/Mathlib/RingTheory/HahnSeries/Basic.lean b/Mathlib/RingTheory/HahnSeries/Basic.lean
@@ -476,10 +476,9 @@ theorem BddBelow_zero [Nonempty Γ] : BddBelow (Function.support (0 : Γ → R))
 
 variable [LocallyFiniteOrder Γ]
 
-theorem suppBddBelow_supp_PWO (f : Γ → R)
-    (hf : BddBelow (Function.support f)) :
+theorem suppBddBelow_supp_PWO (f : Γ → R) (hf : BddBelow (Function.support f)) :
     (Function.support f).IsPWO :=
-  Set.isWF_iff_isPWO.mp hf.wellFoundedOn_lt
+  hf.isWF.isPWO
 
 /-- Construct a Hahn series from any function whose support is bounded below. -/
 @[simps]