Constant | Type |
---|---|
choice_fun | :((α -> bool) -> α) -> ((α -> bool) -> bool) -> bool |
partitioning | :((α -> bool) -> bool) -> (α -> bool) -> bool |
quotient | :((α -> bool) -> bool) -> α -> α -> bool |
transversal | :((α -> bool) -> α) -> ((α -> bool) -> bool) -> bool |
|- ∀sos X. partitioning sos X ⇔ (BIGUNION sos = X) ∧ ∀s t. s ∈ sos ∧ t ∈ sos ⇒ (s = t) ∨ DISJOINT s t
|- ∀f sos. choice_fun f sos ⇔ ∀s. s ∈ sos ⇒ f s ∈ s
|- ∀tvsal sos. transversal tvsal sos ⇔ INJ tvsal sos (BIGUNION sos) ∧ choice_fun tvsal sos
|- ∀sos x. quotient sos x = CHOICE {s | x ∈ s ∧ s ∈ sos}
|- ∀P X x. partitioning P X ∧ x ∈ X ⇒ SING {p' | x ∈ p' ∧ p' ∈ P}