ext

Mathlib.Data.Set.Defs

URI: https://scilib.ai/kg/mathlib#Set.ext

English

Two sets are equal if they have exactly the same elements.

Русский

Два множества равны, если у них совпадают все элементы.

LaTeX

$$$\\forall x, (x \\in a \\iff x \\in b) \\Rightarrow a = b$$$

Lean4

theorem ext {a b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b :=
  funext (fun x ↦ propext (h x))

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru