congToClass — Mathlib

English

Convert a conglomerate (a set of classes) into a single class by collecting those y with ↑y ∈ x.

Русский

Преобразование конгломерата в единый класс через те y, для которых ↑y ∈ x.

LaTeX

$$$\\\\mathrm{congToClass}(x) = \\{ y \\\\mid \\\\uparrow y \\in x \\}$$$

Lean4

/-- Convert a conglomerate (a collection of classes) into a class -/
def congToClass (x : Set Class.{u}) : Class.{u} :=
  {y | ↑y ∈ x}

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