ext_iff — Mathlib

English

Let p and q be two SetLike elements. Then p and q are equal if and only if they have the same membership for every element x.

Русский

Пусть p и q — два элемента SetLike. Тогда p = q тогда же, когда для каждого x выполняется x ∈ p ⇔ x ∈ q.

LaTeX

$$$ p = q \\iff \\forall x, x \\in p \\iff x \\in q $$$

Lean4

theorem ext_iff : p = q ↔ ∀ x, x ∈ p ↔ x ∈ q :=
  coe_injective.eq_iff.symm.trans Set.ext_iff

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