Theory "set_utils"

Parents     arith_utils

Theorems

scc_lemma_1_4_3_8_2_1
|- ∀s t. s ≠ ∅ ∧ s ⊆ t ⇒ ¬DISJOINT s t
card_union'
|- FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒ (CARD (s ∪ t) = CARD s + CARD t)
CARD_INJ_IMAGE_2
|- ∀f s.
     FINITE s ⇒
     (∀x y. x ∈ s ∧ y ∈ s ⇒ ((f x = f y) ⇔ (x = y))) ⇒
     (CARD (IMAGE f s) = CARD s)
scc_main_lemma_x
|- ∀s t x. x ∈ s ∧ x ∉ t ⇒ s ≠ t
inter_diff_contains
|- s ∩ (s DIFF t) = s DIFF t
scc_lemma_1_4_2_1_1_1_2_1
|- ∀s t u. s ⊆ t ∧ s ⊆ t DIFF u ⇒ DISJOINT s u
scc_lemma_1_4_2_1_2_1_2_1
|- ∀s S'. s ∉ S' ⇒ ∀s'. s' ∈ S' ⇒ s ≠ s'
scc_lemma_1_4_2_1_3_1_4_3
|- ∀vs vs' v v'. DISJOINT vs vs' ∧ v ∈ vs ∧ v' ∈ vs' ⇒ v ≠ v'
scc_lemma_1_4_3_2_1
|- ∀s t. ¬(s ⊆ t) ⇒ s ≠ t
scc_lemma_1_4_3_8_1
|- ∀S t.
     (∀x y. x ∈ S ∧ y ∈ S ∧ x ≠ y ⇒ DISJOINT x y) ∧
     (∀y. y ∈ S ∧ t ≠ y ⇒ DISJOINT t y) ∧ t ⊆ BIGUNION S ∧ S ≠ ∅ ⇒
     ∃u. u ∈ S ∧ t ⊆ u
scc_lemma_1_4_3_9
|- ∀s t. (s = t) ⇒ s ⊆ t
scc_lemma_1_4_3_10
|- ∀s t u. s ⊆ t ⇒ s ⊆ t ∪ u
scc_lemma_1_4_3_13
|- ∀s S. DISJOINT s (BIGUNION S) ∧ s ≠ ∅ ⇒ s ∉ S
scc_lemma_1_4_4
|- ∀s t. (∀x. x ∉ s ⇒ x ∉ t) ⇒ (t DIFF s = ∅)
scc_lemma_1_4_5
|- ∀x s t. (x INSERT s = t) ⇒ x ∈ t
scc_lemma_1_4_8
|- ∀s t x y. (∀y. y ∉ s ⇒ y ∉ t) ∧ x ∉ t ⇒ y ∉ s DELETE x ⇒ y ∉ t
scc_lemma_1_4_10
|- ∀s t u v x.
     u ⊆ s ∪ t ∧ x ∉ v ∧ t DELETE x ⊆ v ∧ v ⊆ u DIFF s ⇒ (v = t DELETE x)
scc_main_lemma_1_5_1
|- ∀s t u. s ⊆ t ⇒ s DIFF u ⊆ t DIFF u
scc_lemma_1_6_1
|- ∀s t.
     (∀x y. x ∈ s ∧ y ∈ t ∧ x ≠ y ⇒ DISJOINT x y) ⇒
     (BIGUNION (s DIFF t) = BIGUNION s DIFF BIGUNION t)
eq_funs_eq_images
|- (∀x. x ∈ s ⇒ (f1 x = f2 x)) ⇒ (IMAGE f1 s = IMAGE f2 s)
neq_funs_neq_images
|- (∀x. x ∈ s ⇒ ∀y. y ∈ s ⇒ f1 x ≠ f2 y) ∧ (∃x. x ∈ s) ⇒
   IMAGE f1 s ≠ IMAGE f2 s
two_children_parent_bound_main_lemma_2_3
|- ∀s t. DISJOINT (s DIFF t) t
two_children_parent_bound_main_lemma_3_1_2
|- ∀s t. t ⊆ s ⇒ (s DIFF (s DIFF t) = t)
two_children_parent_bound_main_lemma_6
|- ∀vs vs'. DISJOINT vs vs' ⇒ (vs DIFF vs' = vs)
bound_child_parent_lemma_1_1_1_3_1_3
|- ∀a b. a ⊆ b ⇒ (a ∩ b = a)
parent_children_lemma_1_1_1_6_2
|- ∀s t u. DISJOINT s t ⇒ ((u DIFF t) ∩ s = u ∩ s)
parent_children_main_lemma_1_1_1
|- ∀s t. DISJOINT s t ⇒ (s DIFF t = s)
parent_children_main_lemma_1_1_8_2
|- ∀x y z. DISJOINT x y ⇒ (x ∪ y DIFF (x ∪ z) = y DIFF z)
parent_children_main_lemma_1_1_15_2
|- ∀s t. s ⊆ t ⇒ BIGUNION s ⊆ BIGUNION t
invariant_prob_reachable_states_thm_9
|- ∀x s. s ⊆ x INSERT s
invariant_prob_reachable_states_thm_3
|- ∀P f x s.
     (∀x y. P x ∧ P y ∧ x ≠ y ⇒ f x ≠ f y) ∧ P x ∧ x ∉ s ∧ (∀x. x ∈ s ⇒ P x) ⇒
     f x ∉ IMAGE f s
bound_main_lemma_2_1
|- ∀s k. (∀x. x ∈ s ⇒ x ≤ k) ⇒ FINITE s
bound_main_lemma_1_2
|- ∀s k. (∃x. x ∈ s ∧ x ≤ k) ⇒ MIN_SET s ≤ k
bound_child_parent_lemma_2_1_2
|- ∀s k. (∃x. x ∈ s ∧ x < k) ⇒ MIN_SET s < k
bound_child_parent_lemma_2_2_1
|- ∀s k. (∀x. x ∈ s ⇒ x < k) ⇒ FINITE s
bounded_imp_finite
|- ∀s k. (∀x. x ∈ s ⇒ x ≤ k) ⇒ FINITE s
bound_main_lemma_2
|- ∀s k. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x ≤ k) ⇒ MAX_SET s ≤ k
bound_child_parent_lemma_2_2
|- ∀s k. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x < k) ⇒ MAX_SET s < k
MAX_SET_LEQ_MAX_SET
|- s ≠ ∅ ∧ FINITE t ∧ (∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ x ≤ y) ⇒ MAX_SET s ≤ MAX_SET t
FINITE_ALL_DISTINCT_LISTS
|- FINITE P ⇒ FINITE {p | ALL_DISTINCT p ∧ set p ⊆ P}
DISJOINT_UNION_thm
|- ∀s t u. DISJOINT s t ∧ DISJOINT s u ⇒ DISJOINT s (t ∪ u)
CARD_IMAGE
|- ∀f s. FINITE s ⇒ CARD (IMAGE f s) ≤ CARD s
in_not_in_neq
|- x ∈ s ∧ y ∉ s ⇒ x ≠ y
finite_card_bounded
|- FINITE s ⇒ ∃k. CARD s ≤ k
PROD_IMAGE_MONO_LESS_EQ
|- FINITE s ⇒ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ Π f s ≤ Π g s
PROD_IMAGE_MONO_LESS_EQ'
|- FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ Π f s ≤ Π g s
CARD_SING_REST_INSERT
|- FINITE s ⇒ e ∉ s ⇒ SING (REST (e INSERT s)) ⇒ SING s
TWO_SET_CASES
|- ∀a b c d. ({a; b} = {c; d}) ⇒ (a = c) ∧ (b = d) ∨ (a = d) ∧ (b = c)
INSERT_EQ_TWO_SET
|- e ∉ s ∧ a ≠ b ∧ (e INSERT s = {a; b}) ⇒ (s = {a}) ∨ (s = {b})
CARD_TWO_HAS_TWO_MEM
|- FINITE s ⇒ ((CARD s = 2) ⇔ ∃x y. x ≠ y ∧ (s = {x; y}))
CHOICE_OF_TWO
|- ∀a b. (CHOICE {a; b} = a) ∨ (CHOICE {a; b} = b)
CHOICE_OF_THREE
|- ∀a b c.
     (CHOICE {a; b; c} = a) ∨ (CHOICE {a; b; c} = b) ∨ (CHOICE {a; b; c} = c)
CHOICE_AND_REST_OF_TWO
|- ∀a b. a ≠ b ⇒ ((CHOICE {a; b} = a) ⇔ (REST {a; b} = {b}))
CHOICE_AND_REST_OF_THREE
|- ∀a b c.
     a ≠ b ∧ a ≠ c ∧ b ≠ c ⇒
     ((CHOICE {a; b; c} = a) ⇔ (REST {a; b; c} = {b; c}))
SET_TWO_COMM
|- {a; b} = {b; a}
SET_THREE_COMM
|- ({a; b; c} = {b; a; c}) ∧ ({a; b; c} = {b; c; a}) ∧ ({a; b; c} = {a; c; b})
CARD_NZERO_EMPTY
|- FINITE s ⇒ s ≠ ∅ ⇒ CARD s > 0
INSERT_DELETE
|- (e INSERT s) DELETE e = s DELETE e
INSERT_DELETE_2
|- e ≠ e' ⇒ ((e' INSERT s) DELETE e = e' INSERT s DELETE e)
DELETE_DELETE_2
|- e' ∉ s ⇒ (s DELETE e DELETE e' = s DELETE e)
PROD_DELET_LEQ_PROD
|- ∀f s e. FINITE s ⇒ (∀x. x ∈ s ⇒ f x > 0) ⇒ Π f (s DELETE e) ≤ Π f s
PRED_IMG_PRED_COMPOSE
|- (∀x. x ∈ s ⇒ P ((f ∘ g) x)) ⇔ ∀y. y ∈ IMAGE g s ⇒ P (f y)
PROD_IMAGE_COMPOSE
|- FINITE s ⇒ (∀x. x ∈ s ⇒ (f ∘ g) x > 0) ⇒ Π f (IMAGE g s) ≤ Π (f ∘ g) s
PROD_IMAGE_COMPOSE'
|- FINITE s ∧ (∀x. x ∈ s ⇒ (f ∘ g) x > 0) ⇒ Π f (IMAGE g s) ≤ Π (f ∘ g) s
CARD_SUBSET'
|- ∀s. FINITE s ∧ t ⊆ s ⇒ CARD t ≤ CARD s
subset_inter_diff_empty
|- s ⊆ t ⇒ (s ∩ (u DIFF t) = ∅)
UNION_SUBSET_UNION
|- s ⊆ u ⇒ s ∪ t ⊆ u ∪ t
IMAGE_INTER_EQ
|- INJ f 𝕌(:α) 𝕌(:β) ⇒ (IMAGE f (s ∩ t) = IMAGE f s ∩ IMAGE f t)