isCoatomic_of_isAtomic_of_complementedLattice_of_isModular

English

In a complemented modular lattice that is atomic, the lattice is strongly atomic.

Русский

В дополненной модульной решётке, которая атомна, решетка является сильно атомной.

LaTeX

$$$ \\text{IsAtomic}(\\alpha) \\implies \\text{IsStronglyAtomic}(\\alpha) $$$

Lean4

theorem isCoatomic_of_isAtomic_of_complementedLattice_of_isModular [IsAtomic α] : IsCoatomic α :=
  ⟨fun x => by
    rcases exists_isCompl x with ⟨y, xy⟩
    apply (eq_bot_or_exists_atom_le y).imp _ _
    · rintro rfl
      exact eq_top_of_isCompl_bot xy
    · rintro ⟨a, ha, ay⟩
      rcases exists_isCompl (xy.symm.IicOrderIsoIci ⟨a, ay⟩) with ⟨⟨b, xb⟩, hb⟩
      refine ⟨↑(⟨b, xb⟩ : Set.Ici x), IsCoatom.of_isCoatom_coe_Ici ?_, xb⟩
      rw [← hb.isAtom_iff_isCoatom, OrderIso.isAtom_iff]
      apply ha.Iic⟩

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