small_toSet — Mathlib

English

For every i, the image toSet is Small; i.e., there is a surjection from a finite type onto toSet.

Русский

Для каждого x toSet является малым; существует сюръекция из конечного типа на toSet.

LaTeX

$$$$ \forall x : ZFSet, Small \ x.toSet. $$$$

Lean4

instance small_toSet (x : ZFSet.{u}) : Small.{u} x.toSet :=
  Quotient.inductionOn x fun a =>
    by
    let f : a.Type → (mk a).toSet := fun i => ⟨mk <| a.Func i, func_mem a i⟩
    suffices Function.Surjective f by exact small_of_surjective this
    rintro ⟨y, hb⟩
    induction y using Quotient.inductionOn
    obtain ⟨i, h⟩ := hb
    exact ⟨i, Subtype.coe_injective (Quotient.sound h.symm)⟩

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