small_univ_iff — Mathlib

English

Let α be a type. Then α is small in universe u if and only if Set.univ α is small in universe u.

Русский

Пусть α — тип. Тогда α является малым в вселенной u тогда и только тогда, когда множество Set.univ α является малым той же вселенной.

LaTeX

$$$\operatorname{Small}(\mathrm{Set.univ}(\alpha)) \iff \operatorname{Small}(\alpha)$$

Lean4

theorem small_univ_iff : Small.{u} (@Set.univ α) ↔ Small.{u} α :=
  small_congr <| Equiv.Set.univ α

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