Mathlib Map

Structures · Order

IsAtomistic

A lattice is atomistic iff every element is a sSup of a set of atoms.

Defined in
Mathlib.Order.Atoms
Shape
One type argument · adds isLUB_atoms

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances3

  • OrderDual
  • Submodule
  • Set

How is a type an instance?

Loading the hierarchy index…

Assumed by13

Ancestors0

No ancestors.