Theory "res_quan"

Theorems

IN_BIGINTER_RES_FORALL

⊢ ∀x sos. x ∈ BIGINTER sos ⇔ ∀s::sos. x ∈ s

IN_BIGUNION_RES_EXISTS

⊢ ∀x sos. x ∈ BIGUNION sos ⇔ ∃s::sos. x ∈ s

NOT_RES_EXISTS

⊢ ∀P s. ¬(∃x::s. P x) ⇔ ∀x::s. ¬P x

NOT_RES_FORALL

⊢ ∀P s. ¬(∀x::s. P x) ⇔ ∃x::s. ¬P x

RES_ABSTRACT

⊢ ∀p m x. x ∈ p ⇒ (RES_ABSTRACT p m x = m x)

RES_ABSTRACT_EQUAL

⊢ ∀p m1 m2.
    (∀x. x ∈ p ⇒ (m1 x = m2 x)) ⇒ (RES_ABSTRACT p m1 = RES_ABSTRACT p m2)

RES_ABSTRACT_EQUAL_EQ

⊢ ∀p m1 m2.
    (RES_ABSTRACT p m1 = RES_ABSTRACT p m2) ⇔ ∀x. x ∈ p ⇒ (m1 x = m2 x)

RES_ABSTRACT_IDEMPOT

⊢ ∀p m. RES_ABSTRACT p (RES_ABSTRACT p m) = RES_ABSTRACT p m

RES_ABSTRACT_UNIV

⊢ ∀m. RES_ABSTRACT 𝕌(:α) m = m

RES_DISJ_EXISTS_DIST

⊢ ∀P Q R. (∃i::(λi. P i ∨ Q i). R i) ⇔ (∃i::P. R i) ∨ ∃i::Q. R i

RES_EXISTS

⊢ ∀P f. RES_EXISTS P f ⇔ ∃x. x ∈ P ∧ f x

RES_EXISTS_ALT

⊢ ∀p m. RES_EXISTS p m ⇔ RES_SELECT p m ∈ p ∧ m (RES_SELECT p m)

RES_EXISTS_BIGINTER

⊢ ∀P sos. (∃x::BIGINTER sos. P x) ⇔ ∃x. (∀s::sos. x ∈ s) ∧ P x

RES_EXISTS_BIGUNION

⊢ ∀P sos. (∃x::BIGUNION sos. P x) ⇔ ∃(s::sos) (x::s). P x

RES_EXISTS_DIFF

⊢ ∀P s t x. (∃x::s DIFF t. P x) ⇔ ∃x::s. x ∉ t ∧ P x

RES_EXISTS_DISJ_DIST

⊢ ∀P Q R. (∃i::P. Q i ∨ R i) ⇔ (∃i::P. Q i) ∨ ∃i::P. R i

RES_EXISTS_EMPTY

⊢ ∀p. ¬RES_EXISTS ∅ p

RES_EXISTS_EQUAL

⊢ ∀P j. (∃i:: $= j. P i) ⇔ P j

RES_EXISTS_F

⊢ ∀P s x. ¬∃s::x. F

RES_EXISTS_NOT_EMPTY

⊢ ∀P s. RES_EXISTS s P ⇒ s ≠ ∅

RES_EXISTS_NULL

⊢ ∀p m. (∃x::p. m) ⇔ p ≠ ∅ ∧ m

RES_EXISTS_REORDER

⊢ ∀P Q R. (∃(i::P) (j::Q). R i j) ⇔ ∃(j::Q) (i::P). R i j

RES_EXISTS_SUBSET

⊢ ∀P s t. s ⊆ t ⇒ RES_EXISTS s P ⇒ RES_EXISTS t P

RES_EXISTS_T

⊢ ∀P s x. (∃x::s. T) ⇔ s ≠ ∅

RES_EXISTS_UNION

⊢ ∀P s t. RES_EXISTS (s ∪ t) P ⇔ RES_EXISTS s P ∨ RES_EXISTS t P

RES_EXISTS_UNIQUE

⊢ ∀P f. RES_EXISTS_UNIQUE P f ⇔ (∃x::P. f x) ∧ ∀x y::P. f x ∧ f y ⇒ (x = y)

RES_EXISTS_UNIQUE_ALT

⊢ ∀p m. RES_EXISTS_UNIQUE p m ⇔ ∃x::p. m x ∧ ∀y::p. m y ⇒ (y = x)

RES_EXISTS_UNIQUE_ELIM

⊢ ∀P s. (∃!x::s. P x) ⇔ ∃!x. x ∈ s ∧ P x

RES_EXISTS_UNIQUE_EMPTY

⊢ ∀p. ¬RES_EXISTS_UNIQUE ∅ p

RES_EXISTS_UNIQUE_EXISTS

⊢ ∀P s. RES_EXISTS_UNIQUE P s ⇒ RES_EXISTS P s

RES_EXISTS_UNIQUE_F

⊢ ∀P s x. ¬∃!x::s. F

RES_EXISTS_UNIQUE_NOT_EMPTY

⊢ ∀P s. RES_EXISTS_UNIQUE s P ⇒ s ≠ ∅

RES_EXISTS_UNIQUE_NULL

⊢ ∀p m. (∃!x::p. m) ⇔ (∃x. p = {x}) ∧ m

RES_EXISTS_UNIQUE_SING

⊢ ∀P s x. (∃!x::s. T) ⇔ ∃y. s = {y}

RES_EXISTS_UNIQUE_T

⊢ ∀P s x. (∃!x::s. T) ⇔ ∃!x. x ∈ s

RES_EXISTS_UNIQUE_UNIV

⊢ ∀p. RES_EXISTS_UNIQUE 𝕌(:α) p ⇔ $?! p

RES_EXISTS_UNIV

⊢ ∀p. RES_EXISTS 𝕌(:α) p ⇔ $? p

RES_FORALL

⊢ ∀P f. RES_FORALL P f ⇔ ∀x. x ∈ P ⇒ f x

RES_FORALL_BIGINTER

⊢ ∀P sos. (∀x::BIGINTER sos. P x) ⇔ ∀x. (∀s::sos. x ∈ s) ⇒ P x

RES_FORALL_BIGUNION

⊢ ∀P sos. (∀x::BIGUNION sos. P x) ⇔ ∀(s::sos) (x::s). P x

RES_FORALL_CONJ_DIST

⊢ ∀P Q R. (∀i::P. Q i ∧ R i) ⇔ (∀i::P. Q i) ∧ ∀i::P. R i

RES_FORALL_DIFF

⊢ ∀P s t x. (∀x::s DIFF t. P x) ⇔ ∀x::s. x ∉ t ⇒ P x

RES_FORALL_DISJ_DIST

⊢ ∀P Q R. (∀i::(λj. P j ∨ Q j). R i) ⇔ (∀i::P. R i) ∧ ∀i::Q. R i

RES_FORALL_EMPTY

⊢ ∀p. RES_FORALL ∅ p

RES_FORALL_F

⊢ ∀P s x. (∀x::s. F) ⇔ (s = ∅)

RES_FORALL_FORALL

⊢ ∀P R x. (∀x (i::P). R i x) ⇔ ∀(i::P) x. R i x

RES_FORALL_NOT_EMPTY

⊢ ∀P s. ¬RES_FORALL s P ⇒ s ≠ ∅

RES_FORALL_NULL

⊢ ∀p m. (∀x::p. m) ⇔ (p = ∅) ∨ m

RES_FORALL_REORDER

⊢ ∀P Q R. (∀(i::P) (j::Q). R i j) ⇔ ∀(j::Q) (i::P). R i j

RES_FORALL_SUBSET

⊢ ∀P s t. s ⊆ t ⇒ RES_FORALL t P ⇒ RES_FORALL s P

RES_FORALL_T

⊢ ∀P s x (x::s). T

RES_FORALL_UNION

⊢ ∀P s t. RES_FORALL (s ∪ t) P ⇔ RES_FORALL s P ∧ RES_FORALL t P

RES_FORALL_UNIQUE

⊢ ∀P j. (∀i:: $= j. P i) ⇔ P j

RES_FORALL_UNIV

⊢ ∀p. RES_FORALL 𝕌(:α) p ⇔ $! p

RES_SELECT

⊢ ∀P f. RES_SELECT P f = @x. x ∈ P ∧ f x

RES_SELECT_EMPTY

⊢ ∀p. RES_SELECT ∅ p = @x. F

RES_SELECT_UNIV

⊢ ∀p. RES_SELECT 𝕌(:α) p = $@ p