Skip to content

Commit 58df4fc

Browse files
vihdzpvihdzp
committed
feat: many simp lemmas about aleph/beth/omega functions and lift (leanprover-community#37363)
1 parent 8910a13 commit 58df4fc

1 file changed

Lines changed: 220 additions & 41 deletions

File tree

‎Mathlib/SetTheory/Cardinal/Aleph.lean‎

Lines changed: 220 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -513,50 +513,12 @@ theorem aleph1_le_mk (α : Type*) [Uncountable α] : ℵ₁ ≤ #α := by
513513
theorem countable_iff_lt_aleph_one {α : Type*} (s : Set α) : s.Countable ↔ #s < ℵ₁ := by
514514
rw [lt_aleph_one_iff, le_aleph0_iff_set_countable]
515515

516-
@[deprecated aleph0_lt_lift (since := "2026-03-23")]
517-
theorem aleph_one_le_lift {c : Cardinal.{u}} : ℵ₁ ≤ lift.{v} c ↔ ℵ₁ ≤ c := by
518-
simp
519-
520-
@[deprecated (since := "2025-12-22")]
521-
alias aleph1_le_lift := aleph_one_le_lift
522-
523-
@[simp]
524-
theorem lift_le_aleph_one {c : Cardinal.{u}} : lift.{v} c ≤ ℵ₁ ↔ c ≤ ℵ₁ := by
525-
simpa using lift_le (b := ℵ₁)
526-
527-
@[deprecated (since := "2025-12-22")]
528-
alias lift_le_aleph1 := lift_le_aleph_one
529-
530-
@[simp]
531-
theorem aleph_one_lt_lift {c : Cardinal.{u}} : ℵ₁ < lift.{v} c ↔ ℵ₁ < c := by
532-
simpa using lift_lt (a := ℵ₁)
533-
534-
@[deprecated (since := "2025-12-22")]
535-
alias aleph1_lt_lift := aleph_one_lt_lift
536-
537-
@[deprecated lift_le_aleph0 (since := "2026-03-23")]
538-
theorem lift_lt_aleph_one {c : Cardinal.{u}} : lift.{v} c < ℵ₁ ↔ c < ℵ₁ := by
539-
simp
540-
541-
@[deprecated (since := "2025-12-22")]
542-
alias lift_lt_aleph1 := lift_lt_aleph_one
543-
544-
@[simp]
545-
theorem aleph_one_eq_lift {c : Cardinal.{u}} : ℵ₁ = lift.{v} c ↔ ℵ₁ = c := by
546-
simpa using lift_inj (a := ℵ₁)
547-
548-
@[deprecated (since := "2025-12-22")]
549-
alias aleph1_eq_lift := aleph_one_eq_lift
550-
551-
@[simp]
552-
theorem lift_eq_aleph_one {c : Cardinal.{u}} : lift.{v} c = ℵ₁ ↔ c = ℵ₁ := by
553-
simpa using lift_inj (b := ℵ₁)
554-
555-
@[deprecated (since := "2025-12-22")]
556-
alias lift_eq_aleph1 := lift_eq_aleph_one
516+
end Cardinal
557517

558518
/-! ### Beth cardinals -/
559519

520+
namespace Cardinal
521+
560522
/-- The "pre-beth" function is defined so that `preBeth o` is the supremum of `2 ^ preBeth a` for
561523
`a < o`. This implies `beth 0 = 0`, `beth (succ o) = 2 ^ beth o`, and that for a limit ordinal `o`,
562524
`beth o` is the supremum of `beth a` for `a < o`.
@@ -759,4 +721,221 @@ theorem isStrongLimit_beth {o : Ordinal} : IsStrongLimit (ℶ_ o) ↔ IsSuccPrel
759721
theorem lift_beth (o : Ordinal) : lift.{v} (ℶ_ o) = ℶ_ (Ordinal.lift.{v} o) := by
760722
rw [beth_eq_preBeth, beth_eq_preBeth, lift_preBeth, Ordinal.lift_add, lift_omega0]
761723

724+
/-! ### Simp lemmas with `lift` -/
725+
726+
section lift
727+
variable {c : Cardinal.{u}} {n : ℕ}
728+
729+
@[deprecated aleph0_lt_lift (since := "2026-03-23")]
730+
theorem aleph_one_le_lift : ℵ₁ ≤ lift.{v} c ↔ ℵ₁ ≤ c := by
731+
simp
732+
733+
@[deprecated (since := "2025-12-22")] alias aleph1_le_lift := aleph_one_le_lift
734+
735+
@[simp]
736+
theorem lift_le_aleph_one : lift.{v} c ≤ ℵ₁ ↔ c ≤ ℵ₁ := by
737+
simpa using lift_le (b := ℵ₁)
738+
739+
@[deprecated (since := "2025-12-22")] alias lift_le_aleph1 := lift_le_aleph_one
740+
741+
@[simp]
742+
theorem aleph_one_lt_lift : ℵ₁ < lift.{v} c ↔ ℵ₁ < c := by
743+
simpa using lift_lt (a := ℵ₁)
744+
745+
@[deprecated (since := "2025-12-22")] alias aleph1_lt_lift := aleph_one_lt_lift
746+
747+
@[deprecated lift_le_aleph0 (since := "2026-03-23")]
748+
theorem lift_lt_aleph_one : lift.{v} c < ℵ₁ ↔ c < ℵ₁ := by
749+
simp
750+
751+
@[deprecated (since := "2025-12-22")] alias lift_lt_aleph1 := lift_lt_aleph_one
752+
753+
@[simp]
754+
theorem aleph_one_eq_lift : ℵ₁ = lift.{v} c ↔ ℵ₁ = c := by
755+
simpa using lift_inj (a := ℵ₁)
756+
757+
@[deprecated (since := "2025-12-22")] alias aleph1_eq_lift := aleph_one_eq_lift
758+
759+
@[simp]
760+
theorem lift_eq_aleph_one : lift.{v} c = ℵ₁ ↔ c = ℵ₁ := by
761+
simpa using lift_inj (b := ℵ₁)
762+
763+
@[deprecated (since := "2025-12-22")] alias lift_eq_aleph1 := lift_eq_aleph_one
764+
765+
@[simp]
766+
theorem aleph_natCast_le_lift : ℵ_ n ≤ lift.{v} c ↔ ℵ_ n ≤ c := by
767+
simpa using lift_le (a := ℵ_ n)
768+
769+
@[simp]
770+
theorem lift_le_aleph_natCast : lift.{v} c ≤ ℵ_ n ↔ c ≤ ℵ_ n := by
771+
simpa using lift_le (b := ℵ_ n)
772+
773+
@[simp]
774+
theorem aleph_natCast_lt_lift : ℵ_ n < lift.{v} c ↔ ℵ_ n < c := by
775+
simpa using lift_lt (a := ℵ_ n)
776+
777+
@[simp]
778+
theorem lift_lt_aleph_natCast : lift.{v} c < ℵ_ n ↔ c < ℵ_ n := by
779+
simpa using lift_lt (b := ℵ_ n)
780+
781+
@[simp]
782+
theorem aleph_natCast_eq_lift : ℵ_ n = lift.{v} c ↔ ℵ_ n = c := by
783+
simpa using lift_inj (a := ℵ_ n)
784+
785+
@[simp]
786+
theorem lift_eq_aleph_natCast : lift.{v} c = ℵ_ n ↔ c = ℵ_ n := by
787+
simpa using lift_inj (b := ℵ_ n)
788+
789+
@[simp]
790+
theorem aleph_ofNat_le_lift [n.AtLeastTwo] : ℵ_ ofNat(n) ≤ lift.{v} c ↔ ℵ_ ofNat(n) ≤ c :=
791+
aleph_natCast_le_lift
792+
793+
@[simp]
794+
theorem lift_le_aleph_ofNat [n.AtLeastTwo] : lift.{v} c ≤ ℵ_ ofNat(n) ↔ c ≤ ℵ_ ofNat(n) :=
795+
lift_le_aleph_natCast
796+
797+
@[simp]
798+
theorem aleph_ofNat_lt_lift [n.AtLeastTwo] : ℵ_ ofNat(n) < lift.{v} c ↔ ℵ_ ofNat(n) < c :=
799+
aleph_natCast_lt_lift
800+
801+
@[simp]
802+
theorem lift_lt_aleph_ofNat [n.AtLeastTwo] : lift.{v} c < ℵ_ ofNat(n) ↔ c < ℵ_ ofNat(n) :=
803+
lift_lt_aleph_natCast
804+
805+
@[simp]
806+
theorem aleph_ofNat_eq_lift [n.AtLeastTwo] : ℵ_ ofNat(n) = lift.{v} c ↔ ℵ_ ofNat(n) = c :=
807+
aleph_natCast_eq_lift
808+
809+
@[simp]
810+
theorem lift_eq_aleph_ofNat [n.AtLeastTwo] : lift.{v} c = ℵ_ ofNat(n) ↔ c = ℵ_ ofNat(n) :=
811+
lift_eq_aleph_natCast
812+
813+
@[simp]
814+
theorem beth_natCast_le_lift : ℶ_ n ≤ lift.{v} c ↔ ℶ_ n ≤ c := by
815+
simpa using lift_le (a := ℶ_ n)
816+
817+
@[simp]
818+
theorem lift_le_beth_natCast : lift.{v} c ≤ ℶ_ n ↔ c ≤ ℶ_ n := by
819+
simpa using lift_le (b := ℶ_ n)
820+
821+
@[simp]
822+
theorem beth_natCast_lt_lift : ℶ_ n < lift.{v} c ↔ ℶ_ n < c := by
823+
simpa using lift_lt (a := ℶ_ n)
824+
825+
@[simp]
826+
theorem lift_lt_beth_natCast : lift.{v} c < ℶ_ n ↔ c < ℶ_ n := by
827+
simpa using lift_lt (b := ℶ_ n)
828+
829+
@[simp]
830+
theorem beth_natCast_eq_lift : ℶ_ n = lift.{v} c ↔ ℶ_ n = c := by
831+
simpa using lift_inj (a := ℶ_ n)
832+
833+
@[simp]
834+
theorem lift_eq_beth_natCast : lift.{v} c = ℶ_ n ↔ c = ℶ_ n := by
835+
simpa using lift_inj (b := ℶ_ n)
836+
837+
@[simp]
838+
theorem beth_ofNat_le_lift [n.AtLeastTwo] : ℶ_ ofNat(n) ≤ lift.{v} c ↔ ℶ_ ofNat(n) ≤ c :=
839+
beth_natCast_le_lift
840+
841+
@[simp]
842+
theorem lift_le_beth_ofNat [n.AtLeastTwo] : lift.{v} c ≤ ℶ_ ofNat(n) ↔ c ≤ ℶ_ ofNat(n) :=
843+
lift_le_beth_natCast
844+
845+
@[simp]
846+
theorem beth_ofNat_lt_lift [n.AtLeastTwo] : ℶ_ ofNat(n) < lift.{v} c ↔ ℶ_ ofNat(n) < c :=
847+
beth_natCast_lt_lift
848+
849+
@[simp]
850+
theorem lift_lt_beth_ofNat [n.AtLeastTwo] : lift.{v} c < ℶ_ ofNat(n) ↔ c < ℶ_ ofNat(n) :=
851+
lift_lt_beth_natCast
852+
853+
@[simp]
854+
theorem beth_ofNat_eq_lift [n.AtLeastTwo] : ℶ_ ofNat(n) = lift.{v} c ↔ ℶ_ ofNat(n) = c :=
855+
beth_natCast_eq_lift
856+
857+
@[simp]
858+
theorem lift_eq_beth_ofNat [n.AtLeastTwo] : lift.{v} c = ℶ_ ofNat(n) ↔ c = ℶ_ ofNat(n) :=
859+
lift_eq_beth_natCast
860+
861+
end lift
762862
end Cardinal
863+
864+
namespace Ordinal
865+
section lift
866+
variable {o : Ordinal.{u}} {n : ℕ}
867+
868+
@[simp]
869+
theorem omega_one_le_lift : ω₁ ≤ lift.{v} o ↔ ω₁ ≤ o := by
870+
simpa using lift_le (a := ω₁)
871+
872+
@[simp]
873+
theorem lift_le_omega_one : lift.{v} o ≤ ω₁ ↔ o ≤ ω₁ := by
874+
simpa using lift_le (b := ω₁)
875+
876+
@[simp]
877+
theorem omega_one_lt_lift : ω₁ < lift.{v} o ↔ ω₁ < o := by
878+
simpa using lift_lt (a := ω₁)
879+
880+
@[simp]
881+
theorem lift_lt_omega_one : lift.{v} o < ω₁ ↔ o < ω₁ := by
882+
simpa using lift_lt (b := ω₁)
883+
884+
@[simp]
885+
theorem omega_one_eq_lift : ω₁ = lift.{v} o ↔ ω₁ = o := by
886+
simpa using lift_inj (a := ω₁)
887+
888+
@[simp]
889+
theorem lift_eq_omega_one : lift.{v} o = ω₁ ↔ o = ω₁ := by
890+
simpa using lift_inj (b := ω₁)
891+
892+
@[simp]
893+
theorem omega_natCast_le_lift : ω_ n ≤ lift.{v} o ↔ ω_ n ≤ o := by
894+
simpa using lift_le (a := ω_ n)
895+
896+
@[simp]
897+
theorem lift_le_omega_natCast : lift.{v} o ≤ ω_ n ↔ o ≤ ω_ n := by
898+
simpa using lift_le (b := ω_ n)
899+
900+
@[simp]
901+
theorem omega_natCast_lt_lift : ω_ n < lift.{v} o ↔ ω_ n < o := by
902+
simpa using lift_lt (a := ω_ n)
903+
904+
@[simp]
905+
theorem lift_lt_omega_natCast : lift.{v} o < ω_ n ↔ o < ω_ n := by
906+
simpa using lift_lt (b := ω_ n)
907+
908+
@[simp]
909+
theorem omega_natCast_eq_lift : ω_ n = lift.{v} o ↔ ω_ n = o := by
910+
simpa using lift_inj (a := ω_ n)
911+
912+
@[simp]
913+
theorem lift_eq_omega_natCast : lift.{v} o = ω_ n ↔ o = ω_ n := by
914+
simpa using lift_inj (b := ω_ n)
915+
916+
@[simp]
917+
theorem omega_ofNat_le_lift [n.AtLeastTwo] : ω_ ofNat(n) ≤ lift.{v} o ↔ ω_ ofNat(n) ≤ o :=
918+
omega_natCast_le_lift
919+
920+
@[simp]
921+
theorem lift_le_omega_ofNat [n.AtLeastTwo] : lift.{v} o ≤ ω_ ofNat(n) ↔ o ≤ ω_ ofNat(n) :=
922+
lift_le_omega_natCast
923+
924+
@[simp]
925+
theorem omega_ofNat_lt_lift [n.AtLeastTwo] : ω_ ofNat(n) < lift.{v} o ↔ ω_ ofNat(n) < o :=
926+
omega_natCast_lt_lift
927+
928+
@[simp]
929+
theorem lift_lt_omega_ofNat [n.AtLeastTwo] : lift.{v} o < ω_ ofNat(n) ↔ o < ω_ ofNat(n) :=
930+
lift_lt_omega_natCast
931+
932+
@[simp]
933+
theorem omega_ofNat_eq_lift [n.AtLeastTwo] : ω_ ofNat(n) = lift.{v} o ↔ ω_ ofNat(n) = o :=
934+
omega_natCast_eq_lift
935+
936+
@[simp]
937+
theorem lift_eq_omega_ofNat [n.AtLeastTwo] : lift.{v} o = ω_ ofNat(n) ↔ o = ω_ ofNat(n) :=
938+
lift_eq_omega_natCast
939+
940+
end lift
941+
end Ordinal

0 commit comments

Comments
 (0)