English
If every π(i) is atomic, then the Pi-product ∀ i, π(i) is atomic.
Русский
Если каждый π(i) атомарен, то произведение Pi ∀ i, π(i) является атомарным.
LaTeX
$$$ IsAtomic\left(\forall i,\ π(i)\right) $$$
Lean4
instance isAtomic [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] [∀ i, IsAtomic (π i)] : IsAtomic (∀ i, π i) where
eq_bot_or_exists_atom_le
b :=
or_iff_not_imp_left.2 fun h =>
have ⟨i, hi⟩ : ∃ i, b i ≠ ⊥ := not_forall.1 (h.imp Pi.eq_bot_iff.2)
have ⟨a, ha, hab⟩ := (eq_bot_or_exists_atom_le (b i)).resolve_left hi
by classical exact ⟨Function.update ⊥ i a, isAtom_single ha, update_le_iff.2 ⟨hab, by simp⟩⟩
