feat(set_theory/ordinal_arithmetic): out_nonempty_iff_ne_zero (#12223)

leanprover-community · Feb 22, 2022 · f7b6f42 · f7b6f42
1 parent e50ebde
commit f7b6f42
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/set_theory/ordinal.lean b/src/set_theory/ordinal.lean
@@ -775,6 +775,9 @@ begin
   exact not_lt_of_le (ordinal.zero_le _) this
 end
 
+@[simp] theorem out_nonempty_iff_ne_zero {o : ordinal} : nonempty o.out.α ↔ o ≠ 0 :=
+by rw [←not_iff_not, ←not_is_empty_iff, not_not, not_not, out_empty_iff_eq_zero]
+
 instance : has_one ordinal :=
 ⟨⟦⟨punit, empty_relation, by apply_instance⟩⟧⟩