feat(topology/noetherian_space): use well_founded_(lt/gt)

src/order/compactly_generated.lean

@@ -31,7 +31,7 @@ proofs that they are indeed equivalent to well-foundedness.
 
 ## Main results
 The main result is that the following four conditions are equivalent for a complete lattice:
- * `well_founded (>)`
+ * `well_founded_gt`
  * `complete_lattice.is_sup_closed_compact`
  * `complete_lattice.is_Sup_finite_compact`
  * `∀ k, complete_lattice.is_compact_element k`
@@ -188,10 +188,10 @@ begin
   simpa only [exists_prop],
 end
 
-lemma well_founded.is_Sup_finite_compact (h : well_founded ((>) : α → α → Prop)) :
+lemma well_founded_gt.is_Sup_finite_compact [h : well_founded_gt α] :
   is_Sup_finite_compact α :=
 λ s, begin
-  obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := well_founded.well_founded_iff_has_min.mp h
+  obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := well_founded.well_founded_iff_has_min.mp h.wf
     {x | ∃ t : finset α, ↑t ⊆ s ∧ t.sup id = x} ⟨⊥, ∅, by simp⟩,
   refine ⟨t, ht₁, (Sup_le (λ y hy, _)).antisymm _⟩,
   { classical,
@@ -213,8 +213,8 @@ begin
 end
 
 lemma is_sup_closed_compact.well_founded (h : is_sup_closed_compact α) :
-  well_founded ((>) : α → α → Prop) :=
-begin
+  well_founded_gt α :=
+⟨begin
   refine rel_embedding.well_founded_iff_no_descending_seq.mpr ⟨λ a, _⟩,
   suffices : Sup (set.range a) ∈ set.range a,
   { obtain ⟨n, hn⟩ := set.mem_range.mp this,
@@ -223,7 +223,7 @@ begin
   apply h (set.range a),
   { use a 37, apply set.mem_range_self, },
   { rintros x ⟨m, hm⟩ y ⟨n, hn⟩, use m ⊔ n, rw [← hm, ← hn], apply rel_hom_class.map_sup a, },
-end
+end⟩
 
 lemma is_Sup_finite_compact_iff_all_elements_compact :
   is_Sup_finite_compact α ↔ (∀ k : α, is_compact_element k) :=
@@ -242,43 +242,43 @@ begin
 end
 
 lemma well_founded_characterisations :
-  tfae [well_founded ((>) : α → α → Prop),
+  tfae [well_founded_gt α,
         is_Sup_finite_compact α,
         is_sup_closed_compact α,
         ∀ k : α, is_compact_element k] :=
 begin
-  tfae_have : 1 → 2, by { exact well_founded.is_Sup_finite_compact α, },
+  tfae_have : 1 → 2, by { exact @well_founded_gt.is_Sup_finite_compact α _, },
   tfae_have : 2 → 3, by { exact is_Sup_finite_compact.is_sup_closed_compact α, },
   tfae_have : 3 → 1, by { exact is_sup_closed_compact.well_founded α, },
   tfae_have : 2 ↔ 4, by { exact is_Sup_finite_compact_iff_all_elements_compact α },
   tfae_finish,
 end
 
-lemma well_founded_iff_is_Sup_finite_compact :
-  well_founded ((>) : α → α → Prop) ↔ is_Sup_finite_compact α :=
+lemma well_founded_gt_iff_is_Sup_finite_compact :
+  well_founded_gt α ↔ is_Sup_finite_compact α :=
 (well_founded_characterisations α).out 0 1
 
 lemma is_Sup_finite_compact_iff_is_sup_closed_compact :
   is_Sup_finite_compact α ↔ is_sup_closed_compact α :=
 (well_founded_characterisations α).out 1 2
 
 lemma is_sup_closed_compact_iff_well_founded :
-  is_sup_closed_compact α ↔ well_founded ((>) : α → α → Prop) :=
+  is_sup_closed_compact α ↔ well_founded_gt α :=
 (well_founded_characterisations α).out 2 0
 
-alias well_founded_iff_is_Sup_finite_compact ↔ _ is_Sup_finite_compact.well_founded
+alias well_founded_gt_iff_is_Sup_finite_compact ↔ _ is_Sup_finite_compact.well_founded
 alias is_Sup_finite_compact_iff_is_sup_closed_compact ↔
       _ is_sup_closed_compact.is_Sup_finite_compact
 alias is_sup_closed_compact_iff_well_founded ↔ _ _root_.well_founded.is_sup_closed_compact
 
 variables {α}
 
-lemma well_founded.finite_of_set_independent (h : well_founded ((>) : α → α → Prop))
+lemma well_founded_gt.finite_of_set_independent [well_founded_gt α]
   {s : set α} (hs : set_independent s) : s.finite :=
 begin
   classical,
   refine set.not_infinite.mp (λ contra, _),
-  obtain ⟨t, ht₁, ht₂⟩ := well_founded.is_Sup_finite_compact α h s,
+  obtain ⟨t, ht₁, ht₂⟩ := well_founded_gt.is_Sup_finite_compact α s,
   replace contra : ∃ (x : α), x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t,
   { have : (s \ (insert ⊥ t : finset α)).infinite := contra.diff (finset.finite_to_set _),
     obtain ⟨x, hx₁, hx₂⟩ := this.nonempty,
@@ -292,10 +292,10 @@ begin
   exact le_Sup hx₀,
 end
 
-lemma well_founded.finite_of_independent (hwf : well_founded ((>) : α → α → Prop))
+lemma well_founded_gt.finite_of_independent [well_founded_gt α]
   {ι : Type*} {t : ι → α} (ht : independent t) (h_ne_bot : ∀ i, t i ≠ ⊥) : finite ι :=
 begin
-  haveI := (well_founded.finite_of_set_independent hwf ht.set_independent_range).to_subtype,
+  haveI := (well_founded_gt.finite_of_set_independent ht.set_independent_range).to_subtype,
   exact finite.of_injective_finite_range (ht.injective h_ne_bot),
 end
 
@@ -404,10 +404,11 @@ end
 
 namespace complete_lattice
 
-lemma compactly_generated_of_well_founded (h : well_founded ((>) : α → α → Prop)) :
+lemma compactly_generated_of_well_founded [well_founded_gt α] :
   is_compactly_generated α :=
 begin
-  rw [well_founded_iff_is_Sup_finite_compact, is_Sup_finite_compact_iff_all_elements_compact] at h,
+  have h := well_founded_gt.is_Sup_finite_compact α,
+  rw [is_Sup_finite_compact_iff_all_elements_compact] at h,
   -- x is the join of the set of compact elements {x}
   exact ⟨λ x, ⟨{x}, ⟨λ x _, h x, Sup_singleton⟩⟩⟩,
 end

src/order/rel_iso/basic.lean

@@ -164,6 +164,10 @@ iff.intro (begin
   iterate 2 { apply classical.some_spec hf.has_right_inverse },
 end) (rel_hom_class.well_founded (⟨f, λ _ _, o.1⟩ : r →r s))
 
+theorem surjective.is_well_founded_iff {f : α → β} (hf : surjective f)
+  (o : ∀ {a b}, r a b ↔ s (f a) (f b)) : is_well_founded α r ↔ is_well_founded β s :=
+by rw [is_well_founded_iff, is_well_founded_iff, surjective.well_founded_iff hf @o]
+
 /-- A relation embedding with respect to a given pair of relations `r` and `s`
 is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`. -/
 structure rel_embedding {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ↪ β :=

src/topology/noetherian_space.lean

@@ -13,8 +13,8 @@ import topology.sets.closeds
 > Any changes to this file require a corresponding PR to mathlib4.
 
 A Noetherian space is a topological space that satisfies any of the following equivalent conditions:
-- `well_founded ((>) : opens α → opens α → Prop)`
-- `well_founded ((<) : closeds α → closeds α → Prop)`
+- `well_founded_gt (opens α)`
+- `well_founded_lt (closeds α)`
 - `∀ s : set α, is_compact s`
 - `∀ s : opens α, is_compact s`
 
@@ -43,14 +43,12 @@ variables (α β : Type*) [topological_space α] [topological_space β]
 namespace topological_space
 
 /-- Type class for noetherian spaces. It is defined to be spaces whose open sets satisfies ACC. -/
-@[mk_iff]
-class noetherian_space : Prop :=
-(well_founded : well_founded ((>) : opens α → opens α → Prop))
+@[reducible] def noetherian_space : Prop := well_founded_gt (opens α)
 
 lemma noetherian_space_iff_opens :
   noetherian_space α ↔ ∀ s : opens α, is_compact (s : set α) :=
 begin
-  rw [noetherian_space_iff, complete_lattice.well_founded_iff_is_Sup_finite_compact,
+  rw [noetherian_space, complete_lattice.well_founded_gt_iff_is_Sup_finite_compact,
     complete_lattice.is_Sup_finite_compact_iff_all_elements_compact],
   exact forall_congr opens.is_compact_element_iff,
 end
@@ -82,12 +80,12 @@ example (α : Type*) : set α ≃o (set α)ᵒᵈ := by refine order_iso.compl (
 
 lemma noetherian_space_tfae :
   tfae [noetherian_space α,
-    well_founded (λ s t : closeds α, s < t),
+    well_founded_lt (closeds α),
     ∀ s : set α, is_compact s,
     ∀ s : opens α, is_compact (s : set α)] :=
 begin
   tfae_have : 1 ↔ 2,
-  { refine (noetherian_space_iff _).trans (surjective.well_founded_iff opens.compl_bijective.2 _),
+  { refine (surjective.is_well_founded_iff opens.compl_bijective.2 _),
     exact λ s t, (order_iso.compl (set α)).lt_iff_lt.symm },
   tfae_have : 1 ↔ 4,
   { exact noetherian_space_iff_opens α },
@@ -98,6 +96,9 @@ begin
   tfae_finish
 end
 
+instance [h : noetherian_space α] : well_founded_lt (closeds α) :=
+((noetherian_space_tfae α).out 0 1).mp h
+
 variables {α β}
 
 instance {α} : noetherian_space (cofinite_topology α) :=
@@ -180,8 +181,7 @@ lemma noetherian_space.exists_finset_irreducible [noetherian_space α] (s : clos
   ∃ S : finset (closeds α), (∀ k : S, is_irreducible (k : set α)) ∧ s = S.sup id :=
 begin
   classical,
-  have := ((noetherian_space_tfae α).out 0 1).mp infer_instance,
-  apply well_founded.induction this s, clear s,
+  apply well_founded_lt.induction s, clear s,
   intros s H,
   by_cases h₁ : is_preirreducible s.1,
   cases h₂ : s.1.eq_empty_or_nonempty,