feat(set_theory/ordinal/basic): max a 0 = a (#13734)

leanprover-community · Apr 28, 2022 · 0cb20fc · 0cb20fc
1 parent 98e7848
commit 0cb20fc
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/set_theory/ordinal/basic.lean b/src/set_theory/ordinal/basic.lean
@@ -1203,6 +1203,10 @@ wf.conditionally_complete_linear_order_with_bot 0 $ le_antisymm (ordinal.zero_le
 
 @[simp] lemma bot_eq_zero : (⊥ : ordinal) = 0 := rfl
 
+@[simp] lemma max_zero_left : ∀ a : ordinal, max 0 a = a := max_bot_left
+@[simp] lemma max_zero_right : ∀ a : ordinal, max a 0 = a := max_bot_right
+@[simp] lemma max_eq_zero {a b : ordinal} : max a b = 0 ↔ a = 0 ∧ b = 0 := max_eq_bot
+
 protected theorem not_lt_zero (o : ordinal) : ¬ o < 0 :=
 not_lt_bot