theorem 3.60 Equivalence classes partition the set

open in the book · parts/02-mathematical-methods/01-logic-sets.tex:1551 · p. 35

Rests on

depends_on definition 3.59 Equivalence class ¶
- depends_on definition 3.58 Equivalence relation ¶
depends_on definition 3.58 Equivalence relation ¶ ↺
depends_on definition 3.36 Disjoint sets ¶
depends_on equation 3.47 eq:set-double-inclusion ¶
proves proof ch:01-logic-sets@proof-11 ¶

Supports

depends_on lemma A.10 lem:app-comp-welldefined ¶
- depends_on lemma A.11 Truth lemma ¶
  - depends_on theorem A.12 Model existence ¶
    - depends_on corollary A.14 Compactness ¶
    - depends_on theorem A.13 Completeness ¶

Neighborhood

Every logical edge within two steps of this node.

declared and complete
partly declared
a check failed
not graded
declared in the source
inferred from structure

Edges

type	direction	node	provenance	where
`depends_on`	→	Equivalence class	declared	parts/02-mathematical-methods/01-logic-sets.tex:1563
`depends_on`	→	Equivalence relation	declared	parts/02-mathematical-methods/01-logic-sets.tex:1563
`depends_on`	→	Disjoint sets	declared	parts/02-mathematical-methods/01-logic-sets.tex:1563
`depends_on`	→	eq:set-double-inclusion	declared	parts/02-mathematical-methods/01-logic-sets.tex:1563
`depends_on`	←	lem:app-comp-welldefined	declared	appendices/A-long-proofs.tex:1739
`proves`	←	ch:01-logic-sets@proof-11	declared	parts/02-mathematical-methods/01-logic-sets.tex:1566