isAtom_iff — Mathlib

English

An object s in the multiset order is an atom if and only if s is a singleton {a} for some a.

Русский

Элемент s в порядке мультсетов является атомом тогда и только тогда, когда s является синглтоном {a} для некоторого a.

LaTeX

$$$\text{IsAtom}(s) \iff \exists a,\, s = \{a\}$$$

Lean4

theorem isAtom_iff : IsAtom s ↔ ∃ a, s = { a } := by simp [← bot_covBy_iff, covBy_iff, eq_comm]

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