small_subset

theorem small_subset : ∀ {α : Type v} {s t : Set α}, t ⊆ s → ∀ [inst : Small.{u, v} ↑s], Small.{u, v} ↑t

The theorem `small_subset` states that for any type `α` and for any two sets `s` and `t` of that type, if `t` is a subset of `s` and if `s` is a "small" set (where "small" is defined by the `Small.{u, v}` typeclass), then `t` is also a small set. This theorem asserts that the property of being "small" is preserved under taking subsets.

More concisely: If `s` is a small set and `t` is a subset of `s`, then `t` is also a small set.