diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index a487a36c7b89d4..76d887955eb8e6 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -942,6 +942,14 @@ theorem mk_preimage_of_subset_range (f : α → β) (s : Set β) (h : s ⊆ rang rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)] exact mk_preimage_of_subset_range_lift f s h +open Set.Notation in +theorem mk_preimage_val_le_left (s t : Set α) : #(s ↓∩ t) ≤ #s := + mk_set_le _ + +open Set.Notation in +theorem mk_preimage_val_le_right (s t : Set α) : #(s ↓∩ t) ≤ #t := + mk_preimage_of_injective _ _ Subtype.val_injective + theorem mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : Set α} {t : Set β} (h : t ⊆ f '' s) : lift.{u} #t ≤ lift.{v} #({ x ∈ s | f x ∈ t } : Set α) := by rw [image_eq_range] at h diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean index 4cbeee18f776f1..37b70cdc971a40 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean @@ -17,7 +17,7 @@ cardinality of a cofinal subset. public noncomputable section -open Function Cardinal Set Order +open Cardinal Set Order universe u v w @@ -164,21 +164,21 @@ section Congr variable [Preorder α] [Preorder β] [Preorder γ] theorem GaloisConnection.cof_le_lift {f : β → α} {g : α → β} (h : GaloisConnection f g) : - Cardinal.lift.{u} (Order.cof β) ≤ Cardinal.lift.{v} (Order.cof α) := by + Cardinal.lift.{u} (cof β) ≤ Cardinal.lift.{v} (cof α) := by rw [le_lift_cof_iff] exact fun s hs ↦ (lift_le.2 <| cof_le (h.map_isCofinal hs)).trans mk_image_le_lift theorem GaloisConnection.cof_le {f : γ → α} {g : α → γ} (h : GaloisConnection f g) : - Order.cof γ ≤ Order.cof α := by + cof γ ≤ cof α := by simpa using h.cof_le_lift theorem OrderIso.lift_cof_congr (f : α ≃o β) : - Cardinal.lift.{v} (Order.cof α) = Cardinal.lift.{u} (Order.cof β) := + Cardinal.lift.{v} (cof α) = Cardinal.lift.{u} (cof β) := f.to_galoisConnection.cof_le_lift.antisymm (f.symm.to_galoisConnection.cof_le_lift) @[deprecated (since := "2026-03-20")] alias OrderIso.lift_cof_eq := OrderIso.lift_cof_congr -theorem OrderIso.cof_congr (f : α ≃o γ) : Order.cof α = Order.cof γ := by +theorem OrderIso.cof_congr (f : α ≃o γ) : cof α = cof γ := by simpa using f.lift_cof_congr @[deprecated (since := "2026-03-20")] alias OrderIso.cof_eq := OrderIso.cof_congr @@ -191,7 +191,7 @@ end Congr /-- If the union of `s` is cofinal and `s` is smaller than the cofinality, then `s` has a cofinal member. -/ theorem isCofinal_of_isCofinal_sUnion {α : Type*} [LinearOrder α] {s : Set (Set α)} - (h₁ : IsCofinal (⋃₀ s)) (h₂ : #s < Order.cof α) : ∃ x ∈ s, IsCofinal x := by + (h₁ : IsCofinal (⋃₀ s)) (h₂ : #s < cof α) : ∃ x ∈ s, IsCofinal x := by contrapose! h₂ simp_rw [not_isCofinal_iff] at h₂ choose f hf using h₂ @@ -202,7 +202,81 @@ theorem isCofinal_of_isCofinal_sUnion {α : Type*} [LinearOrder α] {s : Set (Se /-- If the union of the `ι`-indexed family `s` is cofinal and `ι` is smaller than the cofinality, then `s` has a cofinal member. -/ theorem isCofinal_of_isCofinal_iUnion {α : Type*} {ι} [LinearOrder α] {s : ι → Set α} - (h₁ : IsCofinal (⋃ i, s i)) (h₂ : #ι < Order.cof α) : ∃ i, IsCofinal (s i) := by + (h₁ : IsCofinal (⋃ i, s i)) (h₂ : #ι < cof α) : ∃ i, IsCofinal (s i) := by rw [← sUnion_range] at h₁ obtain ⟨_, ⟨i, rfl⟩, h⟩ := isCofinal_of_isCofinal_sUnion h₁ (mk_range_le.trans_lt h₂) exact ⟨i, h⟩ + +/-! ### Cofinality within order -/ + +namespace Order +variable {x : α} + +section Preorder +variable [Preorder α] + +/-- The cofinality of an element `x` within a preorder is defined as `cof (Iio x)`. -/ +def cofWithin (x : α) : Cardinal := + cof (Iio x) + +@[simp] +theorem cof_Iio (x : α) : cof (Iio x) = cofWithin x := + (rfl) + +theorem cofWithin_le {s : Set α} (hs : IsCofinalFor (Iio x) s) (hsx : s ⊆ Iio x) : + cofWithin x ≤ #s := by + refine (cof_le fun ⟨y, hy⟩ ↦ ?_).trans <| mk_preimage_val_le_right .. + obtain ⟨z, hz, hyz⟩ := hs hy + exact ⟨⟨z, hsx hz⟩, hz, hyz⟩ + +@[simp] +theorem cofWithin_eq_zero_iff : cofWithin x = 0 ↔ IsMin x := by + rw [cofWithin, cof_eq_zero_iff, isEmpty_coe_sort, Iio_eq_empty_iff] + +@[simp] +theorem cofWithin_bot [OrderBot α] : cofWithin (⊥ : α) = 0 := + cofWithin_eq_zero_iff.2 isMin_bot + +end Preorder + +section LinearOrder +variable [LinearOrder α] [LinearOrder β] + +@[simp] +theorem cofWithin_lt_aleph0_iff : cofWithin x < ℵ₀ ↔ cofWithin x ≤ 1 := + cof_lt_aleph0_iff + +@[simp] +theorem aleph0_le_cofWithin_iff : ℵ₀ ≤ cofWithin x ↔ 1 < cofWithin x := + aleph0_le_cof_iff + +theorem cofWithin_eq_one_iff : cofWithin x = 1 ↔ ¬ IsSuccPrelimit x := by + rw [cofWithin, cof_eq_one_iff] + unfold IsTop IsSuccPrelimit CovBy + simp [← not_lt, imp_not_comm] + +theorem cofWithin_ne_one_iff : cofWithin x ≠ 1 ↔ IsSuccPrelimit x := by + rw [ne_eq, cofWithin_eq_one_iff, not_not] + +theorem cofWithin_le_one_iff : cofWithin x ≤ 1 ↔ ¬ IsSuccLimit x := by + rw [Cardinal.le_one_iff, cofWithin_eq_zero_iff, cofWithin_eq_one_iff, + IsSuccLimit, not_and_or, not_not] + +theorem one_lt_cofWithin_iff : 1 < cofWithin x ↔ IsSuccLimit x := by + rw [← not_le, cofWithin_le_one_iff, not_not] + +alias ⟨_, IsSuccPrelimit.cofWithin_ne_one⟩ := cofWithin_ne_one_iff +alias ⟨_, IsSuccLimit.one_lt_cofWithin⟩ := one_lt_cofWithin_iff + +theorem IsSuccLimit.cofWithin_ne_one (hx : IsSuccLimit x) : cofWithin x ≠ 1 := + hx.one_lt_cofWithin.ne' + +theorem cofWithin_succ_of_not_isMax (hx : ¬ IsMax x) [SuccOrder α] : cofWithin (succ x) = 1 := + cofWithin_eq_one_iff.2 (mt IsSuccPrelimit.isMax hx) + +@[simp] +theorem cofWithin_succ (x : α) [SuccOrder α] [NoMaxOrder α] : cofWithin (succ x) = 1 := + cofWithin_succ_of_not_isMax (not_isMax x) + +end LinearOrder +end Order diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index 19beb23372c63a..f14bfa534d1875 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -43,6 +43,7 @@ theorem Order.cof_int : cof ℤ = ℵ₀ := by simp namespace Ordinal /-- The cofinality on an ordinal is the `Order.cof` of any isomorphic linear order. +This is the same as `Order.cofWithin`, but without the universe bump. In particular, `cof 0 = 0` and `cof (succ o) = 1`. -/ def cof (o : Ordinal.{u}) : Cardinal.{u} := @@ -61,6 +62,12 @@ theorem cof_type (α : Type*) [LinearOrder α] [WellFoundedLT α] : theorem cof_toType (o : Ordinal) : Order.cof o.ToType = o.cof := by conv_rhs => rw [← type_toType o, cof_type] +@[simp] +theorem cof_typein [LinearOrder α] [WellFoundedLT α] (x : α) : + cof (typein (α := α) (· < ·) x) = cofWithin x := by + rw [← cof_Iio] + exact cof_type _ + @[deprecated (since := "2026-02-18")] alias cof_eq_cof_toType := cof_toType @[deprecated (since := "2026-02-18")] alias le_cof_type := le_cof_iff @[deprecated (since := "2026-02-18")] alias cof_type_le := cof_le @@ -73,13 +80,14 @@ theorem lift_cof (o : Ordinal.{u}) : Cardinal.lift.{v} (cof o) = cof (Ordinal.li rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)), ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr] -theorem _root_.Order.cof_Iio [LinearOrder α] [WellFoundedLT α] (x : α) : - Order.cof (Iio x) = cof (typein (α := α) (· < ·) x) := - (cof_type _).symm - @[simp] -theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) := by - rw [Order.cof_Iio, typein_ordinal] +theorem _root_.Order.cofWithin_ordinal (o : Ordinal.{u}) : cofWithin o = cof (lift.{u + 1} o) := by + rw [← cof_typein, typein_ordinal] + +@[deprecated cofWithin_ordinal (since := "2026-05-22")] +protected theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) := by + rw [cof_Iio] + exact cofWithin_ordinal o theorem cof_le_card (o : Ordinal) : cof o ≤ card o := by simpa using cof_le_cardinalMk o.ToType @@ -265,7 +273,7 @@ theorem sSup_add_one_lt_of_lt_cof {s : Set Ordinal.{u}} {a : Ordinal.{u}} · simp [hs] · rintro rfl rw [← lift_cof, ← Cardinal.lift_lt.{_, u + 2}, Cardinal.lift_lift, - lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, ← lift_cof, cof_type, + lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, cofWithin_ordinal, ← lift_cof, cof_type, Cardinal.lift_lift, Cardinal.lift_lt] at ha exact ha.not_ge (cof_le_cardinalMk _)