Theory SML_Topological_Space_Countability
section‹
Relativization of the results related to the countability properties of
topological spaces
›
theory SML_Topological_Space_Countability
imports SML_Topological_Space
begin
subsection‹First countable topological space›
subsubsection‹Definitions and common properties›
locale first_countable_topology_ow =
topological_space_ow U τ for U :: "'at set" and τ +
assumes first_countable_basis:
"(
∀x∈U.
(
∃B::nat ⇒ 'at set.
(∀i. B i ⊆ U ∧ x ∈ B i ∧ τ (B i)) ∧
(∀S. S ⊆ U ∧ τ S ∧ x ∈ S ⟶ (∃i. B i ⊆ S))
)
)"
locale ts_fct_ow =
ts: topological_space_ow U⇩1 τ⇩1 + fct: first_countable_topology_ow U⇩2 τ⇩2
for U⇩1 :: "'at set" and τ⇩1 and U⇩2 :: "'bt set" and τ⇩2
begin
sublocale topological_space_pair_ow U⇩1 τ⇩1 U⇩2 τ⇩2 ..
end
locale first_countable_topology_pair_ow =
fct⇩1: first_countable_topology_ow U⇩1 τ⇩1 +
fct⇩2: first_countable_topology_ow U⇩2 τ⇩2
for U⇩1 :: "'at set" and τ⇩1 and U⇩2 :: "'bt set" and τ⇩2
begin
sublocale ts_fct_ow U⇩1 τ⇩1 U⇩2 τ⇩2 ..
end
subsubsection‹Transfer rules›
context
includes lifting_syntax
begin
private lemma first_countable_topology_transfer_h:
"(∀i. B i ⊆ Collect (Domainp A) ∧ x ∈ B i ∧ τ (B i)) =
(B ` Collect top ⊆ {Aa. Aa ⊆ Collect (Domainp A)} ∧
(∀i. x ∈ B i ∧ τ (B i)))"
by auto
lemma first_countable_topology_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((rel_set A ===> (=)) ===> (=))
(first_countable_topology_ow (Collect (Domainp A)))
class.first_countable_topology"
unfolding
first_countable_topology_ow_def
class.first_countable_topology_def
first_countable_topology_ow_axioms_def
class.first_countable_topology_axioms_def
apply transfer_prover_start
apply transfer_step+
by
(
simp,
unfold Ball_Collect,
intro ext,
unfold first_countable_topology_transfer_h
)
(metis top_set_def)
end
subsubsection‹Relativization›
context first_countable_topology_ow
begin
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting first_countable_topology_ow_axioms
eliminating ‹?U ≠ {}› through simp
begin
tts_lemma countable_basis_at_decseq:
assumes "x ∈ U"
and "⋀A.
⟦
range A ⊆ Pow U;
⋀i. τ (A i);
⋀i. x ∈ A i;
⋀S. ⟦S ⊆ U; τ S; x ∈ S⟧ ⟹ ∀⇩F i in sequentially. A i ⊆ S
⟧ ⟹ thesis"
shows thesis
is first_countable_topology_class.countable_basis_at_decseq.
tts_lemma first_countable_basisE:
assumes "x ∈ U"
and "⋀𝒜.
⟦
𝒜 ⊆ Pow U;
countable 𝒜;
⋀A. ⟦A ⊆ U; A ∈ 𝒜⟧ ⟹ x ∈ A;
⋀A. ⟦A ⊆ U; A ∈ 𝒜⟧ ⟹ τ A;
⋀S. ⟦S ⊆ U; τ S; x ∈ S⟧ ⟹ ∃A∈𝒜. A ⊆ S⟧ ⟹ thesis"
shows thesis
is first_countable_topology_class.first_countable_basisE.
tts_lemma first_countable_basis_Int_stableE:
assumes "x ∈ U"
and "⋀𝒜.
⟦
𝒜 ⊆ Pow U;
countable 𝒜;
⋀A. ⟦A ⊆ U; A ∈ 𝒜⟧ ⟹ x ∈ A;
⋀A. ⟦A ⊆ U; A ∈ 𝒜⟧ ⟹ τ A;
⋀S. ⟦S ⊆ U; τ S; x ∈ S⟧ ⟹ ∃A∈𝒜. A ⊆ S;
⋀A B. ⟦A ⊆ U; B ⊆ U; A ∈ 𝒜; B ∈ 𝒜⟧ ⟹ A ∩ B ∈ 𝒜
⟧ ⟹ thesis"
shows thesis
is first_countable_topology_class.first_countable_basis_Int_stableE.
end
end
subsection‹Topological space with a countable basis›
subsubsection‹Definitions and common properties›
locale countable_basis_ow =
topological_space_ow U τ for U :: "'at set" and τ +
fixes B :: "'at set set"
assumes is_basis: "topological_basis_ow U τ B"
and countable_basis: "countable B"
begin
lemma B_ss_PowU[simp]: "B ⊆ Pow U"
by (simp add: is_basis topological_basis_closed)
end
subsubsection‹Transfer rules›
context
includes lifting_syntax
begin
lemma countable_basis_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((rel_set A ===> (=)) ===> rel_set (rel_set A) ===> (=))
(countable_basis_ow (Collect (Domainp A))) countable_basis"
proof(intro rel_funI)
fix τ :: "'a set ⇒ bool" and τ' :: "'b set ⇒ bool" and B B'
assume ττ'[transfer_rule]: "(rel_set A ===> (=)) τ τ'"
and BB'[transfer_rule]: "rel_set (rel_set A) B B'"
show "countable_basis_ow (Collect (Domainp A)) τ B = countable_basis τ' B'"
proof
assume cbow: "countable_basis_ow (Collect (Domainp A)) τ B"
interpret cbow: countable_basis_ow "Collect (Domainp A)" τ B by (rule cbow)
interpret ts: topological_space τ'
by transfer (simp add: cbow.topological_space_ow_axioms)
show "countable_basis τ' B'"
apply unfold_locales
subgoal
using cbow.is_basis unfolding ts.topological_basis_with by transfer
subgoal using cbow.countable_basis by transfer
done
next
assume cb: "countable_basis τ' B'"
interpret cb: countable_basis τ' B' by (rule cb)
interpret tsow: topological_space_ow "Collect (Domainp A)" τ
using cb.topological_space_axioms by transfer
show "countable_basis_ow (Collect (Domainp A)) τ B"
apply unfold_locales
subgoal using cb.is_basis unfolding cb.topological_basis_with by transfer
subgoal using cb.countable_basis by transfer
done
qed
qed
end
subsubsection‹Relativization›
context countable_basis_ow
begin
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting countable_basis_ow_axioms
eliminating ‹?U ≠ {}› through auto
applying [OF B_ss_PowU]
begin
tts_lemma open_countable_basis_ex:
assumes "X ⊆ U" and "τ X"
shows "∃B'∈Pow (Pow U). B' ⊆ B ∧ X = ⋃ B'"
is countable_basis.open_countable_basis_ex.
tts_lemma countable_dense_exists:
"∃D∈Pow U.
countable D ∧
(∀X∈Pow U. τ X ⟶ X ≠ {} ⟶ (∃d∈D. d ∈ X))"
is countable_basis.countable_dense_exists.
tts_lemma open_countable_basisE:
assumes "X ⊆ U"
and "τ X"
and "⋀B'. ⟦B' ⊆ Pow U; B' ⊆ B; X = ⋃ B'⟧ ⟹ thesis"
shows thesis
is countable_basis.open_countable_basisE.
tts_lemma countable_dense_setE:
assumes "⋀D.
⟦D ⊆ U; countable D; ⋀X. ⟦X ⊆ U; τ X; X ≠ {}⟧ ⟹ ∃x∈D. x ∈ X⟧ ⟹ thesis"
shows thesis
is countable_basis.countable_dense_setE.
end
end
subsection‹Second countable topological space›
subsubsection‹Definitions and common properties›
locale second_countable_topology_ow =
topological_space_ow U τ for U :: "'at set" and τ +
assumes second_countable_basis:
"∃B⊆Pow U. countable B ∧ (∀S⊆U. τ S = generate_topology_on B U S)"
subsubsection‹Transfer rules›
context
includes lifting_syntax
begin
lemma second_countable_topology_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((rel_set A ===> (=)) ===> (=))
(second_countable_topology_ow (Collect (Domainp A)))
class.second_countable_topology"
unfolding
second_countable_topology_ow_def
class.second_countable_topology_def
second_countable_topology_ow_axioms_def
class.second_countable_topology_axioms_def
apply transfer_prover_start
apply transfer_step+
unfolding Ball_Collect ctr_simps_subset_pow_iff''[symmetric]
by simp
end
subsubsection‹Relativization›
context second_countable_topology_ow
begin
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting second_countable_topology_ow_axioms
eliminating ‹?U ≠ {}› through (unfold topological_basis_ow_def, auto)
begin
tts_lemma ex_countable_basis:
"∃B∈Pow (Pow U). countable B ∧ (on U with τ : «topological_basis» B)"
is Elementary_Topology.ex_countable_basis.
end
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting second_countable_topology_ow_axioms
eliminating ‹?U ≠ {}› through (auto simp: countable_subset)
begin
tts_lemma countable_dense_exists:
"∃D∈Pow U. countable D ∧ (∀X∈Pow U. τ X ⟶ X ≠ {} ⟶ (∃d∈D. d ∈ X))"
is Elementary_Topology.countable_dense_exists.
tts_lemma countable_dense_setE:
assumes "⋀D.
⟦
D ⊆ U;
countable D;
⋀X. ⟦X ⊆ U; τ X; X ≠ {}⟧ ⟹ ∃d∈D. d ∈ X
⟧ ⟹ thesis"
shows thesis
is Elementary_Topology.countable_dense_setE.
tts_lemma univ_second_countable:
assumes "⋀ℬ.
⟦
ℬ ⊆ Pow U;
countable ℬ;
⋀C. ⟦C ⊆ U; C ∈ ℬ⟧ ⟹ τ C;
⋀S. ⟦S ⊆ U; τ S⟧ ⟹ ∃U∈Pow (Pow U). U ⊆ ℬ ∧ S = ⋃ U
⟧ ⟹ thesis"
shows thesis
is Elementary_Topology.univ_second_countable.
tts_lemma Lindelof:
assumes "ℱ ⊆ Pow U"
and "⋀S. ⟦S ⊆ U; S ∈ ℱ⟧ ⟹ τ S"
and "⋀ℱ'. ⟦ℱ' ⊆ Pow U; ℱ' ⊆ ℱ; countable ℱ'; ⋃ ℱ' = ⋃ ℱ⟧ ⟹ thesis"
shows thesis
is Elementary_Topology.Lindelof.
tts_lemma countable_disjoint_open_subsets:
assumes "ℱ ⊆ Pow U" and "⋀S. ⟦S ⊆ U; S ∈ ℱ⟧ ⟹ τ S" and "disjoint ℱ"
shows "countable ℱ"
is Elementary_Topology.countable_disjoint_open_subsets.
end
end
text‹\newpage›
end