essentiallySmallOfSmall — Mathlib

English

If α is a small type, then the discrete category on α is essentially small.

Русский

Если α — маленький тип, то дискретное множество на α по существу малое.

LaTeX

$$$\operatorname{EssentiallySmall}(\mathrm{Discrete}(\alpha))$$$

Lean4

theorem essentiallySmallOfSmall {α : Type u} [Small.{w} α] : EssentiallySmall.{w} (Discrete α) :=
  ⟨⟨Discrete (Shrink α), ⟨inferInstance, ⟨Discrete.equivalence (equivShrink _)⟩⟩⟩⟩

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