Theorem small_subset

Modification history

2024-09-12 07:15

Mathlib/Logic/Small/Set.lean

feat: `Small.{u}` sets are closed under various operations (#11126) …

Modified small_subset View on Github →

2024-02-25 18:50

Mathlib/Logic/Small/Basic.lean

feat: `small_iUnion` and `small_sUnion` (#10921) …

Modified small_subset View on Github →

2022-12-17 09:18

Mathlib/Logic/Small/Basic.lean

feat port: Logic.Small.Basic (#1079) …

Added small_subset View on Github →