English
Let i be a fixed index. If a is an atom in π(i), then the element of the product ∀ i, π(i) which is ⊥ in every coordinate except at i where it is a is an atom of the product.
Русский
Пусть i фиксирован, и пусть a является атомом в π(i). Тогда элемент произведения ∀ i, π(i), равный ⊥ во всех координатах, кроме i, где стоит a, является атомом произведения.
LaTeX
$$$ IsAtom a \rightarrow IsAtom (\operatorname{update} (⊥ : \forall i, π i) i a) $$$
Lean4
theorem isAtom_single {i : ι} [DecidableEq ι] [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] {a : π i} (h : IsAtom a) :
IsAtom (Function.update (⊥ : ∀ i, π i) i a) :=
isAtom_iff.2 ⟨i, by simpa, fun _ hji => Function.update_of_ne hji ..⟩
