English
If α has bottom and is strongly atomic, then α is atomic.
Русский
Если у α есть ноль и α сильно атомарно, то α атомарно.
LaTeX
$$$ [OrderBot α] [IsStronglyAtomic α] \Rightarrow IsAtomic α $$$
Lean4
instance isAtomic (α : Type*) [PartialOrder α] [OrderBot α] [IsStronglyAtomic α] : IsAtomic α where
eq_bot_or_exists_atom_le
a := by
rw [or_iff_not_imp_left, ← Ne, ← bot_lt_iff_ne_bot]
refine fun hlt ↦ ?_
obtain ⟨x, hx, hxa⟩ := hlt.exists_covby_le
exact ⟨x, bot_covBy_iff.1 hx, hxa⟩