small_iff_lift_mk_lt_univ — Mathlib

English

A type α is Small iff the lifted cardinal of α is below univ: lift #α < univ.

Русский

Тип α мал по определению тогда и только тогда, когда подъем кардинальности α ниже univ: lift(#α) < univ.

LaTeX

$${\\text{Small}(\\alpha) } \\iff \\operatorname{lift}(\\#\\alpha) < \\mathrm{univ}$$

Lean4

theorem small_iff_lift_mk_lt_univ {α : Type u} : Small.{v} α ↔ Cardinal.lift.{v + 1, _} #α < univ.{v, max u (v + 1)} :=
  by
  rw [lt_univ']
  constructor
  · rintro ⟨β, e⟩
    exact ⟨#β, lift_mk_eq.{u, _, v + 1}.2 e⟩
  · rintro ⟨c, hc⟩
    exact ⟨⟨c.out, lift_mk_eq.{u, _, v + 1}.1 (hc.trans (congr rfl c.mk_out.symm))⟩⟩

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