Theory "partitioning"

Parents     indexedLists   patternMatches

Signature

Constant Type
choice_fun :((α -> bool) -> α) -> ((α -> bool) -> bool) -> bool
partitioning :((α -> bool) -> bool) -> (α -> bool) -> bool
quotient :((α -> bool) -> bool) -> α -> α -> bool
transversal :((α -> bool) -> α) -> ((α -> bool) -> bool) -> bool

Definitions

partitioning_def
|- ∀sos X.
     partitioning sos X ⇔
     (BIGUNION sos = X) ∧ ∀s t. s ∈ sos ∧ t ∈ sos ⇒ (s = t) ∨ DISJOINT s t
choice_fun_def
|- ∀f sos. choice_fun f sos ⇔ ∀s. s ∈ sos ⇒ f s ∈ s
transversal_def
|- ∀tvsal sos.
     transversal tvsal sos ⇔
     INJ tvsal sos (BIGUNION sos) ∧ choice_fun tvsal sos
quotient_def
|- ∀sos x. quotient sos x = CHOICE {s | x ∈ s ∧ s ∈ sos}


Theorems

partitioning_quoteint_sing
|- ∀P X x. partitioning P X ∧ x ∈ X ⇒ SING {p' | x ∈ p' ∧ p' ∈ P}