English
If α is coAtomic, then α is strongly atomic (dual viewpoint).
Русский
Если α коатомная, то она сильно атомна (с точки зрения двойственности).
LaTeX
$$$ \\text{IsCoatomic}(\\alpha) \\Rightarrow \\text{IsStronglyAtomic}(\\alpha) $$$
Lean4
/-- A complemented modular atomic lattice is strongly atomic.
Not an instance to prevent loops. -/
theorem isStronglyAtomic [IsAtomic α] : IsStronglyAtomic α where
exists_covBy_le_of_lt a b
hab := by
obtain ⟨⟨a', ha'b : a' ≤ b⟩, ha'⟩ := exists_isCompl (α := Set.Iic b) ⟨a, hab.le⟩
obtain (rfl | ⟨d, hd⟩) := eq_bot_or_exists_atom_le a'
· obtain rfl : a = b := by simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint
exact False.elim <| hab.ne rfl
refine ⟨d ⊔ a, IsUpperModularLattice.covBy_sup_of_inf_covBy ?_, sup_le (hd.2.trans ha'b) hab.le⟩
convert hd.1.bot_covBy
rw [← le_bot_iff, ← show a ⊓ a' = ⊥ by simpa using Subtype.coe_inj.2 ha'.inf_eq_bot, inf_comm]
exact inf_le_inf_left _ hd.2
