coe_powerset — Mathlib

English

For any ZFSet x, the image of its powerset under the embedding equals the powerset of the embedded x: Class.ofSet(x.powerset) = (Class.ofSet x).powerset.

Русский

Для любого ZF-множества x образ множества подмножеств x под встраиванием в класс равен powerset образа x: Class.ofSet(x.powerset) = (Class.ofSet x).powerset.

LaTeX

$$$ \\mathrm{Class.ofSet}(x \\.\\text{powerset}) = (\\mathrm{Class.ofSet} \\ x) .\\text{powerset}. $$$

Lean4

@[simp, norm_cast]
theorem coe_powerset (x : ZFSet.{u}) : ↑x.powerset = powerset.{u} x :=
  ext fun _ => ZFSet.mem_powerset

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