English
An element f of the Pi-product is an atom iff there exists an index i and an atom a in π(i) such that f is obtained from the bottom by placing a at i and ⊥ elsewhere.
Русский
Элемент f в произведении Pi является атомом тогда и только тогда, когда существует индекс i и атом a в π(i), такой что f получено из нижнего элемента ⊥ размещением a в координате i и ⊥ во всех остальных координатах.
LaTeX
$$$ IsAtom f \;\iff\; \exists i\ a,\ IsAtom a \land f = \operatorname{Function.update} \bot i a. $$$
Lean4
theorem isAtom_iff_eq_single [DecidableEq ι] [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] {f : ∀ i, π i} :
IsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a := by simp [← bot_covBy_iff, covBy_iff_exists_right_eq]
