Mathlib v3 is deprecated. Go to Mathlib v4

Theorem small_subset

Modification history

2022-03-16 08:21
src/logic/small.lean
feat(set_theory/ordinal_arithmetic): A set of ordinals is bounded above iff it's small (#11870)
Added small_subsetView on Github →