equiv_iff_mem — Mathlib

English

Equiv x y holds iff every w is in x exactly when it is in y.

Русский

x эквивалентно y тогда и только тогда, когда для каждого w верно: w ∈ x ↔ w ∈ y.

LaTeX

$$$\\\\forall {x y : PSet.{u}},\\\\ Equiv x y \\\\iff \\\\forall {w : PSet.{u}}, w\\\\in x \\\\leftrightarrow w\\\\in y$$$

Lean4

theorem equiv_iff_mem {x y : PSet.{u}} : Equiv x y ↔ ∀ {w : PSet.{u}}, w ∈ x ↔ w ∈ y :=
  ⟨Mem.congr_right,
    match x, y with
    | ⟨_, A⟩, ⟨_, B⟩ => fun h =>
      ⟨fun a => h.1 (Mem.mk A a), fun b =>
        let ⟨a, h⟩ := h.2 (Mem.mk B b)
        ⟨a, h.symm⟩⟩⟩

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