refactor(set_theory/cardinal_ordinal): aleph_is_principal_aleph → `…

…principal_add_aleph` (#12663) This matches the naming scheme used throughout `set_theory/principal.lean`.
leanprover-community · Mar 14, 2022 · 7b7fea5 · 7b7fea5
1 parent 6ebb378
commit 7b7fea5
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/set_theory/cardinal_ordinal.lean b/src/set_theory/cardinal_ordinal.lean
@@ -525,11 +525,11 @@ protected lemma eq_of_add_eq_add_right {a b c : cardinal} (h : a + b = c + b) (h
   a = c :=
 by { rw [add_comm a b, add_comm c b] at h, exact cardinal.eq_of_add_eq_add_left h hb }
 
-theorem ord_is_principal_add {c : cardinal} (hc : ω ≤ c) : ordinal.principal (+) c.ord :=
+theorem principal_add_ord {c : cardinal} (hc : ω ≤ c) : ordinal.principal (+) c.ord :=
 λ a b ha hb, by { rw [lt_ord, ordinal.card_add] at *, exact add_lt_of_lt hc ha hb }
 
-theorem aleph_is_principal_add (o : ordinal) : ordinal.principal (+) (aleph o).ord :=
-ord_is_principal_add $ omega_le_aleph o
+theorem principal_add_aleph (o : ordinal) : ordinal.principal (+) (aleph o).ord :=
+principal_add_ord $ omega_le_aleph o
 
 /-! ### Properties about power -/