trans_univLE — Mathlib

English

If α is small at level w and UnivLE relates w to v, then α is small at level v.

Русский

Если α мал по уровню w и существует отношение UnivLE между w и v, то α мал на уровне v.

LaTeX

$$$\text{Small}_{v}(\alpha)$$$

Lean4

theorem trans_univLE (α : Type w) [hα : Small.{u} α] [h : UnivLE.{u, v}] : Small.{v} α :=
  let ⟨β, ⟨f⟩⟩ := hα.equiv_small
  let ⟨_, ⟨g⟩⟩ := (h.small β).equiv_small
  ⟨_, ⟨f.trans g⟩⟩

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