English
In a complemented lattice with modularity and compact generation, IsAtomistic holds.
Русский
В комплементированной решётке с модульностью и компактной порождаемостью выполняется атомистичность.
LaTeX
$$$ \text{IsAtomistic}(\alpha) $ given the complemented lattice assumptions$$
Lean4
instance (priority := 100) isAtomic_of_complementedLattice [ComplementedLattice α] : IsAtomic α :=
⟨fun b => by
by_cases h : {c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
· left
rw [← sSup_compact_le_eq b, sSup_eq_bot]
exact h
· rcases Set.not_subset.1 h with ⟨c, ⟨hc, hcb⟩, hcbot⟩
right
have hc' := CompleteLattice.Iic_coatomic_of_compact_element hc
rw [← isAtomic_iff_isCoatomic] at hc'
obtain con | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le (⟨c, le_refl c⟩ : Set.Iic c)
· exfalso
apply hcbot
simp only [Subtype.ext_iff, Set.Iic.coe_bot] at con
exact con
rw [← Subtype.coe_le_coe, Subtype.coe_mk] at hac
exact ⟨a, ha.of_isAtom_coe_Iic, hac.trans hcb⟩⟩
