eq — Mathlib · SciLib

English

Let x and y be pre-sets. Then x and y are equivalent if and only if they have exactly the same members.

Русский

Пусть x и y — предмножества. Тогда x эквивалентно y тогда и только тогда, когда у них совпадают элементы.

LaTeX

$$$$ Equiv(x,y) \iff toSet(x) = toSet(y) $$$$

Lean4

/-- Two pre-sets are equivalent iff they have the same members. -/
theorem eq {x y : PSet} : Equiv x y ↔ toSet x = toSet y :=
  equiv_iff_mem.trans Set.ext_iff.symm

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