small_subtype — Mathlib

English

If α is small, then any subtype of α defined by a predicate P is also small: Small (Subtype P).

Русский

Если α является малым, то любой подтип α, заданный свойством P, тоже мал: Small (Subtype P).

LaTeX

$$$ \\text{Small}(\\operatorname{Subtype} P) $$$

Lean4

instance small_subtype (α : Type v) [Small.{w} α] (P : α → Prop) : Small.{w} { x // P x } :=
  small_map (equivShrink α).subtypeEquivOfSubtype'

Похожие утверждения