pair_eq_pair_iff — Mathlib

English

Let x, y, z, w be elements of a type α. The unordered pair {x, y} equals the unordered pair {z, w} if and only if either x = z and y = w, or x = w and y = z.

Русский

Пусть x, y, z и w — элементы множества α. Непорядковая пара {x, y} равна {z, w} тогда и только тогда, когда либо x = z и y = w, либо x = w и y = z.

LaTeX

$$$\\{x, y\\} = \\{z, w\\} \\iff (x = z \\land y = w) \\lor (x = w \\land y = z)$$$

Lean4

theorem pair_eq_pair_iff {x y z w : α} : ({ x, y } : Set α) = { z, w } ↔ x = z ∧ y = w ∨ x = w ∧ y = z := by
  simp [subset_antisymm_iff, insert_subset_iff]; aesop

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