sep

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.sep

Lean4

/-- `{x ∈ a | p x}` is the set of elements in `a` satisfying `p` -/
protected def sep (p : ZFSet → Prop) : ZFSet → ZFSet :=
  Quotient.map (PSet.sep fun y => p (mk y)) fun ⟨α, A⟩ ⟨β, B⟩ ⟨αβ, βα⟩ =>
    ⟨fun ⟨a, pa⟩ =>
      let ⟨b, hb⟩ := αβ a
      ⟨⟨b, by simpa only [mk_func, ← ZFSet.sound hb]⟩, hb⟩,
      fun ⟨b, pb⟩ =>
      let ⟨a, ha⟩ := βα b
      ⟨⟨a, by simpa only [mk_func, ZFSet.sound ha]⟩, ha⟩⟩
      -- Porting note: the { x | p x } notation appears to be disabled in Lean 4.

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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