case mp
ι : Sort ?u.132411
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : ComplementedLattice α
⊢ IsAtomistic α

case mpr
ι : Sort ?u.132411
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : IsAtomistic α
⊢ ComplementedLattice α
ι : Sort ?u.132411
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α ↔ IsAtomistic α
constructor <;> intros
no goals
case mp
ι : Sort ?u.132411
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : ComplementedLattice α
⊢ IsAtomistic α
exact isAtomistic_of_complementedLattice
no goals
case mpr
ι : Sort ?u.132411
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : IsAtomistic α
⊢ ComplementedLattice α
exact complementedLattice_of_isAtomistic