Definition df-at 10173

Description: Define the set of atoms in a Hilbert lattice. An atom is a non-zero element of a lattice such that anything less than it is zero, i.e. it is a smallest non-zero element of the lattice. Definition of atom in [Kalmbach] p. 15. See elat 10174 and elat2 10175 for membership relations.

Assertion

Ref	Expression
df-at	⊢ Atoms = {x ∈ Cℋ ∣0ℋ ⋖ x}

Detailed syntax breakdown of Definition df-at

Step	Hyp	Ref	Expression
1		cat 8772	. 2 class Atoms
2		c0h 8743	. . . 4 class 0ℋ
3		vx	. . . . 5 set x
4	3	cv 952	. . . 4 class x
5		ccv 8773	. . . 4 class ⋖
6	2, 4, 5	wbr 2609	. . 3 wff 0ℋ ⋖ x
7		cch 8737	. . 3 class Cℋ
8	6, 3, 7	crab 1640	. 2 class {x ∈ Cℋ ∣0ℋ ⋖ x}
9	1, 8	wceq 953	1 wff Atoms = {x ∈ Cℋ ∣0ℋ ⋖ x}

This definition is referenced by:  elat 10174  atssch 10178

Copyright terms: Public domain