disjoint_singleton_left — Mathlib

English

A singleton {a} is disjoint from a set s if and only if a is not in s.

Русский

Единственный элемент {a} не пересекается с множеством s тогда и только тогда, когда a не принадлежит s.

LaTeX

$$$\\operatorname{Disjoint}(\\{a\\}, s) \\iff a \\notin s$$$

Lean4

@[simp]
theorem disjoint_singleton_left : Disjoint (singleton a) s ↔ a ∉ s := by
  simp only [disjoint_left, mem_singleton, forall_eq]

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