chore(Fintype/Order): generalize Fintype to Finite in Directed lemmas (…

…#9754)

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Mathlib/Analysis/NormedSpace/PiLp.lean

@@ -309,7 +309,7 @@ use outside this file. -/
 theorem iSup_edist_ne_top_aux {ι : Type*} [Finite ι] {α : ι → Type*}
     [∀ i, PseudoMetricSpace (α i)] (f g : PiLp ∞ α) : (⨆ i, edist (f i) (g i)) ≠ ⊤ := by
   cases nonempty_fintype ι
-  obtain ⟨M, hM⟩ := Fintype.exists_le fun i => (⟨dist (f i) (g i), dist_nonneg⟩ : ℝ≥0)
+  obtain ⟨M, hM⟩ := Finite.exists_le fun i => (⟨dist (f i) (g i), dist_nonneg⟩ : ℝ≥0)
   refine' ne_of_lt ((iSup_le fun i => _).trans_lt (@ENNReal.coe_lt_top M))
   simp only [edist, PseudoMetricSpace.edist_dist, ENNReal.ofReal_eq_coe_nnreal dist_nonneg]
   exact mod_cast hM i
@@ -353,7 +353,7 @@ def pseudoMetricAux : PseudoMetricSpace (PiLp p α) :=
               rw [PseudoMetricSpace.edist_dist]
               -- Porting note: `le_ciSup` needed some help
               exact ENNReal.ofReal_le_ofReal
-                (le_ciSup (Fintype.bddAbove_range (fun k => dist (f k) (g k))) i)
+                (le_ciSup (Finite.bddAbove_range (fun k => dist (f k) (g k))) i)
     · have A : ∀ i, edist (f i) (g i) ^ p.toReal ≠ ⊤ := fun i =>
         ENNReal.rpow_ne_top_of_nonneg (zero_le_one.trans h) (edist_ne_top _ _)
       simp only [edist_eq_sum (zero_lt_one.trans_le h), dist_edist, ENNReal.toReal_rpow,
@@ -672,7 +672,7 @@ def equivₗᵢ : PiLp ∞ β ≃ₗᵢ[𝕜] ∀ i, β i :=
       suffices (Finset.univ.sup fun i => ‖f i‖₊) = ⨆ i, ‖f i‖₊ by
         simpa only [NNReal.coe_iSup] using congr_arg ((↑) : ℝ≥0 → ℝ) this
       refine'
-        antisymm (Finset.sup_le fun i _ => le_ciSup (Fintype.bddAbove_range fun i => ‖f i‖₊) _) _
+        antisymm (Finset.sup_le fun i _ => le_ciSup (Finite.bddAbove_range fun i => ‖f i‖₊) _) _
       cases isEmpty_or_nonempty ι
       · simp only [ciSup_of_empty, Finset.univ_eq_empty, Finset.sup_empty, le_rfl]
       · -- Porting note: `Finset.le_sup` needed some helps

Mathlib/Data/Fintype/Order.lean

@@ -198,35 +198,50 @@ noncomputable instance Bool.completeAtomicBooleanAlgebra : CompleteAtomicBoolean
 /-! ### Directed Orders -/
 
 
-variable {α : Type*}
+variable {α : Type*} {r : α → α → Prop} [IsTrans α r] {β γ : Type*} [Nonempty γ] {f : γ → α}
+  [Finite β] (D : Directed r f)
 
-theorem Directed.fintype_le {r : α → α → Prop} [IsTrans α r] {β γ : Type*} [Nonempty γ] {f : γ → α}
-    [Fintype β] (D : Directed r f) (g : β → γ) : ∃ z, ∀ i, r (f (g i)) (f z) := by
+theorem Directed.finite_set_le {s : Set γ} (hs : s.Finite) : ∃ z, ∀ i ∈ s, r (f i) (f z) := by
+  convert D.finset_le hs.toFinset; rw [Set.Finite.mem_toFinset]
+
+theorem Directed.finite_le (g : β → γ) : ∃ z, ∀ i, r (f (g i)) (f z) := by
   classical
-    obtain ⟨z, hz⟩ := D.finset_le (Finset.image g Finset.univ)
-    exact ⟨z, fun i => hz (g i) (Finset.mem_image_of_mem g (Finset.mem_univ i))⟩
-#align directed.fintype_le Directed.fintype_le
-
-theorem Fintype.exists_le [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] {β : Type*} [Fintype β]
-    (f : β → α) : ∃ M, ∀ i, f i ≤ M :=
-  directed_id.fintype_le _
-#align fintype.exists_le Fintype.exists_le
-
-theorem Fintype.exists_ge [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] {β : Type*} [Fintype β]
-    (f : β → α) : ∃ M, ∀ i, M ≤ f i :=
-  directed_id.fintype_le (r := (· ≥ ·)) _
-
-theorem Fintype.bddAbove_range [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] {β : Type*}
-    [Fintype β] (f : β → α) : BddAbove (Set.range f) := by
-  obtain ⟨M, hM⟩ := Fintype.exists_le f
+    obtain ⟨z, hz⟩ := D.finite_set_le (Set.finite_range g)
+    exact ⟨z, fun i => hz (g i) ⟨i, rfl⟩⟩
+#align directed.fintype_le Directed.finite_le
+
+variable [Nonempty α] [Preorder α]
+
+theorem Finite.exists_le [IsDirected α (· ≤ ·)] (f : β → α) : ∃ M, ∀ i, f i ≤ M :=
+  directed_id.finite_le _
+#align fintype.exists_le Finite.exists_le
+
+theorem Finite.exists_ge [IsDirected α (· ≥ ·)] (f : β → α) : ∃ M, ∀ i, M ≤ f i :=
+  directed_id.finite_le (r := (· ≥ ·)) _
+
+theorem Set.Finite.exists_le [IsDirected α (· ≤ ·)] {s : Set α} (hs : s.Finite) :
+    ∃ M, ∀ i ∈ s, i ≤ M :=
+  directed_id.finite_set_le hs
+
+theorem Set.Finite.exists_ge [IsDirected α (· ≥ ·)] {s : Set α} (hs : s.Finite) :
+    ∃ M, ∀ i ∈ s, M ≤ i :=
+  directed_id.finite_set_le (r := (· ≥ ·)) hs
+
+theorem Finite.bddAbove_range [IsDirected α (· ≤ ·)] (f : β → α) : BddAbove (Set.range f) := by
+  obtain ⟨M, hM⟩ := Finite.exists_le f
   refine' ⟨M, fun a ha => _⟩
   obtain ⟨b, rfl⟩ := ha
   exact hM b
-#align fintype.bdd_above_range Fintype.bddAbove_range
+#align fintype.bdd_above_range Finite.bddAbove_range
 
-theorem Fintype.bddBelow_range [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] {β : Type*}
-    [Fintype β] (f : β → α) : BddBelow (Set.range f) := by
-  obtain ⟨M, hM⟩ := Fintype.exists_ge f
+theorem Finite.bddBelow_range [IsDirected α (· ≥ ·)] (f : β → α) : BddBelow (Set.range f) := by
+  obtain ⟨M, hM⟩ := Finite.exists_ge f
   refine' ⟨M, fun a ha => _⟩
   obtain ⟨b, rfl⟩ := ha
   exact hM b
+
+@[deprecated] alias Directed.fintype_le := Directed.finite_le
+@[deprecated] alias Fintype.exists_le := Finite.exists_le
+@[deprecated] alias Fintype.exists_ge := Finite.exists_ge
+@[deprecated] alias Fintype.bddAbove_range := Finite.bddAbove_range
+@[deprecated] alias Fintype.bddBelow_range := Finite.bddBelow_range

Mathlib/ModelTheory/DirectLimit.lean

@@ -148,12 +148,12 @@ noncomputable def sigmaStructure [IsDirected ι (· ≤ ·)] [Nonempty ι] : L.S
   funMap F x :=
     ⟨_,
       funMap F
-        (unify f x (Classical.choose (Fintype.bddAbove_range fun a => (x a).1))
-          (Classical.choose_spec (Fintype.bddAbove_range fun a => (x a).1)))⟩
+        (unify f x (Classical.choose (Finite.bddAbove_range fun a => (x a).1))
+          (Classical.choose_spec (Finite.bddAbove_range fun a => (x a).1)))⟩
   RelMap R x :=
     RelMap R
-      (unify f x (Classical.choose (Fintype.bddAbove_range fun a => (x a).1))
-        (Classical.choose_spec (Fintype.bddAbove_range fun a => (x a).1)))
+      (unify f x (Classical.choose (Finite.bddAbove_range fun a => (x a).1))
+        (Classical.choose_spec (Finite.bddAbove_range fun a => (x a).1)))
 #align first_order.language.direct_limit.sigma_structure FirstOrder.Language.DirectLimit.sigmaStructure
 
 end DirectLimit
@@ -210,7 +210,7 @@ variable [Nonempty ι]
 theorem exists_unify_eq {α : Type*} [Fintype α] {x y : α → Σˣ f} (xy : x ≈ y) :
     ∃ (i : ι)(hx : i ∈ upperBounds (range (Sigma.fst ∘ x)))(hy :
       i ∈ upperBounds (range (Sigma.fst ∘ y))), unify f x i hx = unify f y i hy := by
-  obtain ⟨i, hi⟩ := Fintype.bddAbove_range (Sum.elim (fun a => (x a).1) fun a => (y a).1)
+  obtain ⟨i, hi⟩ := Finite.bddAbove_range (Sum.elim (fun a => (x a).1) fun a => (y a).1)
   rw [Sum.elim_range, upperBounds_union] at hi
   simp_rw [← Function.comp_apply (f := Sigma.fst)] at hi
   exact ⟨i, hi.1, hi.2, funext fun a => (equiv_iff G f _ _).1 (xy a)⟩
@@ -219,13 +219,13 @@ theorem exists_unify_eq {α : Type*} [Fintype α] {x y : α → Σˣ f} (xy : x
 theorem funMap_equiv_unify {n : ℕ} (F : L.Functions n) (x : Fin n → Σˣ f) (i : ι)
     (hi : i ∈ upperBounds (range (Sigma.fst ∘ x))) :
     funMap F x ≈ .mk f _ (funMap F (unify f x i hi)) :=
-  funMap_unify_equiv G f F x (Classical.choose (Fintype.bddAbove_range fun a => (x a).1)) i _ hi
+  funMap_unify_equiv G f F x (Classical.choose (Finite.bddAbove_range fun a => (x a).1)) i _ hi
 #align first_order.language.direct_limit.fun_map_equiv_unify FirstOrder.Language.DirectLimit.funMap_equiv_unify
 
 theorem relMap_equiv_unify {n : ℕ} (R : L.Relations n) (x : Fin n → Σˣ f) (i : ι)
     (hi : i ∈ upperBounds (range (Sigma.fst ∘ x))) :
     RelMap R x = RelMap R (unify f x i hi) :=
-  relMap_unify_equiv G f R x (Classical.choose (Fintype.bddAbove_range fun a => (x a).1)) i _ hi
+  relMap_unify_equiv G f R x (Classical.choose (Finite.bddAbove_range fun a => (x a).1)) i _ hi
 #align first_order.language.direct_limit.rel_map_equiv_unify FirstOrder.Language.DirectLimit.relMap_equiv_unify
 
 /-- The direct limit `setoid` respects the structure `sigmaStructure`, so quotienting by it
@@ -256,7 +256,7 @@ theorem funMap_quotient_mk'_sigma_mk' {n : ℕ} {F : L.Functions n} {i : ι} {x
     funMap F (fun a => (⟦.mk f i (x a)⟧ : DirectLimit G f)) = ⟦.mk f i (funMap F x)⟧ := by
   simp only [funMap_quotient_mk', Quotient.eq]
   obtain ⟨k, ik, jk⟩ :=
-    directed_of (· ≤ ·) i (Classical.choose (Fintype.bddAbove_range fun _ : Fin n => i))
+    directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => i))
   refine' ⟨k, jk, ik, _⟩
   simp only [Embedding.map_fun, comp_unify]
   rfl
@@ -267,14 +267,14 @@ theorem relMap_quotient_mk'_sigma_mk' {n : ℕ} {R : L.Relations n} {i : ι} {x
     RelMap R (fun a => (⟦.mk f i (x a)⟧ : DirectLimit G f)) = RelMap R x := by
   rw [relMap_quotient_mk']
   obtain ⟨k, _, _⟩ :=
-    directed_of (· ≤ ·) i (Classical.choose (Fintype.bddAbove_range fun _ : Fin n => i))
+    directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => i))
   rw [relMap_equiv_unify G f R (fun a => .mk f i (x a)) i]
   rw [unify_sigma_mk_self]
 #align first_order.language.direct_limit.rel_map_quotient_mk_sigma_mk FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk'
 
 theorem exists_quotient_mk'_sigma_mk'_eq {α : Type*} [Fintype α] (x : α → DirectLimit G f) :
     ∃ (i : ι) (y : α → G i), x = fun a => ⟦.mk f i (y a)⟧ := by
-  obtain ⟨i, hi⟩ := Fintype.bddAbove_range fun a => (x a).out.1
+  obtain ⟨i, hi⟩ := Finite.bddAbove_range fun a => (x a).out.1
   refine' ⟨i, unify f (Quotient.out ∘ x) i hi, _⟩
   ext a
   rw [Quotient.eq_mk_iff_out, unify]