Commit 2024-02-25 18:50 89415b39

View on Github →

feat: small_iUnion and small_sUnion (#10921) Also moves the other results about Small on sets to their own file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow.lean

Modified Mathlib/Logic/Small/Basic.lean

deleted theorem small_subset

Created Mathlib/Logic/Small/Set.lean

added theorem small_subset

Modified Mathlib/SetTheory/Cardinal/Basic.lean