powerset

Mathlib.SetTheory.ZFC.Basic

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

Lean4

/-- The powerset operation, the collection of subsets of a ZFC set -/
def powerset : ZFSet → ZFSet :=
  Quotient.map PSet.powerset fun ⟨_, A⟩ ⟨_, B⟩ ⟨αβ, βα⟩ =>
    ⟨fun p =>
      ⟨{b | ∃ a, p a ∧ Equiv (A a) (B b)}, fun ⟨a, pa⟩ =>
        let ⟨b, ab⟩ := αβ a
        ⟨⟨b, a, pa, ab⟩, ab⟩,
        fun ⟨_, a, pa, ab⟩ => ⟨⟨a, pa⟩, ab⟩⟩,
      fun q =>
      ⟨{a | ∃ b, q b ∧ Equiv (A a) (B b)}, fun ⟨_, b, qb, ab⟩ => ⟨⟨b, qb⟩, ab⟩, fun ⟨b, qb⟩ =>
        let ⟨a, ab⟩ := βα b
        ⟨⟨a, b, qb, ab⟩, ab⟩⟩⟩

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

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

Разделы

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

Аффилиация

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