Structure topologyTheory
signature topologyTheory =
sig
type thm = Thm.thm
(* Definitions *)
val ARBITRARY : thm
val INTERSECTION_OF : thm
val UNION_OF : thm
val closed_DEF : thm
val closed_in : thm
val hull : thm
val istopology : thm
val limpt : thm
val neigh : thm
val open_DEF : thm
val pairwise : thm
val relative_to : thm
val subtopology : thm
val topology_TY_DEF : thm
val topology_tybij : thm
val topspace : thm
(* Theorems *)
val ARBITRARY_INTERSECTION_OF_COMPLEMENT : thm
val ARBITRARY_INTERSECTION_OF_EMPTY : thm
val ARBITRARY_INTERSECTION_OF_IDEMPOT : thm
val ARBITRARY_INTERSECTION_OF_INC : thm
val ARBITRARY_INTERSECTION_OF_INTER : thm
val ARBITRARY_INTERSECTION_OF_INTERS : thm
val ARBITRARY_INTERSECTION_OF_RELATIVE_TO : thm
val ARBITRARY_INTERSECTION_OF_UNION : thm
val ARBITRARY_INTERSECTION_OF_UNION_EQ : thm
val ARBITRARY_UNION_OF_ALT : thm
val ARBITRARY_UNION_OF_COMPLEMENT : thm
val ARBITRARY_UNION_OF_EMPTY : thm
val ARBITRARY_UNION_OF_IDEMPOT : thm
val ARBITRARY_UNION_OF_INC : thm
val ARBITRARY_UNION_OF_INTER : thm
val ARBITRARY_UNION_OF_INTER_EQ : thm
val ARBITRARY_UNION_OF_NONEMPTY_FINITE_INTERSECTION : thm
val ARBITRARY_UNION_OF_RELATIVE_TO : thm
val ARBITRARY_UNION_OF_UNION : thm
val ARBITRARY_UNION_OF_UNIONS : thm
val BIGUNION_2 : thm
val CLOSED_IN_BIGINTER : thm
val CLOSED_IN_BIGUNION : thm
val CLOSED_IN_DIFF : thm
val CLOSED_IN_EMPTY : thm
val CLOSED_IN_IMP_SUBSET : thm
val CLOSED_IN_INTER : thm
val CLOSED_IN_OPEN_IN_COMPL : thm
val CLOSED_IN_RELATIVE_TO : thm
val CLOSED_IN_SUBSET : thm
val CLOSED_IN_SUBTOPOLOGY : thm
val CLOSED_IN_SUBTOPOLOGY_EMPTY : thm
val CLOSED_IN_SUBTOPOLOGY_REFL : thm
val CLOSED_IN_SUBTOPOLOGY_UNION : thm
val CLOSED_IN_TOPSPACE : thm
val CLOSED_IN_UNION : thm
val CLOSED_LIMPT : thm
val COMPL_COMPL_applied : thm
val COUNTABLE_DISJOINT_UNION_OF_IDEMPOT : thm
val COUNTABLE_INTERSECTION_OF_COMPLEMENT : thm
val COUNTABLE_INTERSECTION_OF_EMPTY : thm
val COUNTABLE_INTERSECTION_OF_IDEMPOT : thm
val COUNTABLE_INTERSECTION_OF_INC : thm
val COUNTABLE_INTERSECTION_OF_INTER : thm
val COUNTABLE_INTERSECTION_OF_INTERS : thm
val COUNTABLE_INTERSECTION_OF_RELATIVE_TO : thm
val COUNTABLE_INTERSECTION_OF_RELATIVE_TO_ALT : thm
val COUNTABLE_INTERSECTION_OF_UNION : thm
val COUNTABLE_INTERSECTION_OF_UNIONS : thm
val COUNTABLE_INTERSECTION_OF_UNIONS_NONEMPTY : thm
val COUNTABLE_INTERSECTION_OF_UNION_EQ : thm
val COUNTABLE_SUBSET_NUM : thm
val COUNTABLE_UNION_OF_ASCENDING : thm
val COUNTABLE_UNION_OF_COMPLEMENT : thm
val COUNTABLE_UNION_OF_EMPTY : thm
val COUNTABLE_UNION_OF_EXPLICIT : thm
val COUNTABLE_UNION_OF_IDEMPOT : thm
val COUNTABLE_UNION_OF_INC : thm
val COUNTABLE_UNION_OF_INTER : thm
val COUNTABLE_UNION_OF_INTERS : thm
val COUNTABLE_UNION_OF_INTERS_NONEMPTY : thm
val COUNTABLE_UNION_OF_INTER_EQ : thm
val COUNTABLE_UNION_OF_RELATIVE_TO : thm
val COUNTABLE_UNION_OF_UNION : thm
val COUNTABLE_UNION_OF_UNIONS : thm
val DIFF_INTERS : thm
val DIFF_UNIONS : thm
val DIFF_UNIONS_NONEMPTY : thm
val EMPTY_GSPEC : thm
val EXT_SKOLEM_THM : thm
val EXT_SKOLEM_THM' : thm
val FINITE_IMAGE : thm
val FINITE_INDUCT_STRONG : thm
val FINITE_INTERSECTION_OF_COMPLEMENT : thm
val FINITE_INTERSECTION_OF_EMPTY : thm
val FINITE_INTERSECTION_OF_IDEMPOT : thm
val FINITE_INTERSECTION_OF_INC : thm
val FINITE_INTERSECTION_OF_INTER : thm
val FINITE_INTERSECTION_OF_INTERS : thm
val FINITE_INTERSECTION_OF_RELATIVE_TO : thm
val FINITE_INTERSECTION_OF_RELATIVE_TO_ALT : thm
val FINITE_INTERSECTION_OF_UNION : thm
val FINITE_INTERSECTION_OF_UNION_EQ : thm
val FINITE_SUBSET : thm
val FINITE_UNION_OF_COMPLEMENT : thm
val FINITE_UNION_OF_EMPTY : thm
val FINITE_UNION_OF_IDEMPOT : thm
val FINITE_UNION_OF_INC : thm
val FINITE_UNION_OF_INTER : thm
val FINITE_UNION_OF_INTER_EQ : thm
val FINITE_UNION_OF_RELATIVE_TO : thm
val FINITE_UNION_OF_UNION : thm
val FINITE_UNION_OF_UNIONS : thm
val FORALL_INTERSECTION_OF : thm
val FORALL_RELATIVE_TO : thm
val FORALL_UNION_OF : thm
val HULLS_EQ : thm
val HULL_ANTIMONO : thm
val HULL_EQ : thm
val HULL_HULL : thm
val HULL_IMAGE : thm
val HULL_IMAGE_GALOIS : thm
val HULL_IMAGE_SUBSET : thm
val HULL_INC : thm
val HULL_INDUCT : thm
val HULL_MINIMAL : thm
val HULL_MONO : thm
val HULL_P : thm
val HULL_P_AND_Q : thm
val HULL_REDUNDANT : thm
val HULL_REDUNDANT_EQ : thm
val HULL_SUBSET : thm
val HULL_UNION : thm
val HULL_UNION_LEFT : thm
val HULL_UNION_RIGHT : thm
val HULL_UNION_SUBSET : thm
val HULL_UNIQUE : thm
val IMP_CONJ : thm
val IMP_IMP : thm
val INTERSECTION_OF_EMPTY : thm
val INTERSECTION_OF_INC : thm
val INTERSECTION_OF_MONO : thm
val INTERS_0 : thm
val INTERS_1 : thm
val INTERS_2 : thm
val INTERS_GSPEC : thm
val INTERS_IMAGE : thm
val INTERS_INSERT : thm
val INTERS_SUBSET : thm
val INTERS_SUBSET_STRONG : thm
val INTERS_UNIONS : thm
val INTER_INTERS : thm
val INTER_UNIONS : thm
val IN_GSPEC : thm
val IN_INTERS : thm
val IN_UNIONS : thm
val ISTOPOLOGY_OPEN_IN : thm
val ISTOPOLOGY_SUBTOPOLOGY : thm
val IS_HULL : thm
val LE_0 : thm
val OPEN_IN_BIGINTER : thm
val OPEN_IN_BIGUNION : thm
val OPEN_IN_CLAUSES : thm
val OPEN_IN_CLOSED_IN : thm
val OPEN_IN_CLOSED_IN_EQ : thm
val OPEN_IN_DIFF : thm
val OPEN_IN_EMPTY : thm
val OPEN_IN_IMP_SUBSET : thm
val OPEN_IN_INTER : thm
val OPEN_IN_RELATIVE_TO : thm
val OPEN_IN_SUBOPEN : thm
val OPEN_IN_SUBSET : thm
val OPEN_IN_SUBTOPOLOGY : thm
val OPEN_IN_SUBTOPOLOGY_EMPTY : thm
val OPEN_IN_SUBTOPOLOGY_REFL : thm
val OPEN_IN_SUBTOPOLOGY_UNION : thm
val OPEN_IN_TOPSPACE : thm
val OPEN_IN_UNION : thm
val OPEN_NEIGH : thm
val OPEN_OWN_NEIGH : thm
val OPEN_SUBOPEN : thm
val OPEN_UNOPEN : thm
val PAIRWISE_AND : thm
val PAIRWISE_EMPTY : thm
val PAIRWISE_IMAGE : thm
val PAIRWISE_IMP : thm
val PAIRWISE_INSERT : thm
val PAIRWISE_MONO : thm
val PAIRWISE_SING : thm
val PAIRWISE_UNION : thm
val P_HULL : thm
val RELATIVE_TO : thm
val RELATIVE_TO_COMPL : thm
val RELATIVE_TO_IMP_SUBSET : thm
val RELATIVE_TO_INC : thm
val RELATIVE_TO_INTER : thm
val RELATIVE_TO_MONO : thm
val RELATIVE_TO_RELATIVE_TO : thm
val RELATIVE_TO_SUBSET : thm
val RELATIVE_TO_SUBSET_INC : thm
val RELATIVE_TO_SUBSET_TRANS : thm
val RELATIVE_TO_UNION : thm
val RELATIVE_TO_UNIV : thm
val SIMPLE_IMAGE : thm
val SING_GSPEC : thm
val SUBSET_HULL : thm
val SUBSET_RESTRICT : thm
val SUBTOPOLOGY_SUBTOPOLOGY : thm
val SUBTOPOLOGY_SUPERSET : thm
val SUBTOPOLOGY_TOPSPACE : thm
val SUBTOPOLOGY_UNIV : thm
val TOPOLOGY_EQ : thm
val TOPSPACE_SUBTOPOLOGY : thm
val UNIONS_0 : thm
val UNIONS_1 : thm
val UNIONS_2 : thm
val UNIONS_GSPEC : thm
val UNIONS_IMAGE : thm
val UNIONS_INSERT : thm
val UNIONS_INTERS : thm
val UNIONS_SUBSET : thm
val UNIONS_UNION : thm
val UNION_OF_EMPTY : thm
val UNION_OF_INC : thm
val UNION_OF_MONO : thm
val UNIV_GSPEC : thm
val closed_topspace : thm
val limpt_thm : thm
val open_topspace : thm
val pairwiseD_alt_pairwiseN : thm
val topology_grammars : type_grammar.grammar * term_grammar.grammar
(*
[cardinal] Parent theory of "topology"
[ARBITRARY] Definition
⊢ ∀s. ARBITRARY s ⇔ T
[INTERSECTION_OF] Definition
⊢ ∀P Q.
P INTERSECTION_OF Q =
(λs. ∃u. P u ∧ (∀c. c ∈ u ⇒ Q c) ∧ BIGINTER u = s)
[UNION_OF] Definition
⊢ ∀P Q.
P UNION_OF Q = (λs. ∃u. P u ∧ (∀c. c ∈ u ⇒ Q c) ∧ BIGUNION u = s)
[closed_DEF] Definition
⊢ ∀s. closed s ⇔ closed_in s 𝕌(:α)
[closed_in] Definition
⊢ ∀top s.
closed_in top s ⇔
s ⊆ topspace top ∧ open_in top (topspace top DIFF s)
[hull] Definition
⊢ ∀P s. P hull s = BIGINTER {t | P t ∧ s ⊆ t}
[istopology] Definition
⊢ ∀L. istopology L ⇔
∅ ∈ L ∧ (∀s t. s ∈ L ∧ t ∈ L ⇒ s ∩ t ∈ L) ∧
∀k. k ⊆ L ⇒ BIGUNION k ∈ L
[limpt] Definition
⊢ ∀top x S'.
limpt top x S' ⇔
x ∈ topspace top ∧ ∀N. neigh top (N,x) ⇒ ∃y. x ≠ y ∧ S' y ∧ N y
[neigh] Definition
⊢ ∀top N x.
neigh top (N,x) ⇔
∃P. open_in top P ∧ P ⊆ N ∧ P x ∧ N ⊆ topspace top
[open_DEF] Definition
⊢ ∀s. open s ⇔ open_in s 𝕌(:α)
[pairwise] Definition
⊢ ∀r s. pairwiseD r s ⇔ ∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ⇒ r x y
[relative_to] Definition
⊢ ∀P s t. (P relative_to s) t ⇔ ∃u. P u ∧ s ∩ u = t
[subtopology] Definition
⊢ ∀top u. subtopology top u = topology {s ∩ u | open_in top s}
[topology_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION istopology rep
[topology_tybij] Definition
⊢ (∀a. topology (open_in a) = a) ∧
∀r. istopology r ⇔ open_in (topology r) = r
[topspace] Definition
⊢ ∀top. topspace top = BIGUNION {s | open_in top s}
[ARBITRARY_INTERSECTION_OF_COMPLEMENT] Theorem
⊢ ∀P s.
(ARBITRARY INTERSECTION_OF P) s ⇔
(ARBITRARY UNION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)
[ARBITRARY_INTERSECTION_OF_EMPTY] Theorem
⊢ ∀P. (ARBITRARY INTERSECTION_OF P) 𝕌(:α)
[ARBITRARY_INTERSECTION_OF_IDEMPOT] Theorem
⊢ ∀P. ARBITRARY INTERSECTION_OF ARBITRARY INTERSECTION_OF P =
ARBITRARY INTERSECTION_OF P
[ARBITRARY_INTERSECTION_OF_INC] Theorem
⊢ ∀P s. P s ⇒ (ARBITRARY INTERSECTION_OF P) s
[ARBITRARY_INTERSECTION_OF_INTER] Theorem
⊢ ∀P s t.
(ARBITRARY INTERSECTION_OF P) s ∧ (ARBITRARY INTERSECTION_OF P) t ⇒
(ARBITRARY INTERSECTION_OF P) (s ∩ t)
[ARBITRARY_INTERSECTION_OF_INTERS] Theorem
⊢ ∀P u.
(∀s. s ∈ u ⇒ (ARBITRARY INTERSECTION_OF P) s) ⇒
(ARBITRARY INTERSECTION_OF P) (BIGINTER u)
[ARBITRARY_INTERSECTION_OF_RELATIVE_TO] Theorem
⊢ ∀P u.
ARBITRARY INTERSECTION_OF P relative_to u =
ARBITRARY INTERSECTION_OF (P relative_to u) relative_to u
[ARBITRARY_INTERSECTION_OF_UNION] Theorem
⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∪ t)) ⇒
∀s t.
(ARBITRARY INTERSECTION_OF P) s ∧
(ARBITRARY INTERSECTION_OF P) t ⇒
(ARBITRARY INTERSECTION_OF P) (s ∪ t)
[ARBITRARY_INTERSECTION_OF_UNION_EQ] Theorem
⊢ ∀P. (∀s t.
(ARBITRARY INTERSECTION_OF P) s ∧
(ARBITRARY INTERSECTION_OF P) t ⇒
(ARBITRARY INTERSECTION_OF P) (s ∪ t)) ⇔
∀s t. P s ∧ P t ⇒ (ARBITRARY INTERSECTION_OF P) (s ∪ t)
[ARBITRARY_UNION_OF_ALT] Theorem
⊢ ∀B s.
(ARBITRARY UNION_OF B) s ⇔ ∀x. x ∈ s ⇒ ∃u. u ∈ B ∧ x ∈ u ∧ u ⊆ s
[ARBITRARY_UNION_OF_COMPLEMENT] Theorem
⊢ ∀P s.
(ARBITRARY UNION_OF P) s ⇔
(ARBITRARY INTERSECTION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)
[ARBITRARY_UNION_OF_EMPTY] Theorem
⊢ ∀P. (ARBITRARY UNION_OF P) ∅
[ARBITRARY_UNION_OF_IDEMPOT] Theorem
⊢ ∀P. ARBITRARY UNION_OF ARBITRARY UNION_OF P = ARBITRARY UNION_OF P
[ARBITRARY_UNION_OF_INC] Theorem
⊢ ∀P s. P s ⇒ (ARBITRARY UNION_OF P) s
[ARBITRARY_UNION_OF_INTER] Theorem
⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∩ t)) ⇒
∀s t.
(ARBITRARY UNION_OF P) s ∧ (ARBITRARY UNION_OF P) t ⇒
(ARBITRARY UNION_OF P) (s ∩ t)
[ARBITRARY_UNION_OF_INTER_EQ] Theorem
⊢ ∀P. (∀s t.
(ARBITRARY UNION_OF P) s ∧ (ARBITRARY UNION_OF P) t ⇒
(ARBITRARY UNION_OF P) (s ∩ t)) ⇔
∀s t. P s ∧ P t ⇒ (ARBITRARY UNION_OF P) (s ∩ t)
[ARBITRARY_UNION_OF_NONEMPTY_FINITE_INTERSECTION] Theorem
⊢ ∀u. ARBITRARY UNION_OF (λs. FINITE s ∧ s ≠ ∅) INTERSECTION_OF u =
ARBITRARY UNION_OF
(FINITE INTERSECTION_OF u relative_to BIGUNION u)
[ARBITRARY_UNION_OF_RELATIVE_TO] Theorem
⊢ ∀P u.
ARBITRARY UNION_OF P relative_to u =
ARBITRARY UNION_OF (P relative_to u)
[ARBITRARY_UNION_OF_UNION] Theorem
⊢ ∀P s t.
(ARBITRARY UNION_OF P) s ∧ (ARBITRARY UNION_OF P) t ⇒
(ARBITRARY UNION_OF P) (s ∪ t)
[ARBITRARY_UNION_OF_UNIONS] Theorem
⊢ ∀P u.
(∀s. s ∈ u ⇒ (ARBITRARY UNION_OF P) s) ⇒
(ARBITRARY UNION_OF P) (BIGUNION u)
[BIGUNION_2] Theorem
⊢ ∀s t. BIGUNION {s; t} = s ∪ t
[CLOSED_IN_BIGINTER] Theorem
⊢ ∀top k.
k ≠ ∅ ∧ (∀s. s ∈ k ⇒ closed_in top s) ⇒
closed_in top (BIGINTER k)
[CLOSED_IN_BIGUNION] Theorem
⊢ ∀top s.
FINITE s ∧ (∀t. t ∈ s ⇒ closed_in top t) ⇒
closed_in top (BIGUNION s)
[CLOSED_IN_DIFF] Theorem
⊢ ∀top s t.
closed_in top s ∧ open_in top t ⇒ closed_in top (s DIFF t)
[CLOSED_IN_EMPTY] Theorem
⊢ ∀top. closed_in top ∅
[CLOSED_IN_IMP_SUBSET] Theorem
⊢ ∀top s t. closed_in (subtopology top s) t ⇒ t ⊆ s
[CLOSED_IN_INTER] Theorem
⊢ ∀top s t. closed_in top s ∧ closed_in top t ⇒ closed_in top (s ∩ t)
[CLOSED_IN_OPEN_IN_COMPL] Theorem
⊢ ∀top. closed top ⇒ ∀s. closed_in top s ⇔ open_in top (COMPL s)
[CLOSED_IN_RELATIVE_TO] Theorem
⊢ ∀top s. closed_in top relative_to s = closed_in (subtopology top s)
[CLOSED_IN_SUBSET] Theorem
⊢ ∀top s. closed_in top s ⇒ s ⊆ topspace top
[CLOSED_IN_SUBTOPOLOGY] Theorem
⊢ ∀top u s.
closed_in (subtopology top u) s ⇔ ∃t. closed_in top t ∧ s = t ∩ u
[CLOSED_IN_SUBTOPOLOGY_EMPTY] Theorem
⊢ ∀top s. closed_in (subtopology top ∅) s ⇔ s = ∅
[CLOSED_IN_SUBTOPOLOGY_REFL] Theorem
⊢ ∀top u. closed_in (subtopology top u) u ⇔ u ⊆ topspace top
[CLOSED_IN_SUBTOPOLOGY_UNION] Theorem
⊢ ∀top s t u.
closed_in (subtopology top t) s ∧ closed_in (subtopology top u) s ⇒
closed_in (subtopology top (t ∪ u)) s
[CLOSED_IN_TOPSPACE] Theorem
⊢ ∀top. closed_in top (topspace top)
[CLOSED_IN_UNION] Theorem
⊢ ∀top s t. closed_in top s ∧ closed_in top t ⇒ closed_in top (s ∪ t)
[CLOSED_LIMPT] Theorem
⊢ ∀top.
closed top ⇒ ∀S'. closed_in top S' ⇔ ∀x. limpt top x S' ⇒ S' x
[COMPL_COMPL_applied] Theorem
⊢ ∀s. 𝕌(:α) DIFF (𝕌(:α) DIFF s) = s
[COUNTABLE_DISJOINT_UNION_OF_IDEMPOT] Theorem
⊢ ∀P. (countable ∩ pairwiseD DISJOINT) UNION_OF
(countable ∩ pairwiseD DISJOINT) UNION_OF P =
(countable ∩ pairwiseD DISJOINT) UNION_OF P
[COUNTABLE_INTERSECTION_OF_COMPLEMENT] Theorem
⊢ ∀P s.
(countable INTERSECTION_OF P) s ⇔
(countable UNION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)
[COUNTABLE_INTERSECTION_OF_EMPTY] Theorem
⊢ ∀P. (countable INTERSECTION_OF P) 𝕌(:α)
[COUNTABLE_INTERSECTION_OF_IDEMPOT] Theorem
⊢ ∀P. countable INTERSECTION_OF countable INTERSECTION_OF P =
countable INTERSECTION_OF P
[COUNTABLE_INTERSECTION_OF_INC] Theorem
⊢ ∀P s. P s ⇒ (countable INTERSECTION_OF P) s
[COUNTABLE_INTERSECTION_OF_INTER] Theorem
⊢ ∀P s t.
(countable INTERSECTION_OF P) s ∧ (countable INTERSECTION_OF P) t ⇒
(countable INTERSECTION_OF P) (s ∩ t)
[COUNTABLE_INTERSECTION_OF_INTERS] Theorem
⊢ ∀P u.
countable u ∧ (∀s. s ∈ u ⇒ (countable INTERSECTION_OF P) s) ⇒
(countable INTERSECTION_OF P) (BIGINTER u)
[COUNTABLE_INTERSECTION_OF_RELATIVE_TO] Theorem
⊢ ∀P u.
countable INTERSECTION_OF P relative_to u =
countable INTERSECTION_OF (P relative_to u) relative_to u
[COUNTABLE_INTERSECTION_OF_RELATIVE_TO_ALT] Theorem
⊢ ∀P u s.
P u ⇒
((countable INTERSECTION_OF P relative_to u) s ⇔
(countable INTERSECTION_OF P) s ∧ s ⊆ u)
[COUNTABLE_INTERSECTION_OF_UNION] Theorem
⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∪ t)) ⇒
∀s t.
(countable INTERSECTION_OF P) s ∧
(countable INTERSECTION_OF P) t ⇒
(countable INTERSECTION_OF P) (s ∪ t)
[COUNTABLE_INTERSECTION_OF_UNIONS] Theorem
⊢ ∀P u.
(countable INTERSECTION_OF P) ∅ ∧ (∀s t. P s ∧ P t ⇒ P (s ∪ t)) ∧
FINITE u ∧ (∀s. s ∈ u ⇒ (countable INTERSECTION_OF P) s) ⇒
(countable INTERSECTION_OF P) (BIGUNION u)
[COUNTABLE_INTERSECTION_OF_UNIONS_NONEMPTY] Theorem
⊢ ∀P u.
(∀s t. P s ∧ P t ⇒ P (s ∪ t)) ∧ FINITE u ∧ u ≠ ∅ ∧
(∀s. s ∈ u ⇒ (countable INTERSECTION_OF P) s) ⇒
(countable INTERSECTION_OF P) (BIGUNION u)
[COUNTABLE_INTERSECTION_OF_UNION_EQ] Theorem
⊢ ∀P. (∀s t.
(countable INTERSECTION_OF P) s ∧
(countable INTERSECTION_OF P) t ⇒
(countable INTERSECTION_OF P) (s ∪ t)) ⇔
∀s t. P s ∧ P t ⇒ (countable INTERSECTION_OF P) (s ∪ t)
[COUNTABLE_SUBSET_NUM] Theorem
⊢ ∀s. countable s
[COUNTABLE_UNION_OF_ASCENDING] Theorem
⊢ ∀P s.
P ∅ ∧ (∀t u. P t ∧ P u ⇒ P (t ∪ u)) ⇒
((countable UNION_OF P) s ⇔
∃t. (∀n. P (t n)) ∧ (∀n. t n ⊆ t (SUC n)) ∧
BIGUNION {t n | n ∈ 𝕌(:num)} = s)
[COUNTABLE_UNION_OF_COMPLEMENT] Theorem
⊢ ∀P s.
(countable UNION_OF P) s ⇔
(countable INTERSECTION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)
[COUNTABLE_UNION_OF_EMPTY] Theorem
⊢ ∀P. (countable UNION_OF P) ∅
[COUNTABLE_UNION_OF_EXPLICIT] Theorem
⊢ ∀P s.
P ∅ ⇒
((countable UNION_OF P) s ⇔
∃t. (∀n. P (t n)) ∧ BIGUNION {t n | n ∈ 𝕌(:num)} = s)
[COUNTABLE_UNION_OF_IDEMPOT] Theorem
⊢ ∀P. countable UNION_OF countable UNION_OF P = countable UNION_OF P
[COUNTABLE_UNION_OF_INC] Theorem
⊢ ∀P s. P s ⇒ (countable UNION_OF P) s
[COUNTABLE_UNION_OF_INTER] Theorem
⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∩ t)) ⇒
∀s t.
(countable UNION_OF P) s ∧ (countable UNION_OF P) t ⇒
(countable UNION_OF P) (s ∩ t)
[COUNTABLE_UNION_OF_INTERS] Theorem
⊢ ∀P u.
(countable UNION_OF P) 𝕌(:α) ∧ (∀s t. P s ∧ P t ⇒ P (s ∩ t)) ∧
FINITE u ∧ (∀s. s ∈ u ⇒ (countable UNION_OF P) s) ⇒
(countable UNION_OF P) (BIGINTER u)
[COUNTABLE_UNION_OF_INTERS_NONEMPTY] Theorem
⊢ ∀P u.
(∀s t. P s ∧ P t ⇒ P (s ∩ t)) ∧ FINITE u ∧ u ≠ ∅ ∧
(∀s. s ∈ u ⇒ (countable UNION_OF P) s) ⇒
(countable UNION_OF P) (BIGINTER u)
[COUNTABLE_UNION_OF_INTER_EQ] Theorem
⊢ ∀P. (∀s t.
(countable UNION_OF P) s ∧ (countable UNION_OF P) t ⇒
(countable UNION_OF P) (s ∩ t)) ⇔
∀s t. P s ∧ P t ⇒ (countable UNION_OF P) (s ∩ t)
[COUNTABLE_UNION_OF_RELATIVE_TO] Theorem
⊢ ∀P u.
countable UNION_OF P relative_to u =
countable UNION_OF (P relative_to u)
[COUNTABLE_UNION_OF_UNION] Theorem
⊢ ∀P s t.
(countable UNION_OF P) s ∧ (countable UNION_OF P) t ⇒
(countable UNION_OF P) (s ∪ t)
[COUNTABLE_UNION_OF_UNIONS] Theorem
⊢ ∀P u.
countable u ∧ (∀s. s ∈ u ⇒ (countable UNION_OF P) s) ⇒
(countable UNION_OF P) (BIGUNION u)
[DIFF_INTERS] Theorem
⊢ ∀u s. u DIFF BIGINTER s = BIGUNION {u DIFF t | t ∈ s}
[DIFF_UNIONS] Theorem
⊢ ∀u s. u DIFF BIGUNION s = u ∩ BIGINTER {u DIFF t | t ∈ s}
[DIFF_UNIONS_NONEMPTY] Theorem
⊢ ∀u s. s ≠ ∅ ⇒ u DIFF BIGUNION s = BIGINTER {u DIFF t | t ∈ s}
[EMPTY_GSPEC] Theorem
⊢ {x | F} = ∅
[EXT_SKOLEM_THM] Theorem
⊢ ∀P Q. (∀x. x ∈ P ⇒ ∃y. Q x y) ⇔ ∃f. ∀x. x ∈ P ⇒ Q x (f x)
[EXT_SKOLEM_THM'] Theorem
⊢ ∀P Q. (∀x. P x ⇒ ∃y. Q x y) ⇔ ∃f. ∀x. P x ⇒ Q x (f x)
[FINITE_IMAGE] Theorem
⊢ ∀s. FINITE s ⇒ ∀f. FINITE (IMAGE f s)
[FINITE_INDUCT_STRONG] Theorem
⊢ ∀P. P ∅ ∧ (∀x s. P s ∧ x ∉ s ∧ FINITE s ⇒ P (x INSERT s)) ⇒
∀s. FINITE s ⇒ P s
[FINITE_INTERSECTION_OF_COMPLEMENT] Theorem
⊢ ∀P s.
(FINITE INTERSECTION_OF P) s ⇔
(FINITE UNION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)
[FINITE_INTERSECTION_OF_EMPTY] Theorem
⊢ ∀P. (FINITE INTERSECTION_OF P) 𝕌(:α)
[FINITE_INTERSECTION_OF_IDEMPOT] Theorem
⊢ ∀P. FINITE INTERSECTION_OF FINITE INTERSECTION_OF P =
FINITE INTERSECTION_OF P
[FINITE_INTERSECTION_OF_INC] Theorem
⊢ ∀P s. P s ⇒ (FINITE INTERSECTION_OF P) s
[FINITE_INTERSECTION_OF_INTER] Theorem
⊢ ∀P s t.
(FINITE INTERSECTION_OF P) s ∧ (FINITE INTERSECTION_OF P) t ⇒
(FINITE INTERSECTION_OF P) (s ∩ t)
[FINITE_INTERSECTION_OF_INTERS] Theorem
⊢ ∀P u.
FINITE u ∧ (∀s. s ∈ u ⇒ (FINITE INTERSECTION_OF P) s) ⇒
(FINITE INTERSECTION_OF P) (BIGINTER u)
[FINITE_INTERSECTION_OF_RELATIVE_TO] Theorem
⊢ ∀P u.
FINITE INTERSECTION_OF P relative_to u =
FINITE INTERSECTION_OF (P relative_to u) relative_to u
[FINITE_INTERSECTION_OF_RELATIVE_TO_ALT] Theorem
⊢ ∀P u s.
P u ⇒
((FINITE INTERSECTION_OF P relative_to u) s ⇔
(FINITE INTERSECTION_OF P) s ∧ s ⊆ u)
[FINITE_INTERSECTION_OF_UNION] Theorem
⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∪ t)) ⇒
∀s t.
(FINITE INTERSECTION_OF P) s ∧ (FINITE INTERSECTION_OF P) t ⇒
(FINITE INTERSECTION_OF P) (s ∪ t)
[FINITE_INTERSECTION_OF_UNION_EQ] Theorem
⊢ ∀P. (∀s t.
(FINITE INTERSECTION_OF P) s ∧ (FINITE INTERSECTION_OF P) t ⇒
(FINITE INTERSECTION_OF P) (s ∪ t)) ⇔
∀s t. P s ∧ P t ⇒ (FINITE INTERSECTION_OF P) (s ∪ t)
[FINITE_SUBSET] Theorem
⊢ ∀s t. FINITE s ∧ t ⊆ s ⇒ FINITE t
[FINITE_UNION_OF_COMPLEMENT] Theorem
⊢ ∀P s.
(FINITE UNION_OF P) s ⇔
(FINITE INTERSECTION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)
[FINITE_UNION_OF_EMPTY] Theorem
⊢ ∀P. (FINITE UNION_OF P) ∅
[FINITE_UNION_OF_IDEMPOT] Theorem
⊢ ∀P. FINITE UNION_OF FINITE UNION_OF P = FINITE UNION_OF P
[FINITE_UNION_OF_INC] Theorem
⊢ ∀P s. P s ⇒ (FINITE UNION_OF P) s
[FINITE_UNION_OF_INTER] Theorem
⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∩ t)) ⇒
∀s t.
(FINITE UNION_OF P) s ∧ (FINITE UNION_OF P) t ⇒
(FINITE UNION_OF P) (s ∩ t)
[FINITE_UNION_OF_INTER_EQ] Theorem
⊢ ∀P. (∀s t.
(FINITE UNION_OF P) s ∧ (FINITE UNION_OF P) t ⇒
(FINITE UNION_OF P) (s ∩ t)) ⇔
∀s t. P s ∧ P t ⇒ (FINITE UNION_OF P) (s ∩ t)
[FINITE_UNION_OF_RELATIVE_TO] Theorem
⊢ ∀P u.
FINITE UNION_OF P relative_to u =
FINITE UNION_OF (P relative_to u)
[FINITE_UNION_OF_UNION] Theorem
⊢ ∀P s t.
(FINITE UNION_OF P) s ∧ (FINITE UNION_OF P) t ⇒
(FINITE UNION_OF P) (s ∪ t)
[FINITE_UNION_OF_UNIONS] Theorem
⊢ ∀P u.
FINITE u ∧ (∀s. s ∈ u ⇒ (FINITE UNION_OF P) s) ⇒
(FINITE UNION_OF P) (BIGUNION u)
[FORALL_INTERSECTION_OF] Theorem
⊢ (∀s. (P INTERSECTION_OF Q) s ⇒ R s) ⇔
∀t. P t ∧ (∀c. c ∈ t ⇒ Q c) ⇒ R (BIGINTER t)
[FORALL_RELATIVE_TO] Theorem
⊢ (∀s. (P relative_to u) s ⇒ Q s) ⇔ ∀s. P s ⇒ Q (u ∩ s)
[FORALL_UNION_OF] Theorem
⊢ (∀s. (P UNION_OF Q) s ⇒ R s) ⇔
∀t. P t ∧ (∀c. c ∈ t ⇒ Q c) ⇒ R (BIGUNION t)
[HULLS_EQ] Theorem
⊢ ∀P s t.
(∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ∧ s ⊆ P hull t ∧
t ⊆ P hull s ⇒
P hull s = P hull t
[HULL_ANTIMONO] Theorem
⊢ ∀P Q s. P ⊆ Q ⇒ Q hull s ⊆ P hull s
[HULL_EQ] Theorem
⊢ ∀P s.
(∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ⇒ (P hull s = s ⇔ P s)
[HULL_HULL] Theorem
⊢ ∀P s. P hull (P hull s) = P hull s
[HULL_IMAGE] Theorem
⊢ ∀P f s.
(∀s. P (P hull s)) ∧ (∀s. P (IMAGE f s) ⇔ P s) ∧
(∀x y. f x = f y ⇒ x = y) ∧ (∀y. ∃x. f x = y) ⇒
P hull IMAGE f s = IMAGE f (P hull s)
[HULL_IMAGE_GALOIS] Theorem
⊢ ∀P f g s.
(∀s. P (P hull s)) ∧ (∀s. P s ⇒ P (IMAGE f s)) ∧
(∀s. P s ⇒ P (IMAGE g s)) ∧ (∀s t. s ⊆ IMAGE g t ⇔ IMAGE f s ⊆ t) ⇒
P hull IMAGE f s = IMAGE f (P hull s)
[HULL_IMAGE_SUBSET] Theorem
⊢ ∀P f s.
P (P hull s) ∧ (∀s. P s ⇒ P (IMAGE f s)) ⇒
P hull IMAGE f s ⊆ IMAGE f (P hull s)
[HULL_INC] Theorem
⊢ ∀P s x. x ∈ s ⇒ x ∈ P hull s
[HULL_INDUCT] Theorem
⊢ ∀P p s. (∀x. x ∈ s ⇒ p x) ∧ P {x | p x} ⇒ ∀x. x ∈ P hull s ⇒ p x
[HULL_MINIMAL] Theorem
⊢ ∀P s t. s ⊆ t ∧ P t ⇒ P hull s ⊆ t
[HULL_MONO] Theorem
⊢ ∀P s t. s ⊆ t ⇒ P hull s ⊆ P hull t
[HULL_P] Theorem
⊢ ∀P s. P s ⇒ P hull s = s
[HULL_P_AND_Q] Theorem
⊢ ∀P Q.
(∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ∧
(∀f. (∀s. s ∈ f ⇒ Q s) ⇒ Q (BIGINTER f)) ∧
(∀s. Q s ⇒ Q (P hull s)) ⇒
(λx. P x ∧ Q x) hull s = P hull (Q hull s)
[HULL_REDUNDANT] Theorem
⊢ ∀P a s. a ∈ P hull s ⇒ P hull (a INSERT s) = P hull s
[HULL_REDUNDANT_EQ] Theorem
⊢ ∀P a s. a ∈ P hull s ⇔ P hull (a INSERT s) = P hull s
[HULL_SUBSET] Theorem
⊢ ∀P s. s ⊆ P hull s
[HULL_UNION] Theorem
⊢ ∀P s t. P hull s ∪ t = P hull (P hull s) ∪ (P hull t)
[HULL_UNION_LEFT] Theorem
⊢ ∀P s t. P hull s ∪ t = P hull (P hull s) ∪ t
[HULL_UNION_RIGHT] Theorem
⊢ ∀P s t. P hull s ∪ t = P hull s ∪ (P hull t)
[HULL_UNION_SUBSET] Theorem
⊢ ∀P s t. (P hull s) ∪ (P hull t) ⊆ P hull s ∪ t
[HULL_UNIQUE] Theorem
⊢ ∀P s t. s ⊆ t ∧ P t ∧ (∀t'. s ⊆ t' ∧ P t' ⇒ t ⊆ t') ⇒ P hull s = t
[IMP_CONJ] Theorem
⊢ ∀p q r. p ∧ q ⇒ r ⇔ p ⇒ q ⇒ r
[IMP_IMP] Theorem
⊢ ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3
[INTERSECTION_OF_EMPTY] Theorem
⊢ ∀P Q. P ∅ ⇒ (P INTERSECTION_OF Q) 𝕌(:α)
[INTERSECTION_OF_INC] Theorem
⊢ ∀P Q s. P {s} ∧ Q s ⇒ (P INTERSECTION_OF Q) s
[INTERSECTION_OF_MONO] Theorem
⊢ ∀P Q Q' s.
(P INTERSECTION_OF Q) s ∧ (∀x. Q x ⇒ Q' x) ⇒
(P INTERSECTION_OF Q') s
[INTERS_0] Theorem
⊢ BIGINTER ∅ = 𝕌(:α)
[INTERS_1] Theorem
⊢ ∀P. BIGINTER {P} = P
[INTERS_2] Theorem
⊢ ∀P Q. BIGINTER {P; Q} = P ∩ Q
[INTERS_GSPEC] Theorem
⊢ (∀P f. BIGINTER {f x | P x} = {a | ∀x. P x ⇒ a ∈ f x}) ∧
(∀P f. BIGINTER {f x y | P x y} = {a | ∀x y. P x y ⇒ a ∈ f x y}) ∧
∀P f.
BIGINTER {f x y z | P x y z} =
{a | ∀x y z. P x y z ⇒ a ∈ f x y z}
[INTERS_IMAGE] Theorem
⊢ ∀f s. BIGINTER (IMAGE f s) = {y | ∀x. x ∈ s ⇒ y ∈ f x}
[INTERS_INSERT] Theorem
⊢ ∀P B. BIGINTER (P INSERT B) = P ∩ BIGINTER B
[INTERS_SUBSET] Theorem
⊢ ∀u s. u ≠ ∅ ∧ (∀t. t ∈ u ⇒ t ⊆ s) ⇒ BIGINTER u ⊆ s
[INTERS_SUBSET_STRONG] Theorem
⊢ ∀u s. (∃t. t ∈ u ∧ t ⊆ s) ⇒ BIGINTER u ⊆ s
[INTERS_UNIONS] Theorem
⊢ ∀s. BIGINTER s = 𝕌(:α) DIFF BIGUNION {𝕌(:α) DIFF t | t ∈ s}
[INTER_INTERS] Theorem
⊢ (∀f s.
s ∩ BIGINTER f = if f = ∅ then s else BIGINTER {s ∩ t | t ∈ f}) ∧
∀f s.
BIGINTER f ∩ s = if f = ∅ then s else BIGINTER {t ∩ s | t ∈ f}
[INTER_UNIONS] Theorem
⊢ (∀s t. BIGUNION s ∩ t = BIGUNION {x ∩ t | x ∈ s}) ∧
∀s t. t ∩ BIGUNION s = BIGUNION {t ∩ x | x ∈ s}
[IN_GSPEC] Theorem
⊢ ∀s. {x | x ∈ s} = s
[IN_INTERS] Theorem
⊢ x ∈ BIGINTER B ⇔ ∀P. P ∈ B ⇒ x ∈ P
[IN_UNIONS] Theorem
⊢ ∀x sos. x ∈ BIGUNION sos ⇔ ∃s. x ∈ s ∧ s ∈ sos
[ISTOPOLOGY_OPEN_IN] Theorem
⊢ ∀top. istopology (open_in top)
[ISTOPOLOGY_SUBTOPOLOGY] Theorem
⊢ ∀top u. istopology {s ∩ u | open_in top s}
[IS_HULL] Theorem
⊢ ∀P s.
(∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ⇒
(P s ⇔ ∃t. s = P hull t)
[LE_0] Theorem
⊢ ∀n. 0 ≤ n
[OPEN_IN_BIGINTER] Theorem
⊢ ∀top s.
FINITE s ∧ s ≠ ∅ ∧ (∀t. t ∈ s ⇒ open_in top t) ⇒
open_in top (BIGINTER s)
[OPEN_IN_BIGUNION] Theorem
⊢ ∀top k. (∀s. s ∈ k ⇒ open_in top s) ⇒ open_in top (BIGUNION k)
[OPEN_IN_CLAUSES] Theorem
⊢ ∀top.
open_in top ∅ ∧
(∀s t. open_in top s ∧ open_in top t ⇒ open_in top (s ∩ t)) ∧
∀k. (∀s. s ∈ k ⇒ open_in top s) ⇒ open_in top (BIGUNION k)
[OPEN_IN_CLOSED_IN] Theorem
⊢ ∀top s.
s ⊆ topspace top ⇒
(open_in top s ⇔ closed_in top (topspace top DIFF s))
[OPEN_IN_CLOSED_IN_EQ] Theorem
⊢ ∀top s.
open_in top s ⇔
s ⊆ topspace top ∧ closed_in top (topspace top DIFF s)
[OPEN_IN_DIFF] Theorem
⊢ ∀top s t. open_in top s ∧ closed_in top t ⇒ open_in top (s DIFF t)
[OPEN_IN_EMPTY] Theorem
⊢ ∀top. open_in top ∅
[OPEN_IN_IMP_SUBSET] Theorem
⊢ ∀top s t. open_in (subtopology top s) t ⇒ t ⊆ s
[OPEN_IN_INTER] Theorem
⊢ ∀top s t. open_in top s ∧ open_in top t ⇒ open_in top (s ∩ t)
[OPEN_IN_RELATIVE_TO] Theorem
⊢ ∀top s. open_in top relative_to s = open_in (subtopology top s)
[OPEN_IN_SUBOPEN] Theorem
⊢ ∀top s.
open_in top s ⇔ ∀x. x ∈ s ⇒ ∃t. open_in top t ∧ x ∈ t ∧ t ⊆ s
[OPEN_IN_SUBSET] Theorem
⊢ ∀top s. open_in top s ⇒ s ⊆ topspace top
[OPEN_IN_SUBTOPOLOGY] Theorem
⊢ ∀top u s.
open_in (subtopology top u) s ⇔ ∃t. open_in top t ∧ s = t ∩ u
[OPEN_IN_SUBTOPOLOGY_EMPTY] Theorem
⊢ ∀top s. open_in (subtopology top ∅) s ⇔ s = ∅
[OPEN_IN_SUBTOPOLOGY_REFL] Theorem
⊢ ∀top u. open_in (subtopology top u) u ⇔ u ⊆ topspace top
[OPEN_IN_SUBTOPOLOGY_UNION] Theorem
⊢ ∀top s t u.
open_in (subtopology top t) s ∧ open_in (subtopology top u) s ⇒
open_in (subtopology top (t ∪ u)) s
[OPEN_IN_TOPSPACE] Theorem
⊢ ∀top. open_in top (topspace top)
[OPEN_IN_UNION] Theorem
⊢ ∀top s t. open_in top s ∧ open_in top t ⇒ open_in top (s ∪ t)
[OPEN_NEIGH] Theorem
⊢ ∀A top. open_in top A ⇔ ∀x. A x ⇒ ∃N. neigh top (N,x) ∧ N ⊆ A
[OPEN_OWN_NEIGH] Theorem
⊢ ∀A top x. open_in top A ∧ A x ⇒ neigh top (A,x)
[OPEN_SUBOPEN] Theorem
⊢ ∀S' top.
open_in top S' ⇔ ∀x. S' x ⇒ ∃P. P x ∧ open_in top P ∧ P ⊆ S'
[OPEN_UNOPEN] Theorem
⊢ ∀S' top.
open_in top S' ⇔ BIGUNION {P | open_in top P ∧ P ⊆ S'} = S'
[PAIRWISE_AND] Theorem
⊢ ∀R R' s.
pairwiseD R s ∧ pairwiseD R' s ⇔
pairwiseD (λx y. R x y ∧ R' x y) s
[PAIRWISE_EMPTY] Theorem
⊢ ∀r. pairwiseD r ∅ ⇔ T
[PAIRWISE_IMAGE] Theorem
⊢ ∀r f.
pairwiseD r (IMAGE f s) ⇔
pairwiseD (λx y. f x ≠ f y ⇒ r (f x) (f y)) s
[PAIRWISE_IMP] Theorem
⊢ ∀P Q s.
pairwiseD P s ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ P x y ∧ x ≠ y ⇒ Q x y) ⇒
pairwiseD Q s
[PAIRWISE_INSERT] Theorem
⊢ ∀r x s.
pairwiseD r (x INSERT s) ⇔
(∀y. y ∈ s ∧ y ≠ x ⇒ r x y ∧ r y x) ∧ pairwiseD r s
[PAIRWISE_MONO] Theorem
⊢ ∀r s t. pairwiseD r s ∧ t ⊆ s ⇒ pairwiseD r t
[PAIRWISE_SING] Theorem
⊢ ∀r x. pairwiseD r {x} ⇔ T
[PAIRWISE_UNION] Theorem
⊢ ∀R s t.
pairwiseD R (s ∪ t) ⇔
pairwiseD R s ∧ pairwiseD R t ∧
∀x y. x ∈ s DIFF t ∧ y ∈ t DIFF s ⇒ R x y ∧ R y x
[P_HULL] Theorem
⊢ ∀P s. (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ⇒ P (P hull s)
[RELATIVE_TO] Theorem
⊢ P relative_to u = {u ∩ s | P s}
[RELATIVE_TO_COMPL] Theorem
⊢ ∀P u s.
s ⊆ u ⇒
((P relative_to u) (u DIFF s) ⇔
((λc. P (𝕌(:α) DIFF c)) relative_to u) s)
[RELATIVE_TO_IMP_SUBSET] Theorem
⊢ ∀P s t. (P relative_to s) t ⇒ t ⊆ s
[RELATIVE_TO_INC] Theorem
⊢ ∀P u s. P s ⇒ (P relative_to u) (u ∩ s)
[RELATIVE_TO_INTER] Theorem
⊢ ∀P s.
(∀c d. P c ∧ P d ⇒ P (c ∩ d)) ⇒
∀c d.
(P relative_to s) c ∧ (P relative_to s) d ⇒
(P relative_to s) (c ∩ d)
[RELATIVE_TO_MONO] Theorem
⊢ ∀P Q.
(∀s. P s ⇒ Q s) ⇒ ∀u. (P relative_to u) s ⇒ (Q relative_to u) s
[RELATIVE_TO_RELATIVE_TO] Theorem
⊢ ∀P s t. P relative_to s relative_to t = P relative_to s ∩ t
[RELATIVE_TO_SUBSET] Theorem
⊢ ∀P s t. s ⊆ t ∧ P s ⇒ (P relative_to t) s
[RELATIVE_TO_SUBSET_INC] Theorem
⊢ ∀P u s. s ⊆ u ∧ P s ⇒ (P relative_to u) s
[RELATIVE_TO_SUBSET_TRANS] Theorem
⊢ ∀P u s t. (P relative_to u) s ∧ s ⊆ t ∧ t ⊆ u ⇒ (P relative_to t) s
[RELATIVE_TO_UNION] Theorem
⊢ ∀P s.
(∀c d. P c ∧ P d ⇒ P (c ∪ d)) ⇒
∀c d.
(P relative_to s) c ∧ (P relative_to s) d ⇒
(P relative_to s) (c ∪ d)
[RELATIVE_TO_UNIV] Theorem
⊢ ∀P s. (P relative_to 𝕌(:α)) s ⇔ P s
[SIMPLE_IMAGE] Theorem
⊢ ∀f s. {f x | x ∈ s} = IMAGE f s
[SING_GSPEC] Theorem
⊢ (∀a. {x | x = a} = {a}) ∧ ∀a. {x | a = x} = {a}
[SUBSET_HULL] Theorem
⊢ ∀P s t. P t ⇒ (P hull s ⊆ t ⇔ s ⊆ t)
[SUBSET_RESTRICT] Theorem
⊢ ∀s P. {x | x ∈ s ∧ P x} ⊆ s
[SUBTOPOLOGY_SUBTOPOLOGY] Theorem
⊢ ∀top s t.
subtopology (subtopology top s) t = subtopology top (s ∩ t)
[SUBTOPOLOGY_SUPERSET] Theorem
⊢ ∀top s. topspace top ⊆ s ⇒ subtopology top s = top
[SUBTOPOLOGY_TOPSPACE] Theorem
⊢ ∀top. subtopology top (topspace top) = top
[SUBTOPOLOGY_UNIV] Theorem
⊢ ∀top. subtopology top 𝕌(:α) = top
[TOPOLOGY_EQ] Theorem
⊢ ∀top1 top2. top1 = top2 ⇔ ∀s. open_in top1 s ⇔ open_in top2 s
[TOPSPACE_SUBTOPOLOGY] Theorem
⊢ ∀top u. topspace (subtopology top u) = topspace top ∩ u
[UNIONS_0] Theorem
⊢ BIGUNION ∅ = ∅
[UNIONS_1] Theorem
⊢ ∀x. BIGUNION {x} = x
[UNIONS_2] Theorem
⊢ ∀s t. BIGUNION {s; t} = s ∪ t
[UNIONS_GSPEC] Theorem
⊢ (∀P f. BIGUNION {f x | P x} = {a | ∃x. P x ∧ a ∈ f x}) ∧
(∀P f. BIGUNION {f x y | P x y} = {a | ∃x y. P x y ∧ a ∈ f x y}) ∧
∀P f.
BIGUNION {f x y z | P x y z} =
{a | ∃x y z. P x y z ∧ a ∈ f x y z}
[UNIONS_IMAGE] Theorem
⊢ ∀f s. BIGUNION (IMAGE f s) = {y | ∃x. x ∈ s ∧ y ∈ f x}
[UNIONS_INSERT] Theorem
⊢ ∀s P. BIGUNION (s INSERT P) = s ∪ BIGUNION P
[UNIONS_INTERS] Theorem
⊢ ∀s. BIGUNION s = 𝕌(:α) DIFF BIGINTER {𝕌(:α) DIFF t | t ∈ s}
[UNIONS_SUBSET] Theorem
⊢ ∀X P. BIGUNION P ⊆ X ⇔ ∀Y. Y ∈ P ⇒ Y ⊆ X
[UNIONS_UNION] Theorem
⊢ ∀s1 s2. BIGUNION (s1 ∪ s2) = BIGUNION s1 ∪ BIGUNION s2
[UNION_OF_EMPTY] Theorem
⊢ ∀P Q. P ∅ ⇒ (P UNION_OF Q) ∅
[UNION_OF_INC] Theorem
⊢ ∀P Q s. P {s} ∧ Q s ⇒ (P UNION_OF Q) s
[UNION_OF_MONO] Theorem
⊢ ∀P Q Q' s. (P UNION_OF Q) s ∧ (∀x. Q x ⇒ Q' x) ⇒ (P UNION_OF Q') s
[UNIV_GSPEC] Theorem
⊢ {x | T} = 𝕌(:α)
[closed_topspace] Theorem
⊢ ∀top. closed top ⇒ topspace top = 𝕌(:α)
[limpt_thm] Theorem
⊢ limpt t x A ⇔
x ∈ topspace t ∧
∀U. open_in t U ∧ x ∈ U ⇒ ∃y. y ∈ U ∧ y ∈ A ∧ y ≠ x
[open_topspace] Theorem
⊢ ∀top. open top ⇒ topspace top = 𝕌(:α)
[pairwiseD_alt_pairwiseN] Theorem
⊢ ∀R. pairwiseD R = pairwiseN (RC R)
*)
end
HOL 4, Trindemossen-1