English
For any class A, iota A is an element of the universe: iota A ∈ univ.
Русский
Для любого класса A элемент iota A принадлежит вселенной: iota A ∈ univ.
LaTeX
$$$ iota(A) \\in \\mathrm{univ}. $$$
Lean4
/-- Unlike the other set constructors, the `iota` definite descriptor
is a set for any set input, but not constructively so, so there is no
associated `Class → Set` function. -/
theorem iota_ex (A) : iota.{u} A ∈ univ.{u} :=
mem_univ.2 <|
Or.elim (Classical.em <| ∃ x, ∀ y, A y ↔ y = x) (fun ⟨x, h⟩ => ⟨x, Eq.symm <| iota_val A x h⟩) fun hn =>
⟨∅, ext fun _ => coe_empty.symm ▸ ⟨False.rec, fun ⟨_, ⟨x, rfl, H⟩, _⟩ => hn ⟨x, H⟩⟩⟩
