Theory SML_Topological_Space
section‹Relativization of the results about simple topological spaces›
theory SML_Topological_Space
imports
"../Simple_Orders/SML_Simple_Orders"
"HOL-Analysis.Elementary_Topology"
"../Foundations/Transfer_Ext"
"../Foundations/Lifting_Set_Ext"
begin
subsection‹Definitions and common properties›
text‹
Some of the entities that are presented in this subsection were
copied from the theory \<^text>‹HOL-Types_To_Sets/Examples/T2_Spaces›.
›
locale topological_space_ow =
fixes U :: "'at set" and τ :: "'at set ⇒ bool"
assumes open_UNIV[simp, intro]: "τ U"
assumes open_Int[intro]:
"⟦ S ⊆ U; T ⊆ U; τ S; τ T ⟧ ⟹ τ (S ∩ T)"
assumes open_Union[intro]:
"⟦ K ⊆ Pow U; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)"
begin
context
includes lifting_syntax
begin
tts_register_sbts τ | U
proof-
assume dom_ATA: "Domainp ATA = (λx. x ∈ U)"
and "bi_unique ATA"
and "right_total ATA"
from ‹bi_unique ATA› ‹right_total ATA›
obtain Rep :: "'a ⇒ 'at" and Abs :: "'at ⇒ 'a" where
td: "type_definition Rep Abs (Collect (Domainp ATA))" and
ATA_Rep: "ATA b b' = (b = Rep b')" for b b'
by (blast dest: ex_type_definition)
define τ' where τ': "τ' = (image Rep ---> id) τ"
have Domainp_scr_S: "Domainp (rel_set ATA) = (λx. x ⊆ U)"
unfolding Domainp_set by (auto simp: dom_ATA)
have scr_S_rep[intro, simp]: "rel_set ATA (image Rep a) a" for a
unfolding rel_set_def by (auto simp: ATA_Rep)
have rel_set_eq_rep_set: "rel_set ATA x y ⟷ x = image Rep y" for x y
proof -
have "bi_unique (rel_set ATA)"
by (simp add: ‹bi_unique ATA› bi_unique_rel_set)
from this show ?thesis by (auto dest: bi_uniqueDl)
qed
have "(rel_set ATA ===> (=)) τ τ'"
unfolding τ' map_fun_apply id_def
apply(intro rel_funI)
unfolding rel_set_eq_rep_set
apply(elim ssubst)
..
then show " ∃τ'. (rel_set ATA ===> (=)) τ τ'" by auto
qed
end
end
locale topological_space_pair_ow =
ts⇩1: topological_space_ow U⇩1 τ⇩1 + ts⇩2: topological_space_ow U⇩2 τ⇩2
for U⇩1 :: "'at set" and τ⇩1 and U⇩2 :: "'bt set" and τ⇩2
locale topological_space_triple_ow =
ts⇩1: topological_space_ow U⇩1 τ⇩1 +
ts⇩2: topological_space_ow U⇩2 τ⇩2 +
ts⇩3: topological_space_ow U⇩3 τ⇩3
for U⇩1 :: "'at set" and τ⇩1
and U⇩2 :: "'bt set" and τ⇩2
and U⇩3 :: "'ct set" and τ⇩3
begin
sublocale tsp⇩1⇩2: topological_space_pair_ow U⇩1 τ⇩1 U⇩2 τ⇩2 ..
sublocale tsp⇩1⇩3: topological_space_pair_ow U⇩1 τ⇩1 U⇩3 τ⇩3 ..
sublocale tsp⇩2⇩3: topological_space_pair_ow U⇩2 τ⇩2 U⇩3 τ⇩3 ..
sublocale tsp⇩2⇩1: topological_space_pair_ow U⇩2 τ⇩2 U⇩1 τ⇩1 ..
sublocale tsp⇩3⇩1: topological_space_pair_ow U⇩3 τ⇩3 U⇩1 τ⇩1 ..
sublocale tsp⇩3⇩2: topological_space_pair_ow U⇩3 τ⇩3 U⇩2 τ⇩2 ..
end
inductive generate_topology_on :: "['at set set, 'at set, 'at set] ⇒ bool"
(
‹(in'_topology'_generated'_by _ on _ : «open» _)›
[1000, 1000, 1000] 10
)
for S :: "'at set set"
where
UNIV: "(in_topology_generated_by S on U : «open» U)"
| Int: "(in_topology_generated_by S on U : «open» (a ∩ b))"
if "(in_topology_generated_by S on U : «open» a)"
and "(in_topology_generated_by S on U : «open» b)"
and "a ⊆ U"
and "b ⊆ U"
| UN: "(in_topology_generated_by S on U : «open» (⋃K))"
if "K ⊆ Pow U"
and "(⋀k. k ∈ K ⟹ (in_topology_generated_by S on U : «open» k))"
| Basis: "(in_topology_generated_by S on U : «open» s)"
if "s ∈ S" and "s ⊆ U"
lemma gto_imp_ss: "(in_topology_generated_by S on U : «open» A) ⟹ A ⊆ U"
by (induction rule: generate_topology_on.induct) auto
lemma gt_eq_gto: "generate_topology = (λS. generate_topology_on S UNIV)"
proof(intro ext iffI)
fix S and x :: "'a set"
assume "generate_topology S x"
then show "in_topology_generated_by S on UNIV : «open» x"
by (induction rule: generate_topology.induct)
(simp_all add: UNIV Int UN Basis)
next
fix S and x :: "'a set"
assume gto: "in_topology_generated_by S on UNIV : «open» x"
define U where U: "U = (UNIV::'a set)"
from gto have "generate_topology_on S U x" unfolding U .
from this U show "generate_topology S x"
by (induction rule: generate_topology_on.induct)
(
simp_all add:
generate_topology.UNIV
generate_topology.Int
generate_topology.UN
generate_topology.Basis
)
qed
ud ‹topological_space.closed› (‹(with _ : «closed» _)› [1000, 1000] 10)
ud closed' ‹closed›
ud ‹topological_space.compact› (‹(with _ : «compact» _)› [1000, 1000] 10)
ud compact' ‹compact›
ud ‹topological_space.connected› (‹(with _ : «connected» _)› [1000, 1000] 10)
ud connected' ‹connected›
ud ‹topological_space.islimpt› (‹(with _ : _ «islimpt» _)› [1000, 1000, 1000] 60)
ud islimpt' ‹topological_space_class.islimpt›
ud ‹interior› (‹(with _ : «interior» _)› [1000, 1000] 10)
ud ‹closure› (‹(with _ : «closure» _)› [1000, 1000] 10)
ud ‹frontier› (‹(with _ : «frontier» _)› [1000, 1000] 10)
ud ‹countably_compact› (‹(with _ : «countably'_compact» _)› [1000, 1000] 10)
definition topological_basis_with :: "['a set ⇒ bool, 'a set set] ⇒ bool"
(‹(with _ : «topological'_basis» _)› [1000, 1000] 10)
where
"(with τ : «topological_basis» B) =
(⋃B = UNIV ∧ (∀b ∈ B. τ b) ∧ (∀q. τ q ⟶ (∃B'⊆B. ⋃B' = q)))"
ctr relativization
synthesis ctr_simps
assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (λx. x ∈ U)"
and [transfer_rule]: "bi_unique A" "right_total A"
trp (?'a A)
in closed_ow: closed.with_def
(‹(on _ with _ : «closed» _)› [1000, 1000] 10)
and compact_ow: compact.with_def
(‹(on _ with _ : «compact» _)› [1000, 1000, 1000] 10)
and connected_ow: connected.with_def
(‹(on _ with _ : «connected» _)› [1000, 1000, 1000] 10)
and islimpt_ow: islimpt.with_def
(‹(on _ with _ : _ «islimpt» _)› [1000, 1000, 1000, 1000] 10)
and interior_ow: interior.with_def
(‹(on _ with _ : «interior» _)› [1000, 1000, 1000] 10)
and closure_ow: closure.with_def
(‹(on _ with _ : «closure» _)› [1000, 1000, 1000] 10)
and frontier_ow: frontier.with_def
(‹(on _ with _ : «frontier» _)› [1000, 1000, 1000] 10)
and countably_compact_ow: countably_compact.with_def
(‹(on _ with _ : «countably'_compact» _)› [1000, 1000, 1000] 10)
context topological_space_ow
begin
abbreviation closed where "closed ≡ closed_ow U τ"
abbreviation compact where "compact ≡ compact_ow U τ"
abbreviation connected where "connected ≡ connected_ow U τ"
abbreviation islimpt (infixr ‹«islimpt»› 60)
where "x «islimpt» S ≡ on U with τ : x «islimpt» S"
abbreviation interior where "interior ≡ interior_ow U τ"
abbreviation closure where "closure ≡ closure_ow U τ"
abbreviation frontier where "frontier ≡ frontier_ow U τ"
abbreviation countably_compact
where "countably_compact ≡ countably_compact_ow U τ"
end
context
includes lifting_syntax
begin
private lemma Domainp_fun_rel_eq_subset:
fixes A :: "['a, 'c] ⇒ bool"
fixes B :: "['b, 'd] ⇒ bool"
assumes "bi_unique A" "bi_unique B"
shows
"Domainp (A ===> B) =
(λf. f ` (Collect (Domainp A)) ⊆ (Collect (Domainp B)))"
proof(intro ext, standard)
let ?sA = "Collect (Domainp A)" and ?sB = "(Collect (Domainp B))"
fix f assume "Domainp (A ===> B) f" show "f ` ?sA ⊆ ?sB"
proof(clarsimp)
fix x x' assume "A x x'"
from ‹Domainp (A ===> B) f› obtain f' where f':
"A x x' ⟹ B (f x) (f' x')" for x x'
unfolding rel_fun_def by auto
with ‹A x x'› have "B (f x) (f' x')" by simp
thus "Domainp B (f x)" by auto
qed
next
let ?sA = "Collect (Domainp A)" and ?sB = "(Collect (Domainp B))"
fix f assume "f ` ?sA ⊆ ?sB"
define f' where f': "f' = (λx'. (THE y'. ∃x. A x x' ∧ B (f x) y'))"
have "(A ===> B) f f'"
proof(intro rel_funI)
fix x x' assume "A x x'"
then have "f x ∈ ?sB" using ‹f ` ?sA ⊆ ?sB› by auto
then obtain y' where y': "B (f x) y'" by clarsimp
have "f' x' = y'" unfolding f'
proof
from ‹A x x'› y' show "∃x. A x x' ∧ B (f x) y'" by auto
{
fix y'' assume "∃x. A x x' ∧ B (f x) y''"
then obtain x'' where x'': "A x'' x' ∧ B (f x'') y''" by clarsimp
with assms(1) have "x'' = x" using ‹A x x'› by (auto dest: bi_uniqueDl)
with y' x'' have "y'' = y'" using assms(2) by (auto dest: bi_uniqueDr)
}
thus "∃x. A x x' ∧ B (f x) y'' ⟹ y'' = y'" for y'' by simp
qed
thus "B (f x) (f' x')" using y' by simp
qed
thus "Domainp (A ===> B) f" by auto
qed
private lemma Ex_rt_bu_transfer[transfer_rule]:
fixes A :: "['a, 'c] ⇒ bool"
fixes B :: "['b, 'd] ⇒ bool"
assumes [transfer_rule]: "bi_unique A" "right_total A" "bi_unique B"
shows
"(((B ===> A) ===> (=)) ===> (=))
(Bex (Collect (λf. f ` (Collect (Domainp B)) ⊆ (Collect (Domainp A)))))
Ex"
proof-
from assms(3,1) have domainp_eq_ss:
"Domainp (B ===> A) =
(λf. f ` (Collect (Domainp B)) ⊆ (Collect (Domainp A)))"
by (rule Domainp_fun_rel_eq_subset)
have "right_total (B ===> A)"
using assms by (simp add: bi_unique_alt_def right_total_fun)
then have
"(((B ===> A) ===> (=)) ===> (=)) (Bex (Collect (Domainp (B ===> A)))) Ex"
by (simp add: right_total_Ex_transfer)
thus ?thesis unfolding domainp_eq_ss by simp
qed
end
definition topological_basis_ow ::
"['a set, 'a set ⇒ bool, 'a set set] ⇒ bool"
(‹(on _ with _ : «topological'_basis» _)› [1000, 1000, 1000] 10)
where
"(on U with τ : «topological_basis» B) =
(⋃B = U ∧ (∀b ∈ B. τ b) ∧ (∀q ⊆ U. τ q ⟶ (∃B'⊆ B. ⋃B' = q)))"
context topological_space
begin
lemma topological_basis_with[ud_with]:
"topological_basis = topological_basis_with open"
unfolding topological_basis_def topological_basis_with_def Ball_def
by (intro ext) (metis Union_mono open_UNIV top.extremum_uniqueI)
end
subsection‹Transfer rules›
text‹Some of the entities that are presented in this subsectionwere
copied from \<^text>‹HOL-Types_To_Sets/Examples/T2_Spaces›.›
context
includes lifting_syntax
begin
lemmas vimage_transfer[transfer_rule] = vimage_transfer
lemma topological_space_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((rel_set A ===> (=)) ===> (=))
(topological_space_ow (Collect (Domainp A))) class.topological_space"
unfolding topological_space_ow_def class.topological_space_def
apply transfer_prover_start
apply transfer_step+
unfolding Pow_def Ball_Collect[symmetric]
by auto
lemma generate_topology_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((rel_set (rel_set A)) ===> (rel_set A ===> (=)))
(λB. generate_topology_on B (Collect (Domainp A))) generate_topology"
proof(intro rel_funI, standard)
fix BL BR xl xr
assume
rsrsT_BLR: "rel_set (rel_set A) BL BR" and
rsT_xl_xr: "rel_set A xl xr" and
gto: "generate_topology_on BL (Collect (Domainp A)) xl"
define CDT where CDT: "CDT = (Collect (Domainp A))"
with gto have gto_CDT: "generate_topology_on BL CDT xl" by simp
from gto_CDT CDT rsrsT_BLR rsT_xl_xr show "generate_topology BR xr"
proof(induction arbitrary: xr rule: generate_topology_on.induct)
case (UNIV S) show ?case
proof -
from assms UNIV.prems have "xr = UNIV"
by (meson bi_uniqueDr bi_unique_rel_set right_total_UNIV_transfer)
thus "generate_topology BR xr" by (simp add: generate_topology.UNIV)
qed
next
case (Int S a b) show ?case
proof -
from Int.hyps(3) Int.prems(1) obtain a' where a': "rel_set A a a'"
by (metis Ball_Collect Domainp_iff Domainp_set)
from Int.hyps(4) Int.prems(1) obtain b' where b': "rel_set A b b'"
by (metis Ball_Collect Domainp_iff Domainp_set)
from Int.prems(1) Int.prems(2) a' have gt_a': "generate_topology BR a'"
by (rule Int.IH(1))
from Int.prems(1) Int.prems(2) b' have gt_b': "generate_topology BR b'"
by (rule Int.IH(2))
from gt_a' gt_b' have "generate_topology BR (a' ∩ b')"
by (rule generate_topology.Int)
also from assms(1) a' b' Int.prems(3) have "a' ∩ b' = xr"
by (rule bi_unique_intersect_r)
ultimately show "generate_topology BR xr" by simp
qed
next
case (UN K S) thus ?case
proof -
define K' where K': "K' = {(x, y). rel_set A x y} `` K" (is "K' = ?K'")
have Union_ss_CDT: "⋃K ⊆ Collect (Domainp A)"
by (metis CollectI Domainp.DomainI UN.prems(3) rel_setD1 subsetI)
from assms(1) Union_ss_CDT UN.prems(3) have "⋃?K' = xr"
by (rule bi_unique_Union_r)
then have UK_eq_xr: "⋃K' = xr" unfolding K' .
have "k' ∈ K' ⟹ generate_topology BR k'" for k'
proof -
assume k'_in_K': "k' ∈ K'"
then obtain k where k: "rel_set A k k'" unfolding K' by auto
from assms(1) have "bi_unique (rel_set A)" by (rule bi_unique_rel_set)
with k have "∃!k. rel_set A k k'" by (meson bi_uniqueDl)
with k'_in_K' k have k_in_K: "k ∈ K" unfolding K' by auto
from k_in_K UN.prems(1,2) k show "generate_topology BR k'"
by (rule UN.IH)
qed
then have "generate_topology BR (⋃K')" by (rule generate_topology.UN)
with UK_eq_xr show "generate_topology BR xr" by simp
qed
next
case (Basis xl S) thus ?case
using assms(1)
by (metis Int_absorb1 bi_unique_intersect_r generate_topology.Basis
rel_setD1 subset_refl)
qed
next
fix BL BR xl xr
assume rsrsT_BLR: "rel_set (rel_set A) BL BR"
and rsT_xl_xr: "rel_set A xl xr"
and gt: "generate_topology BR xr"
from gt rsrsT_BLR rsT_xl_xr show
"generate_topology_on BL (Collect (Domainp A)) xl"
proof(induction arbitrary: xl rule: generate_topology.induct)
case UNIV thus ?case using assms
by (metis bi_uniqueDl bi_unique_rel_set generate_topology_on.simps
right_total_UNIV_transfer)
next
case (Int a' b') show ?case
proof -
from assms(2) obtain a where a: "rel_set A a a'"
by (meson right_totalE right_total_rel_set)
from assms(2) obtain b where b: "rel_set A b b'"
by (meson right_totalE right_total_rel_set)
from Int.prems(1) a have gto_a:
"generate_topology_on BL {x. Domainp A x} a"
by (rule Int.IH(1))
from Int.prems(1) b have gto_b:
"generate_topology_on BL {x. Domainp A x} b"
by (rule Int.IH(2))
from a have a_ss_DT: "a ⊆ {x. Domainp A x}"
by auto (meson Domainp.DomainI rel_setD1)
from b have b_ss_DT: "b ⊆ {x. Domainp A x}"
by auto (meson Domainp.DomainI rel_setD1)
from gto_a gto_b a_ss_DT b_ss_DT have
"generate_topology_on BL {x. Domainp A x} (a ∩ b)"
by (rule generate_topology_on.Int)
also from assms(1) a b Int.prems(2) have "a ∩ b = xl"
by (rule bi_unique_intersect_l)
ultimately show "generate_topology_on BL {a. Domainp A a} xl" by simp
qed
next
case (UN K') thus ?case
proof -
define K where K: "K = {(x, y). rel_set (λy x. A x y) x y} `` K'"
(is "K = ?K")
from assms(2) have Union_ss_CRT: "⋃K' ⊆ Collect (Rangep A)"
by (auto simp add: Domainp_iff right_total_def)
from assms(1) Union_ss_CRT UN.prems(2) have "⋃?K = xl"
by (rule bi_unique_Union_l)
then have UK_eq_xr: "⋃K = xl" unfolding K .
then have "K ⊆ Pow xl" by blast
moreover from UN.prems(2) have "xl ⊆ {x. Domainp A x}"
unfolding rel_set_def by blast
ultimately have UN_prem_1: "K ⊆ Pow {x. Domainp A x}" by auto
have UN_prem_2:
"k ∈ K ⟹ generate_topology_on BL {x. Domainp A x} k" for k
proof -
assume k_in_K: "k ∈ K"
with UN_prem_1 have k_ss_DT: "k ⊆ {x. Domainp A x}" by auto
with k_in_K obtain k' where k': "rel_set (λy x. A x y) k' k"
unfolding K Ball_Collect[symmetric] by blast
from assms(1) have "bi_unique (λy x. A x y)"
unfolding bi_unique_def by simp
then have "bi_unique (rel_set (λy x. A x y))"
by (rule bi_unique_rel_set)
with k' have "∃!k'. rel_set (λy x. A x y) k' k" by (meson bi_uniqueDl)
with k_in_K k' have k'_in_K': "k' ∈ K'" unfolding K by blast
from k' have rsT_kk': "rel_set A k k'" unfolding rel_set_def by auto
from k'_in_K' UN.prems(1) rsT_kk' show
"generate_topology_on BL {x. Domainp A x} k"
by (rule UN.IH)
qed
from UN_prem_1 UN_prem_2 have
"generate_topology_on BL {x. Domainp A x} (⋃K)"
by (rule generate_topology_on.UN)
with UK_eq_xr show "generate_topology_on BL {a. Domainp A a} xl" by simp
qed
next
case (Basis xr) thus ?case
proof -
assume xr_in_BR: "xr ∈ BR"
and rsrsT_BL_BR: "rel_set (rel_set A) BL BR"
and rsT_xl_xr: "rel_set A xl xr"
with assms(1) have "xl ∈ BL"
by (metis bi_uniqueDl bi_unique_rel_set rel_setD2)
also with rsrsT_BL_BR have "xl ⊆ {a. Domainp A a}"
unfolding Ball_Collect[symmetric] by (meson Domainp.DomainI rel_setD1)
ultimately show "generate_topology_on BL {a. Domainp A a} xl"
by (rule generate_topology_on.Basis)
qed
qed
qed
lemma topological_basis_with_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((rel_set A ===> (=)) ===> (rel_set (rel_set A)) ===> (=))
(topological_basis_ow (Collect (Domainp A))) topological_basis_with"
unfolding topological_basis_ow_def topological_basis_with_def
apply transfer_prover_start
apply transfer_step+
unfolding Ball_Collect[symmetric]
apply(clarsimp, intro ext iffI)
subgoal by (metis UnionI)
subgoal by metis
done
end
subsection‹Relativization›
tts_context
tts: (?'a to ‹U⇩1::'a set›) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
begin
tts_lemma generate_topology_Union:
assumes "U⇩1 ≠ {}"
and "U⇩2 ≠ {}"
and "I ⊆ U⇩1"
and "S ⊆ Pow U⇩2"
and "∀x∈U⇩1. K (x::'a) ⊆ U⇩2"
and
"⋀k. ⟦k ∈ U⇩1; k ∈ I⟧ ⟹
in_topology_generated_by S on U⇩2 : «open» (K k)"
shows "in_topology_generated_by S on U⇩2 : «open» (⋃ (K ` I))"
is generate_topology_Union.
end
tts_context
tts: (?'a to ‹U::'a set›)
rewriting ctr_simps
eliminating through
(unfold topological_space_ow_def; auto intro: generate_topology_on.intros)
begin
tts_lemma topological_space_generate_topology:
shows "topological_space_ow U (generate_topology_on S U)"
is topological_space_generate_topology.
end
context topological_space_ow
begin
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating through (metis open_UNIV)
begin
tts_lemma open_empty[simp]:
shows "τ {}"
is topological_space_class.open_empty.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating through
(
unfold
closed_ow_def
compact_ow_def
connected_ow_def
interior_ow_def
closure_ow_def
frontier_ow_def,
auto
)
begin
tts_lemma closed_empty[simp]: "closed {}"
is topological_space_class.closed_empty.
tts_lemma closed_UNIV[simp]: "closed U"
is topological_space_class.closed_UNIV.
tts_lemma compact_empty[simp]: "compact {}"
is topological_space_class.compact_empty.
tts_lemma connected_empty[simp]: "connected {}"
is topological_space_class.connected_empty.
tts_lemma interior_empty[simp]: "interior {} = {}"
is interior_empty.
tts_lemma closure_empty[simp]: "closure {} = {}"
is closure_empty.
tts_lemma closure_UNIV[simp]: "closure U = U"
is closure_UNIV.
tts_lemma frontier_empty[simp]: "frontier {} = {}"
is frontier_empty.
tts_lemma frontier_UNIV[simp]: "frontier U = {}"
is frontier_UNIV.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating through (auto simp: UNIV inj_on_def)
begin
tts_lemma connected_Union:
assumes "S ⊆ Pow U" and "⋀s. s ∈ S ⟹ connected s" and "⋂ S ∩ U ≠ {}"
shows "connected (⋃ S)"
given Topological_Spaces.connected_Union
by simp
tts_lemma connected_Un:
assumes "s ⊆ U"
and "t ⊆ U"
and "connected s"
and "connected t"
and "s ∩ t ≠ {}"
shows "connected (s ∪ t)"
is Topological_Spaces.connected_Un.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› and ‹?A ⊆ ?B›
through (auto simp: UNIV inj_on_def)
begin
tts_lemma connected_sing:
assumes "x ∈ U"
shows "connected {x}"
is topological_space_class.connected_sing.
tts_lemma topological_basisE:
assumes "B ⊆ Pow U"
and "O' ⊆ U"
and "x ∈ U"
and "on U with τ : «topological_basis» B"
and "τ O'"
and "x ∈ O'"
and "⋀B'. ⟦B' ⊆ U; B' ∈ B; x ∈ B'; B' ⊆ O'⟧ ⟹ thesis"
shows thesis
is topological_space_class.topological_basisE.
tts_lemma islimptE:
assumes "x ∈ U"
and "S ⊆ U"
and "T ⊆ U"
and "x «islimpt» S"
and "x ∈ T"
and "τ T"
and "⋀y. ⟦y ∈ U; y ∈ S; y ∈ T; y ≠ x⟧ ⟹ thesis"
shows thesis
is Elementary_Topology.islimptE.
tts_lemma islimpt_subset:
assumes "x ∈ U" and "T ⊆ U" and "x «islimpt» S" and "S ⊆ T"
shows "x «islimpt» T"
is Elementary_Topology.islimpt_subset.
tts_lemma islimpt_UNIV_iff:
assumes "x ∈ U"
shows "x «islimpt» U = (¬ τ {x})"
is Elementary_Topology.islimpt_UNIV_iff.
tts_lemma islimpt_punctured:
assumes "x ∈ U" and "S ⊆ U"
shows "x «islimpt» S = x «islimpt» S - {x}"
is Elementary_Topology.islimpt_punctured.
tts_lemma islimpt_EMPTY:
assumes "x ∈ U"
shows "¬ x «islimpt» {}"
is Elementary_Topology.islimpt_EMPTY.
tts_lemma islimpt_Un:
assumes "x ∈ U" and "S ⊆ U" and "T ⊆ U"
shows "x «islimpt» S ∪ T = (x «islimpt» S ∨ x «islimpt» T)"
is Elementary_Topology.islimpt_Un.
tts_lemma interiorI:
assumes "x ∈ U" and "S ⊆ U" and "τ T" and "x ∈ T" and "T ⊆ S"
shows "x ∈ interior S"
is Elementary_Topology.interiorI.
tts_lemma islimpt_in_closure:
assumes "x ∈ U" and "S ⊆ U"
shows "x «islimpt» S = (x ∈ closure (S - {x}))"
is Elementary_Topology.islimpt_in_closure.
tts_lemma compact_sing:
assumes "a ∈ U"
shows "compact {a}"
is Elementary_Topology.compact_sing.
tts_lemma compact_insert:
assumes "s ⊆ U" and "x ∈ U" and "compact s"
shows "compact (insert x s)"
is Elementary_Topology.compact_insert.
tts_lemma open_Un:
assumes "S ⊆ U" and "T ⊆ U" and "τ S" and "τ T"
shows "τ (S ∪ T)"
is topological_space_class.open_Un.
tts_lemma open_Inter:
assumes "S ⊆ Pow U" and "finite S" and "Ball S τ"
shows "τ (⋂ S ∩ U)"
is topological_space_class.open_Inter.
tts_lemma openI:
assumes "S ⊆ U" and "⋀x. ⟦x ∈ U; x ∈ S⟧ ⟹ ∃y⊆U. τ y ∧ y ⊆ S ∧ x ∈ y"
shows "τ S"
given topological_space_class.openI by (meson PowI)
tts_lemma closed_Un:
assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "closed T"
shows "closed (S ∪ T)"
is topological_space_class.closed_Un.
tts_lemma closed_Int:
assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "closed T"
shows "closed (S ∩ T)"
is topological_space_class.closed_Int.
tts_lemma open_Collect_conj:
assumes "τ {x. P x ∧ x ∈ U}" and "τ {x. Q x ∧ x ∈ U}"
shows "τ {x ∈ U. P x ∧ Q x}"
is topological_space_class.open_Collect_conj.
tts_lemma open_Collect_disj:
assumes "τ {x. P x ∧ x ∈ U}"
and "τ {x. Q x ∧ x ∈ U}"
shows "τ {x ∈ U. P x ∨ Q x}"
is topological_space_class.open_Collect_disj.
tts_lemma open_Collect_imp:
assumes "closed {x. P x ∧ x ∈ U}"
and "τ {x. Q x ∧ x ∈ U}"
shows "τ {x ∈ U. P x ⟶ Q x}"
is topological_space_class.open_Collect_imp.
tts_lemma open_Collect_const: "τ {x. P ∧ x ∈ U}"
is topological_space_class.open_Collect_const.
tts_lemma closed_Collect_conj:
assumes "closed {x. P x ∧ x ∈ U}" and "closed {x. Q x ∧ x ∈ U}"
shows "closed {x ∈ U. P x ∧ Q x}"
is topological_space_class.closed_Collect_conj.
tts_lemma closed_Collect_disj:
assumes "closed {x. P x ∧ x ∈ U}" and "closed {x. Q x ∧ x ∈ U}"
shows "closed {x ∈ U. P x ∨ Q x}"
is topological_space_class.closed_Collect_disj.
tts_lemma closed_Collect_imp:
assumes "τ {x. P x ∧ x ∈ U}" and "closed {x. Q x ∧ x ∈ U}"
shows "closed {x ∈ U. P x ⟶ Q x}"
is topological_space_class.closed_Collect_imp.
tts_lemma compact_Int_closed:
assumes "S ⊆ U" and "T ⊆ U" and "compact S" and "closed T"
shows "compact (S ∩ T)"
is topological_space_class.compact_Int_closed.
tts_lemma compact_diff:
assumes "S ⊆ U" and "T ⊆ U" and "compact S" and "τ T"
shows "compact (S - T)"
is topological_space_class.compact_diff.
tts_lemma connectedD:
assumes "U ⊆ U"
and "V ⊆ U"
and "connected A"
and "τ U"
and "τ V"
and "U ∩ (V ∩ A) = {}"
and "A ⊆ U ∪ V"
shows "U ∩ A = {} ∨ V ∩ A = {}"
is topological_space_class.connectedD.
tts_lemma topological_basis_open:
assumes "B ⊆ Pow U" and "on U with τ : «topological_basis» B" and "X ∈ B"
shows "τ X"
is topological_space_class.topological_basis_open.
tts_lemma topological_basis_imp_subbasis:
assumes "B ⊆ Pow U" and "on U with τ : «topological_basis» B"
shows "∀s⊆U. τ s = (in_topology_generated_by B on U : «open» s)"
is topological_space_class.topological_basis_imp_subbasis.
tts_lemma connected_closedD:
assumes "A ⊆ U"
and "B ⊆ U"
and "connected s"
and "A ∩ (B ∩ s) = {}"
and "s ⊆ A ∪ B"
and "closed A"
and "closed B"
shows "A ∩ s = {} ∨ B ∩ s = {}"
is Topological_Spaces.connected_closedD.
tts_lemma connected_diff_open_from_closed:
assumes "u ⊆ U"
and "s ⊆ t"
and "t ⊆ u"
and "τ s"
and "closed t"
and "connected u"
and "connected (t - s)"
shows "connected (u - s)"
is Topological_Spaces.connected_diff_open_from_closed.
tts_lemma interior_maximal:
assumes "S ⊆ U" and "T ⊆ S" and "τ T"
shows "T ⊆ interior S"
is Elementary_Topology.interior_maximal.
tts_lemma open_subset_interior:
assumes "S ⊆ U" and "T ⊆ U" and "τ S"
shows "(S ⊆ interior T) = (S ⊆ T)"
is Elementary_Topology.open_subset_interior.
tts_lemma interior_mono:
assumes "T ⊆ U" and "S ⊆ T"
shows "interior S ⊆ interior T"
is Elementary_Topology.interior_mono.
tts_lemma interior_Int:
assumes "S ⊆ U" and "T ⊆ U"
shows "interior (S ∩ T) = interior S ∩ interior T"
is Elementary_Topology.interior_Int.
tts_lemma interior_closed_Un_empty_interior:
assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "interior T = {}"
shows "interior (S ∪ T) = interior S"
is Elementary_Topology.interior_closed_Un_empty_interior.
tts_lemma countably_compact_imp_acc_point:
assumes "local.countably_compact s"
and "countable t"
and "infinite t"
and "t ⊆ s"
shows "∃x∈s. ∀U∈Pow U. τ U ∧ x ∈ U ⟶ infinite (U ∩ t)"
is Elementary_Topology.countably_compact_imp_acc_point.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}›
through (auto simp: UNIV inj_on_def)
begin
tts_lemma first_countableI:
assumes "𝒜 ⊆ Pow U"
and "x ∈ U"
and "countable 𝒜"
and "⋀A. ⟦A ∈ 𝒜⟧ ⟹ x ∈ A"
and "⋀A. ⟦A ∈ 𝒜⟧ ⟹ τ A"
and "⋀S. ⟦τ S; x ∈ S⟧ ⟹ ∃A∈𝒜. A ⊆ S"
shows "∃𝒜∈{f. range f ⊆ Pow U}.
(∀i. τ (𝒜 (i::nat)) ∧ x ∈ 𝒜 i) ∧
(∀S∈Pow U. τ S ∧ x ∈ S ⟶ (∃i. 𝒜 i ⊆ S))"
given topological_space_class.first_countableI by auto
tts_lemma islimptI:
assumes "x ∈ U"
and "S ⊆ U"
and "⋀T. ⟦x ∈ T; τ T⟧ ⟹ ∃y∈S. y ∈ T ∧ y ≠ x"
shows "x «islimpt» S"
given Elementary_Topology.islimptI
by simp
tts_lemma interiorE:
assumes "x ∈ U"
and "S ⊆ U"
and "x ∈ interior S"
and "⋀T. ⟦T ⊆ U; τ T; x ∈ T; T ⊆ S⟧ ⟹ thesis"
shows thesis
is Elementary_Topology.interiorE.
tts_lemma closure_iff_nhds_not_empty:
assumes "x ∈ U" and "X ⊆ U"
shows
"(x ∈ closure X) =
(∀y⊆U. ∀z⊆U. z ⊆ y ⟶ τ z ⟶ x ∈ z ⟶ X ∩ y ≠ {})"
given Elementary_Topology.closure_iff_nhds_not_empty by auto
tts_lemma basis_dense:
assumes "B ⊆ Pow U"
and "∀x⊆U. f x ∈ U"
and "on U with τ : «topological_basis» B"
and "⋀B'. ⟦B' ⊆ U; B' ≠ {}⟧ ⟹ f B' ∈ B'"
shows "∀x⊆U. τ x ⟶ x ≠ {} ⟶ (∃y∈B. f y ∈ x)"
given topological_space_class.basis_dense by auto
tts_lemma inj_setminus:
assumes "A ⊆ Pow U"
shows "inj_on (λS. - S ∩ U) A"
is topological_space_class.inj_setminus.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› and ‹?S ⊆ U› through
(
unfold
closed_ow_def
compact_ow_def
connected_ow_def
interior_ow_def
topological_basis_ow_def
closure_ow_def
frontier_ow_def
countably_compact_ow_def,
auto
)
begin
tts_lemma closed_Inter:
assumes "K ⊆ Pow U" and "Ball K closed"
shows "closed (⋂ K ∩ U)"
is topological_space_class.closed_Inter.
tts_lemma closed_Union:
assumes "S ⊆ Pow U" and "finite S" and "Ball S closed"
shows "closed (⋃ S)"
is topological_space_class.closed_Union.
tts_lemma open_closed:
assumes "S ⊆ U"
shows "τ S = closed (- S ∩ U)"
is topological_space_class.open_closed.
tts_lemma closed_open:
shows "closed S = τ (- S ∩ U)"
is topological_space_class.closed_open.
tts_lemma open_Diff:
assumes "S ⊆ U" and "T ⊆ U" and "τ S" and "closed T"
shows "τ (S - T)"
is topological_space_class.open_Diff.
tts_lemma closed_Diff:
assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "τ T"
shows "closed (S - T)"
is topological_space_class.closed_Diff.
tts_lemma open_Compl:
assumes "closed S"
shows "τ (- S ∩ U)"
is topological_space_class.open_Compl.
tts_lemma closed_Compl:
assumes "S ⊆ U" and "τ S"
shows "closed (- S ∩ U)"
is topological_space_class.closed_Compl.
tts_lemma open_Collect_neg:
assumes "closed {x ∈ U. P x}"
shows "τ {x ∈ U. ¬ P x}"
given topological_space_class.open_Collect_neg
by (simp add: ctr_simps_conj_commute)
tts_lemma closed_Collect_neg:
assumes "τ {x∈U. P x}"
shows "closed {x∈U. ¬ P x}"
given topological_space_class.closed_Collect_neg
by (simp add: ctr_simps_conj_commute)
tts_lemma closed_Collect_const: "closed {x ∈ U. P}"
given topological_space_class.closed_Collect_const
by (simp add: ctr_simps_conj_commute)
tts_lemma connectedI:
assumes
"⋀A B.
⟦
A ⊆ U;
B ⊆ U;
τ A;
τ B;
A ∩ U ≠ {};
B ∩ U ≠ {};
A ∩ (B ∩ U) = {};
U ⊆ A ∪ B
⟧ ⟹ False"
shows "connected U"
is topological_space_class.connectedI.
tts_lemma topological_basis:
assumes "B ⊆ Pow U"
shows "(on U with τ : «topological_basis» B) =
(∀x∈Pow U. τ x = (∃B'∈Pow (Pow U). B' ⊆ B ∧ ⋃ B' = x))"
is topological_space_class.topological_basis.
tts_lemma topological_basis_iff:
assumes "B ⊆ Pow U" and "⋀B'. ⟦B' ⊆ U; B' ∈ B⟧ ⟹ τ B'"
shows "(on U with τ : «topological_basis» B) =
(∀O'∈Pow U. τ O' ⟶ (∀x∈O'. ∃B'∈B. B' ⊆ O' ∧ x ∈ B'))"
is topological_space_class.topological_basis_iff.
tts_lemma topological_basisI:
assumes "B ⊆ Pow U"
and "⋀B'. ⟦B' ⊆ U; B' ∈ B⟧ ⟹ τ B'"
and "⋀O' x. ⟦O' ⊆ U; x ∈ U; τ O'; x ∈ O'⟧ ⟹ ∃y∈B. y ⊆ O' ∧ x ∈ y"
shows "on U with τ : «topological_basis» B"
is topological_space_class.topological_basisI.
tts_lemma closed_closure:
assumes "S ⊆ U"
shows "closed (closure S)"
is Elementary_Topology.closed_closure.
tts_lemma closure_subset: "S ⊆ closure S"
is Elementary_Topology.closure_subset.
tts_lemma closure_eq:
assumes "S ⊆ U"
shows "(closure S = S) = closed S"
is Elementary_Topology.closure_eq.
tts_lemma closure_closed:
assumes "S ⊆ U" and "closed S"
shows "closure S = S"
is Elementary_Topology.closure_closed.
tts_lemma closure_closure:
assumes "S ⊆ U"
shows "closure (closure S) = closure S"
is Elementary_Topology.closure_closure.
tts_lemma closure_mono:
assumes "T ⊆ U" and "S ⊆ T"
shows "closure S ⊆ closure T"
is Elementary_Topology.closure_mono.
tts_lemma closure_minimal:
assumes "T ⊆ U" and "S ⊆ T" and "closed T"
shows "closure S ⊆ T"
is Elementary_Topology.closure_minimal.
tts_lemma closure_unique:
assumes "T ⊆ U"
and "S ⊆ T"
and "closed T"
and "⋀T'. ⟦T' ⊆ U; S ⊆ T'; closed T'⟧ ⟹ T ⊆ T'"
shows "closure S = T"
is Elementary_Topology.closure_unique.
tts_lemma closure_Un:
assumes "S ⊆ U" and "T ⊆ U"
shows "closure (S ∪ T) = closure S ∪ closure T"
is Elementary_Topology.closure_Un.
tts_lemma closure_eq_empty: "(closure S = {}) = (S = {})"
is Elementary_Topology.closure_eq_empty.
tts_lemma closure_subset_eq:
assumes "S ⊆ U"
shows "(closure S ⊆ S) = closed S"
is Elementary_Topology.closure_subset_eq.
tts_lemma open_Int_closure_eq_empty:
assumes "S ⊆ U" and "T ⊆ U" and "τ S"
shows "(S ∩ closure T = {}) = (S ∩ T = {})"
is Elementary_Topology.open_Int_closure_eq_empty.
tts_lemma open_Int_closure_subset:
assumes "S ⊆ U" and "T ⊆ U" and "τ S"
shows "S ∩ closure T ⊆ closure (S ∩ T)"
is Elementary_Topology.open_Int_closure_subset.
tts_lemma closure_Un_frontier: "closure S = S ∪ frontier S"
is Elementary_Topology.closure_Un_frontier.
tts_lemma compact_imp_countably_compact:
assumes "compact U"
shows "countably_compact U"
is Elementary_Topology.compact_imp_countably_compact.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating through auto
begin
tts_lemma Heine_Borel_imp_Bolzano_Weierstrass:
assumes "s ⊆ U"
and "compact s"
and "infinite t"
and "t ⊆ s"
shows "∃x∈s. x «islimpt» t"
is Elementary_Topology.Heine_Borel_imp_Bolzano_Weierstrass.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› through
(
unfold
closed_ow_def
compact_ow_def
connected_ow_def
interior_ow_def
topological_basis_ow_def
closure_ow_def
frontier_ow_def
countably_compact_ow_def,
auto simp: connected_iff_const
)
begin
tts_lemma connected_closed:
assumes "s ⊆ U"
shows "connected s =
(
¬(∃A∈Pow U. ∃B∈Pow U.
closed A ∧
closed B ∧
s ⊆ A ∪ B ∧
A ∩ (B ∩ s) = {} ∧
A ∩ s ≠ {} ∧
B ∩ s ≠ {})
)"
is Topological_Spaces.connected_closed.
tts_lemma closure_complement:
assumes "S ⊆ U"
shows "closure (- S ∩ U) = - interior S ∩ U"
is Elementary_Topology.closure_complement.
tts_lemma interior_complement:
assumes "S ⊆ U"
shows "interior (- S ∩ U) = - closure S ∩ U"
is Elementary_Topology.interior_complement.
tts_lemma interior_diff:
assumes "S ⊆ U" and "T ⊆ U"
shows "interior (S - T) = interior S - closure T"
is Elementary_Topology.interior_diff.
tts_lemma connected_imp_connected_closure:
assumes "S ⊆ U" and "connected S"
shows "connected (closure S)"
is Elementary_Topology.connected_imp_connected_closure.
tts_lemma frontier_closed:
assumes "S ⊆ U"
shows "closed (frontier S)"
is Elementary_Topology.frontier_closed.
tts_lemma frontier_Int:
assumes "S ⊆ U" and "T ⊆ U"
shows "frontier (S ∩ T) = closure (S ∩ T) ∩ (frontier S ∪ frontier T)"
is Elementary_Topology.frontier_Int.
tts_lemma frontier_closures:
assumes "S ⊆ U"
shows "frontier S = closure S ∩ closure (- S ∩ U)"
is Elementary_Topology.frontier_closures.
tts_lemma frontier_Int_subset:
assumes "S ⊆ U" and "T ⊆ U"
shows "frontier (S ∩ T) ⊆ frontier S ∪ frontier T"
is Elementary_Topology.frontier_Int_subset.
tts_lemma frontier_Int_closed:
assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "closed T"
shows "frontier (S ∩ T) = frontier S ∩ T ∪ S ∩ frontier T"
is Elementary_Topology.frontier_Int_closed.
tts_lemma frontier_subset_closed:
assumes "S ⊆ U" and "closed S"
shows "frontier S ⊆ S"
is Elementary_Topology.frontier_subset_closed.
tts_lemma frontier_subset_eq:
assumes "S ⊆ U"
shows "(frontier S ⊆ S) = closed S"
is Elementary_Topology.frontier_subset_eq.
tts_lemma frontier_complement:
assumes "S ⊆ U"
shows "frontier (- S ∩ U) = frontier S"
is Elementary_Topology.frontier_complement.
tts_lemma frontier_Un_subset:
assumes "S ⊆ U" and "T ⊆ U"
shows "frontier (S ∪ T) ⊆ frontier S ∪ frontier T"
is Elementary_Topology.frontier_Un_subset.
tts_lemma frontier_disjoint_eq:
assumes "S ⊆ U"
shows "(frontier S ∩ S = {}) = τ S"
is Elementary_Topology.frontier_disjoint_eq.
tts_lemma frontier_interiors:
assumes "s ⊆ U"
shows "frontier s = - interior s ∩ U - interior (- s ∩ U)"
is Elementary_Topology.frontier_interiors.
tts_lemma frontier_interior_subset:
assumes "S ⊆ U"
shows "frontier (interior S) ⊆ frontier S"
is Elementary_Topology.frontier_interior_subset.
tts_lemma compact_Un:
assumes "s ⊆ U" and "t ⊆ U" and "compact s" and "compact t"
shows "compact (s ∪ t)"
is Elementary_Topology.compact_Un.
tts_lemma closed_Int_compact:
assumes "s ⊆ U" and "t ⊆ U" and "closed s" and "compact t"
shows "compact (s ∩ t)"
is Elementary_Topology.closed_Int_compact.
tts_lemma countably_compact_imp_compact:
assumes "U ⊆ U"
and "B ⊆ Pow U"
and "countably_compact U"
and "countable B"
and "Ball B τ"
and "⋀T x. ⟦T ⊆ U; x ∈ U; τ T; x ∈ T; x ∈ U⟧ ⟹ ∃y∈B. x ∈ y ∧ y ∩ U ⊆ T"
shows "compact U"
is Elementary_Topology.countably_compact_imp_compact.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› through (insert closure_eq_empty, blast)
begin
tts_lemma closure_interior:
assumes "S ⊆ U"
shows "closure S = - interior (- S ∩ U) ∩ U"
is Elementary_Topology.closure_interior.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}›
through (insert compact_empty, fastforce dest: subset_singletonD)
begin
tts_lemma compact_Union:
assumes "S ⊆ Pow U"
and "finite S"
and "⋀T. ⟦T ⊆ U; T ∈ S⟧ ⟹ compact T"
shows "compact (⋃ S)"
is Elementary_Topology.compact_Union.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› through
(
insert
interior_empty
closure_ow_def
closed_UNIV
compact_empty
compact_ow_def,
auto
)
begin
tts_lemma compactI:
assumes "s ⊆ U"
and "⋀C. ⟦C ⊆ Pow U; Ball C τ; s ⊆ ⋃ C⟧ ⟹
∃x⊆Pow U. x ⊆ C ∧ finite x ∧ s ⊆ ⋃ x"
shows "compact s"
given topological_space_class.compactI by (meson PowI)
tts_lemma compactE:
assumes "S ⊆ U"
and "𝒯 ⊆ Pow U"
and "compact S"
and "S ⊆ ⋃ 𝒯"
and "⋀B. B ∈ 𝒯 ⟹ τ B"
and "⋀𝒯'. ⟦𝒯' ⊆ Pow U; 𝒯' ⊆ 𝒯; finite 𝒯'; S ⊆ ⋃ 𝒯'⟧ ⟹ thesis"
shows thesis
given topological_space_class.compactE
by metis
tts_lemma compact_fip:
assumes "U ⊆ U"
shows "compact U =
(
∀x⊆Pow U.
Ball x closed ⟶
(∀y⊆Pow U. y ⊆ x ⟶ finite y ⟶ U ∩ (⋂ y ∩ U) ≠ {}) ⟶
U ∩ (⋂ x ∩ U) ≠ {}
)"
given topological_space_class.compact_fip by auto
tts_lemma compact_imp_fip:
assumes "S ⊆ U"
and "Fa ⊆ Pow U"
and "compact S"
and "⋀T. ⟦T ⊆ U; T ∈ Fa⟧ ⟹ closed T"
and "⋀F'. ⟦F' ⊆ Pow U; finite F'; F' ⊆ Fa⟧ ⟹ S ∩ (⋂ F' ∩ U) ≠ {}"
shows "S ∩ (⋂ Fa ∩ U) ≠ {}"
is topological_space_class.compact_imp_fip.
tts_lemma closed_limpt:
assumes "S ⊆ U"
shows "closed S = (∀x∈U. x «islimpt» S ⟶ x ∈ S)"
is Elementary_Topology.closed_limpt.
tts_lemma open_interior:
assumes "S ⊆ U"
shows "τ (interior S)"
is Elementary_Topology.open_interior.
tts_lemma interior_subset:
assumes "S ⊆ U"
shows "interior S ⊆ S"
is Elementary_Topology.interior_subset.
tts_lemma interior_open:
assumes "S ⊆ U" and "τ S"
shows "interior S = S"
is Elementary_Topology.interior_open.
tts_lemma interior_eq:
assumes "S ⊆ U"
shows "(interior S = S) = τ S"
is Elementary_Topology.interior_eq.
tts_lemma interior_UNIV: "interior U = U"
is Elementary_Topology.interior_UNIV.
tts_lemma interior_interior:
assumes "S ⊆ U"
shows "interior (interior S) = interior S"
is Elementary_Topology.interior_interior.
tts_lemma interior_closure:
assumes "S ⊆ U"
shows "interior S = - closure (- S ∩ U) ∩ U"
is Elementary_Topology.interior_closure.
tts_lemma finite_imp_compact:
assumes "s ⊆ U" and "finite s"
shows "compact s"
is Elementary_Topology.finite_imp_compact.
tts_lemma countably_compactE:
assumes "s ⊆ U"
and "C ⊆ Pow U"
and "countably_compact s"
and "Ball C τ"
and "s ⊆ ⋃ C"
and "countable C"
and "⋀C'. ⟦C' ⊆ Pow U; C' ⊆ C; finite C'; s ⊆ ⋃ C'⟧ ⟹ thesis"
shows thesis
is Elementary_Topology.countably_compactE.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› and ‹?A ⊆ U› through (insert interior_empty, auto)
begin
tts_lemma interior_unique:
assumes "S ⊆ U"
and "T ⊆ S"
and "τ T"
and "⋀T'. ⟦T' ⊆ S; τ T'⟧ ⟹ T' ⊆ T"
shows "interior S = T"
given Elementary_Topology.interior_unique
by auto
end
tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› through (simp add: subset_iff filterlim_iff)
begin
tts_lemma open_UN:
assumes "A ⊆ U⇩2"
and "∀x∈U⇩2. B x ⊆ U"
and "∀x∈A. τ (B x)"
shows "τ (⋃ (B ` A))"
is topological_space_class.open_UN.
tts_lemma open_Collect_ex:
assumes "⋀i. i ∈ U⇩2 ⟹ τ {x. P i x ∧ x ∈ U}"
shows "τ {x ∈ U. ∃i∈U⇩2. P i x}"
is open_Collect_ex.
end
tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› through (unfold closed_ow_def finite_def, auto)
begin
tts_lemma open_INT:
assumes "A ⊆ U⇩2" and "∀x∈U⇩2. B x ⊆ U" and "finite A" and "∀x∈A. τ (B x)"
shows "τ (⋂ (B ` A) ∩ U)"
is topological_space_class.open_INT.
tts_lemma closed_INT:
assumes "A ⊆ U⇩2" and "∀x∈U⇩2. B x ⊆ U" and "∀x∈A. closed (B x)"
shows "closed (⋂ (B ` A) ∩ U)"
is topological_space_class.closed_INT.
tts_lemma closed_UN:
assumes "A ⊆ U⇩2"
and "∀x∈U⇩2. B x ⊆ U"
and "finite A"
and "∀x∈A. closed (B x)"
shows "closed (⋃ (B ` A))"
is topological_space_class.closed_UN.
end
tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› through (insert closed_empty, auto)
begin
tts_lemma closed_Collect_all:
assumes "⋀i. i ∈ U⇩2 ⟹ local.closed {x. P i x ∧ x ∈ U}"
shows "local.closed {x ∈ U. ∀i∈U⇩2. P i x}"
is topological_space_class.closed_Collect_all.
tts_lemma compactE_image:
assumes "S ⊆ U"
and "C ⊆ U⇩2"
and "∀x∈U⇩2. f x ⊆ U"
and "compact S"
and "⋀T. ⟦T ∈ U⇩2; T ∈ C⟧ ⟹ τ (f T)"
and "S ⊆ ⋃ (f ` C)"
and "⋀C'. ⟦C' ⊆ U⇩2; C' ⊆ C; finite C'; S ⊆ ⋃ (f ` C')⟧ ⟹ thesis"
shows thesis
is topological_space_class.compactE_image.
end
tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting topological_space_ow_axioms
eliminating ‹?U ≠ {}› through (simp, blast | simp)
begin
tts_lemma ne_compact_imp_fip_image:
assumes "s ⊆ U"
and "I ⊆ U⇩2"
and "∀x∈U⇩2. f x ⊆ U"
and "compact s"
and "⋀i. ⟦i ∈ U⇩2; i ∈ I⟧ ⟹ closed (f i)"
and "⋀I'. ⟦I' ⊆ U⇩2; finite I'; I' ⊆ I⟧ ⟹ s ∩ (⋂ (f ` I') ∩ U) ≠ {}"
shows "s ∩ (⋂ (f ` I) ∩ U) ≠ {}"
is topological_space_class.compact_imp_fip_image.
end
end
subsection‹Further results›
lemma topological_basis_closed:
assumes "topological_basis_ow U τ B"
shows "B ⊆ Pow U"
using assms unfolding topological_basis_ow_def by auto
lemma ts_open_eq_ts_open:
assumes "topological_space_ow U τ'" and "⋀s. s ⊆ U ⟹ τ' s = τ s"
shows "topological_space_ow U τ"
proof
from assms(1) have "τ' U" unfolding topological_space_ow_def by simp
with assms(2) show "τ U" by auto
from assms(1) have "⋀S T. ⟦ S ⊆ U; T ⊆ U; τ' S; τ' T ⟧ ⟹ τ' (S ∩ T)"
unfolding topological_space_ow_def by simp
with assms(2) show "⋀S T. ⟦ S ⊆ U; T ⊆ U; τ S; τ T ⟧ ⟹ τ (S ∩ T)"
by (meson Int_lower1 order_trans)
from assms(1) have "⋀K. ⟦ K ⊆ Pow U; ∀S∈K. τ' S ⟧ ⟹ τ' (⋃K)"
unfolding topological_space_ow_def by simp
with assms(2) show "⋀K. ⟦ K ⊆ Pow U; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)"
by (metis Union_Pow_eq Union_mono ctr_simps_subset_pow_iff)
qed
lemma (in topological_space_ow) topological_basis_closed:
assumes "topological_basis_ow U τ B"
shows "B ⊆ Pow U"
using assms
unfolding topological_basis_with_def
by (rule topological_basis_closed)
text‹\newpage›
end