Move more

Mathlib/Logic/Small/Set.lean

@@ -12,17 +12,22 @@
 
 universe u v w
 
+theorem small_subset {α : Type v} {s t : Set α} (hts : t ⊆ s) [Small.{u} s] : Small.{u} t :=
+  let f : t → s := fun x => ⟨x, hts x.prop⟩
+  @small_of_injective _ _ _ f fun _ _ hxy => Subtype.ext (Subtype.mk.inj hxy)
+#align small_subset small_subset
+
 instance small_range {α : Type v} {β : Type w} (f : α → β) [Small.{u} α] :
     Small.{u} (Set.range f) :=
   small_of_surjective Set.surjective_onto_range
 #align small_range small_range
 
 instance small_image {α : Type v} {β : Type w} (f : α → β) (S : Set α) [Small.{u} S] :
     Small.{u} (f '' S) :=
   small_of_surjective Set.surjective_onto_image
 #align small_image small_image
 
 instance small_union {α : Type v} (s t : Set α) [Small.{u} s] [Small.{u} t] :
     Small.{u} (s ∪ t : Set α) := by
   rw [← Subtype.range_val (s := s), ← Subtype.range_val (s := t), ← Set.Sum.elim_range]
   infer_instance