Commit 2024-10-22 15:31 e7dbdb48

View on Github →

chore: use new ℵ_ and ℶ_ notation (#18066)

Estimated changes

Modified Counterexamples/Phillips.lean

modified theorem Counterexample.Phillips1940.apply_f_eq_continuousPart

modified theorem Counterexample.Phillips1940.comp_ae_eq_const

modified theorem Counterexample.Phillips1940.countable_compl_spf

modified theorem Counterexample.Phillips1940.countable_ne

modified theorem Counterexample.Phillips1940.countable_spf_mem

modified def Counterexample.Phillips1940.f

modified theorem Counterexample.Phillips1940.integrable_comp

modified theorem Counterexample.Phillips1940.integral_comp

modified theorem Counterexample.Phillips1940.measurable_comp

modified theorem Counterexample.Phillips1940.no_pettis_integral

modified theorem Counterexample.Phillips1940.norm_bound

modified theorem Counterexample.Phillips1940.sierpinski_pathological_family

modified def Counterexample.Phillips1940.spf

Modified Mathlib/Order/Filter/CardinalInter.lean

modified theorem Filter.cardinalInterFilter_aleph0

Modified Mathlib/Order/Filter/CountableInter.lean

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

modified theorem Cardinal.aleph0_le_aleph

modified theorem Cardinal.aleph_pos

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

modified theorem Cardinal.aleph0_mul_aleph

modified theorem Cardinal.aleph_add_aleph

modified theorem Cardinal.aleph_mul_aleph0

modified theorem Cardinal.aleph_mul_aleph

modified theorem Cardinal.principal_add_aleph

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

modified theorem Cardinal.isRegular_aleph_one

modified theorem Cardinal.isRegular_aleph_succ

modified theorem Cardinal.isStrongLimit_beth

modified theorem Ordinal.aleph_cof