English
In a Pi-type product, IsAtom f holds iff there exists an index i such that f_i is an atom and all other coordinates are bottom.
Русский
В произведении типа Pi IsAtom(f) эквивалентно существованию индекса i, для которого f_i является атомом, а все прочие координаты равны ⊥.
LaTeX
$$$ \\text{IsAtom}(f) \\iff \\exists i, \\text{IsAtom}(f(i)) \\land \\forall j \\neq i,\\ f(j) = \\bot $$$
Lean4
theorem isAtom_iff {f : ∀ i, π i} [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] :
IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ j, j ≠ i → f j = ⊥ := by
simp only [← bot_covBy_iff, Pi.covBy_iff, bot_apply, eq_comm]
