Commit 2024-08-11 04:28 bc89bc5b

View on Github →

chore(SetTheory/Ordinal): remove bare open Classical (#15670)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

modified theorem Cardinal.mk_sum_compl

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

modified theorem Cardinal.mk_finset_of_infinite

modified theorem Cardinal.mk_multiset_of_countable

modified theorem Cardinal.mk_multiset_of_nonempty

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Ordinal.lift_pred

modified theorem Ordinal.lt_pred

modified theorem Ordinal.pred_le_self

modified theorem Ordinal.zero_or_succ_or_limit

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Exponential.lean