coe_sep

Mathlib.SetTheory.ZFC.Class

URI: https://scilib.ai/kg/mathlib#Class.coe_sep

English

The coe of the separation of p from x is the class of elements of x satisfying p.

Русский

Образование разделения p от x через встроение даёт класс элементов x, удовлетворяющих p.

LaTeX

$$$\\text{coe\_sep}(p,x) = (\\ZFSet.sep\ p\ x : \\Class)$$$

Lean4

@[simp, norm_cast]
theorem coe_sep (p : Class.{u}) (x : ZFSet.{u}) : (ZFSet.sep p x : Class) = {y ∈ x | p y} :=
  ext fun _ => ZFSet.mem_sep

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru