isAtomic — Mathlib

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⟩

Похожие утверждения