English
Let α be a lattice with a bottom element that is upper-modular and atomistic. Then α is strongly atomic; equivalently, for every a < b in α there exists c with a < c ≤ b and a covers c (a ≺ c).
Русский
Пусть α — решетка с нулем, являющаяся верхнемодульной и атомистической. Тогда α сильно атомарна; эквивалентно тому, что для любых a < b в α существует c such that a < c ≤ b и c покрывает a (a ≺ c).
LaTeX
$$$ (OrderBot\ α) \land (IsUpperModularLattice\ α) \land (IsAtomistic\ α) \Rightarrow IsStronglyAtomic\ α $$$
Lean4
/-- An upper-modular lattice that is atomistic is strongly atomic.
Not an instance to prevent loops. -/
theorem isStronglyAtomic [OrderBot α] [IsUpperModularLattice α] [IsAtomistic α] : IsStronglyAtomic α where
exists_covBy_le_of_lt a b
hab := by
obtain ⟨s, hsb, h⟩ := isLUB_atoms b
refine by_contra fun hcon ↦ hab.not_ge <| (isLUB_le_iff hsb).2 fun x hx ↦ ?_
simp_rw [not_exists, and_comm (b := _ ≤ _), not_and] at hcon
specialize hcon (x ⊔ a) (sup_le (hsb.1 hx) hab.le)
obtain (hbot | h_inf) := (h x hx).bot_covBy.eq_or_eq (c := x ⊓ a) (by simp) (by simp)
· exact False.elim <| hcon <| (hbot ▸ IsUpperModularLattice.covBy_sup_of_inf_covBy) (h x hx).bot_covBy
rwa [inf_eq_left] at h_inf
