small_max — Mathlib

English

There is a preferred lifting of smallness to the maximum universe: for any α, Small^{max(v,w)} α.

Русский

Существует переносимость мелкости в максимальную вселенную: для любого α верно Small^{max(v,w)} α.

LaTeX

$$$\forall \alpha, Small^{\max(v,w)}(\alpha).$$$

Lean4

/-- Due to https://github.com/leanprover/lean4/issues/2297, this is useless as an instance.

See however `Logic.UnivLE`, whose API is able to indirectly provide this instance. -/
theorem small_max (α : Type v) : Small.{max w v} α :=
  small_lift.{v, w} α

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