instSmallElemInvSet — Mathlib

English

For every a, invSet(a) is a small (countable) type; i.e., invSet(a) has a small universe embedding.

Русский

Для каждого a множество invSet(a) является малым (перечислимым) типом; то есть существует встраивание в малое множество.

LaTeX

$$$ \forall a,\ Small\, a.invSet$$$

Lean4

instance (a : Nimber.{u}) : Small.{u} (invSet a) :=
  by
  refine @small_subset.{u, u + 1} _ _ _ ?_ (small_range (@List.toNimber a))
  refine fun x hx ↦ invSet_recOn a ⟨[], rfl⟩ ?_ x hx
  rintro a' ha _ _ ⟨l, rfl⟩
  use Ordinal.enumIsoToType _ ⟨toOrdinal a', ha⟩ :: l
  rw [List.toNimber]
  simp

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