ext — Mathlib

English

If every element satisfies a membership equivalence, x ≃ y.

Русский

Если для всех элементов выполняется эквивалентность принадлежности, то x ≃ y.

LaTeX

$$$\\forall {x y : PSet}, (\\forall w : PSet, x.mem w \\leftrightarrow y.mem w) \\rightarrow x \\Equiv y$$$

Lean4

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

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