mem_powerset — Mathlib

English

An element y is in the powerset of x exactly when y is a subset of x.

Русский

Элемент y принадлежит мощерному множеству x тогда, когда y — подмножество x.

LaTeX

$$$$ y \in \text{powerset}(x) \iff y \subseteq x $$$$

Lean4

@[simp]
theorem mem_powerset : ∀ {x y : PSet}, y ∈ powerset x ↔ y ⊆ x
  | ⟨_, A⟩, ⟨_, B⟩ =>
    ⟨fun ⟨_, e⟩ => (Subset.congr_left e).2 fun ⟨a, _⟩ => ⟨a, Equiv.refl (A a)⟩, fun βα =>
      ⟨{a | ∃ b, Equiv (B b) (A a)}, fun b =>
        let ⟨a, ba⟩ := βα b
        ⟨⟨a, b, ba⟩, ba⟩,
        fun ⟨_, b, ba⟩ => ⟨b, ba⟩⟩⟩

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