instWellPoweredType — Mathlib

English

The category of Types is well-powered; equivalently, subobjects of any type form a set (are small).

Русский

Категория типов хорошо упорядочена; эквивалентно, подобъекты типа образуют множество (они малы).

LaTeX

$$$\text{WellPowered}(\mathrm{Type})$$$

Lean4

instance : WellPowered.{u} (Type u) :=
  wellPowered_of_essentiallySmall_monoOver fun α => EssentiallySmall.mk' (Types.monoOverEquivalenceSet α)

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