English
Let A be a SetLike object with bottom. For K ∈ A, IsAtom(K) holds if and only if K ≠ ⊥ and for all H,g with H ≤ K and g ∈ K \ H, we have H = ⊥.
Русский
Пусть A — множество с нулём; для K ∈ A справедливо: IsAtom(K) тогда и только тогда, когда K ≠ ⊥ и для всех H,g с H ≤ K и g ∈ K \ H имеет место H = ⊥.
LaTeX
$$$ \\mathrm{IsAtom}(K) \\iff \\big(K \\neq \\bot \\land \\forall H\\, g,\\ H \\le K \\to g \\notin H \\to g \\in K \\to H = \\bot\\big).$$$
Lean4
theorem isAtom_iff [OrderBot A] {K : A} : IsAtom K ↔ K ≠ ⊥ ∧ ∀ H g, H ≤ K → g ∉ H → g ∈ K → H = ⊥ := by
simp_rw [IsAtom, lt_iff_le_not_ge, SetLike.not_le_iff_exists, and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp,
and_comm]
