feat(SetTheory/Ordinal/Basic): the #s-th element of α is an upper-bound for the set's mex (#36539)

This is a translation of `card_typein_min_le_mk` to be in terms of `α`.

Author: SnirBroshi

Mathlib/AlgebraicGeometry/Properties.lean

@@ -249,12 +249,12 @@ instance Scheme.component_nontrivial (X : Scheme.{u}) (U : X.Opens) [Nonempty U]
 set_option backward.isDefEq.respectTransparency false in
 instance irreducibleSpace_of_isIntegral [IsIntegral X] : IrreducibleSpace X := by
   by_contra H
-  replace H : ¬IsPreirreducible (⊤ : Set X) := fun h =>
+  replace H : ¬IsPreirreducible .univ := fun h =>
     H { toPreirreducibleSpace := ⟨h⟩
         toNonempty := inferInstance }
   simp_rw [isPreirreducible_iff_isClosed_union_isClosed, not_forall, not_or] at H
   rcases H with ⟨S, T, hS, hT, h₁, h₂, h₃⟩
-  rw [Set.not_top_subset] at h₂ h₃
+  rw [Set.not_univ_subset] at h₂ h₃
   haveI : Nonempty (⟨Sᶜ, hS.1⟩ : X.Opens) := ⟨⟨_, h₂.choose_spec⟩⟩
   haveI : Nonempty (⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, h₃.choose_spec⟩⟩
   haveI : Nonempty (⟨Sᶜ, hS.1⟩ ⊔ ⟨Tᶜ, hT.1⟩ : X.Opens) := ⟨⟨_, Or.inl h₂.choose_spec⟩⟩

Mathlib/Data/Set/Basic.lean

@@ -296,9 +296,13 @@ theorem subset_iff_notMem : s ⊆ t ↔ ∀ ⦃a⦄, a ∉ t → a ∉ s := by
 theorem not_subset : ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t := by
   simp only [subset_def, not_forall, exists_prop]
 
-theorem not_top_subset : ¬⊤ ⊆ s ↔ ∃ a, a ∉ s := by
+theorem not_univ_subset : ¬univ ⊆ s ↔ ∃ a, a ∉ s := by
   simp [not_subset]
 
+@[deprecated not_univ_subset (since := "2026-03-12")]
+theorem not_top_subset : ¬⊤ ⊆ s ↔ ∃ a, a ∉ s :=
+  not_univ_subset
+
 lemma eq_of_forall_subset_iff (h : ∀ u, s ⊆ u ↔ t ⊆ u) : s = t := eq_of_forall_ge_iff h
 
 /-! ### Definition of strict subsets `s ⊂ t` and basic properties. -/
@@ -569,6 +573,18 @@ theorem univ_unique [Unique α] : @Set.univ α = {default} :=
 theorem ssubset_univ_iff : s ⊂ univ ↔ s ≠ univ :=
   lt_top_iff_ne_top
 
+theorem ssubset_univ_iff_nonempty_compl : s ⊂ univ ↔ sᶜ.Nonempty := by
+  rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]
+  simp
+
+alias ⟨_, Nonempty.ssubset_univ⟩ := ssubset_univ_iff_nonempty_compl
+
+theorem compl_ssubset_univ : sᶜ ⊂ univ ↔ s.Nonempty := by
+  rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]
+  simp
+
+alias ⟨_, Nonempty.compl_ssubset_univ⟩ := compl_ssubset_univ
+
 instance nontrivial_of_nonempty [Nonempty α] : Nontrivial (Set α) :=
   ⟨⟨∅, univ, empty_ne_univ⟩⟩
 

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -612,7 +612,7 @@ theorem card_one : card 1 = 1 := mk_eq_one _
 
 variable (r) in
 /-- The cardinality of a set is an upper-bound for the cardinality of the order type of the set's
-mex (minimum excluded value) -/
+mex (minimum excluded value). See `not_lt_enum_ord_mk_min_compl` for the `α` version. -/
 theorem card_typein_min_le_mk [IsWellOrder α r] {s : Set α} (hs : sᶜ.Nonempty) :
     (typein r <| IsWellFounded.wf.min (r := r) sᶜ hs).card ≤ #s :=
   IsWellFounded.wf.cardinalMk_subtype_lt_min_compl_le hs
@@ -1438,12 +1438,33 @@ theorem card_eq_ofNat {o} {n : ℕ} [n.AtLeastTwo] :
     card o = ofNat(n) ↔ o = OfNat.ofNat n :=
   card_eq_nat
 
+variable (r) in
 @[simp]
-theorem type_fintype (r : α → α → Prop) [IsWellOrder α r] [Fintype α] :
+theorem type_fintype [IsWellOrder α r] [Fintype α] :
     type r = Fintype.card α := by rw [← card_eq_nat, card_type, mk_fintype]
 
 theorem type_fin (n : ℕ) : typeLT (Fin n) = n := by simp
 
+variable (r) in
+theorem ord_mk_le_type [IsWellOrder α r] (s : Set α) : (#s).ord ≤ type r := by
+  grw [← ord_le_type, ord_le_ord, le_mk_iff_exists_set]
+  use s
+
+variable (r) in
+theorem ord_mk_lt_type [IsWellOrder α r] {s : Set α} (hfin : s.Finite) (h : sᶜ.Nonempty) :
+    (#s).ord < type r := by
+  grw [← ord_le_type, ord_lt_ord, ← mk_univ (α := α)]
+  exact card_lt_card_of_left_finite hfin h.ssubset_univ
+
+variable (r) in
+/-- The `#s`-th element of `α` is an upper-bound for the set's mex (minimum excluded value),
+ordered by `r`, when `s` is finite. See `card_typein_min_le_mk` for the `Ordinal` version. -/
+theorem not_lt_enum_ord_mk_min_compl [IsWellOrder α r] {s : Set α} (hfin : s.Finite)
+    (h : sᶜ.Nonempty) :
+    ¬r (enum r ⟨#s |>.ord, ord_mk_lt_type r hfin h⟩) (IsWellFounded.wf.min (r := r) sᶜ h) := by
+  grw [← typein_le_typein, typein_enum, Cardinal.le_ord_iff_card_le_of_lt_aleph0 _ hfin.lt_aleph0,
+    card_typein_min_le_mk]
+
 end Ordinal
 
 /-! ### Sorted lists -/