disjoint_singleton — Mathlib

English

Two singletons are disjoint exactly when their elements are different: Disjoint {a} {b} iff a ≠ b.

Русский

Два одиночных множества не пересекаются тогда и только тогда, когда элементы различны: {a} и {b} не пересекаются ⇔ a ≠ b.

LaTeX

$$$\\operatorname{Disjoint}(\\{a\\}, \\{b\\}) \\iff a \\neq b$$$

Lean4

theorem disjoint_singleton : Disjoint ({ a } : Finset α) { b } ↔ a ≠ b := by rw [disjoint_singleton_left, mem_singleton]

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