small_lift

Mathlib.Logic.Small.Defs

URI: https://scilib.ai/kg/mathlib#small_lift

English

If α is Small in universe v, then α is Small in universe max(v,w).

Русский

Если α мала во вселенной v, то она мала во вселенной max(v,w).

LaTeX

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

Lean4

theorem small_lift (α : Type u) [hα : Small.{v} α] : Small.{max v w} α :=
  let ⟨⟨_, ⟨f⟩⟩⟩ := hα
  Small.mk' <| f.trans (Equiv.ulift.{w}).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru