# Theory SML_Ordered_Topological_Spaces

```(* Title: Examples/SML_Relativization/Topology/SML_Ordered_Topological_Spaces.thy
Author: Mihails Milehins
*)
section‹Relativization of the results about ordered topological spaces›
theory SML_Ordered_Topological_Spaces
imports
SML_Topological_Space
"../Lattices/SML_Linorders"
begin

subsection‹Ordered topological space›

subsubsection‹Definitions and common properties›

locale order_topology_ow =
order_ow U le ls for U :: "'at set" and le ls +
fixes τ :: "'at set ⇒ bool"
assumes open_generated_order: "s ⊆ U ⟹
τ s =
(
(
in_topology_generated_by
(
(λa. (on U with (<⇩o⇩w) : {..< a})) ` U ∪
(λa. (on U with (<⇩o⇩w) : {a <..})) ` U
)
on U : «open» s
)
)"
begin

sublocale topological_space_ow
proof -
define τ' where τ':
"τ' = generate_topology_on
(
(λa. (on U with (<⇩o⇩w) : {..< a})) ` U ∪
(λa. (on U with (<⇩o⇩w) : {a <..})) ` U
)
U"
have
"(
(λa. (on U with (<⇩o⇩w) : {..< a})) ` U ∪
(λa. (on U with (<⇩o⇩w) : {a <..})) ` U
) ⊆ Pow U"
unfolding lessThan_def greaterThan_def lessThan_ow_def greaterThan_ow_def
by auto
then have "topological_space_ow U τ'"
unfolding τ' by (simp add: topological_space_generate_topology)
moreover then have "s ⊆ U ⟹ τ' s = τ s" for s
unfolding τ' using open_generated_order by blast
ultimately show "topological_space_ow U τ"
unfolding τ' by (rule ts_open_eq_ts_open)
qed

end

locale ts_ot_ow =
ts: topological_space_ow U⇩1 τ⇩1 + ot: order_topology_ow U⇩2 le⇩2 ls⇩2 τ⇩2
for U⇩1 :: "'at set" and τ⇩1 and U⇩2 :: "'bt set" and le⇩2 ls⇩2 τ⇩2
begin

sublocale topological_space_pair_ow U⇩1 τ⇩1 U⇩2 τ⇩2 ..

end

locale order_topology_pair_ow =
ot⇩1: order_topology_ow U⇩1 le⇩1 ls⇩1 τ⇩1 + ot⇩2: order_topology_ow U⇩2 le⇩2 ls⇩2 τ⇩2
for U⇩1 :: "'at set" and le⇩1 ls⇩1 τ⇩1 and U⇩2 :: "'bt set" and le⇩2 ls⇩2 τ⇩2
begin

sublocale ts_ot_ow U⇩1 τ⇩1 U⇩2 le⇩2 ls⇩2 τ⇩2 ..

end

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

lemma order_topology_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"(
(A ===> A ===> (=)) ===>
(A ===> A ===> (=)) ===>
(rel_set A ===> (=)) ===>
(=)
) (order_topology_ow (Collect (Domainp A))) class.order_topology"
unfolding order_topology_ow_def class.order_topology_def
unfolding order_topology_ow_axioms_def class.order_topology_axioms_def
proof(intro rel_funI, standard; elim conjE)
let ?U = "Collect (Domainp A)"
fix le :: "['a, 'a] ⇒ bool"
and le' :: "['b, 'b] ⇒ bool"
and ls :: "['a, 'a] ⇒ bool"
and ls' :: "['b, 'b] ⇒ bool"
and τ :: "'a set ⇒ bool"
and τ' :: "'b set ⇒ bool"
assume [transfer_rule]: "(A ===> A ===> (=)) le le'"
and [transfer_rule]: "(A ===> A ===> (=)) ls ls'"
and [transfer_rule]: "(rel_set A ===> (=)) τ τ'"
and oow: "order_ow (Collect (Domainp A)) le ls"
and τ:
"∀s⊆Collect (Domainp A). τ s =
generate_topology_on
(lessThan_ow ?U ls ` ?U ∪ greaterThan_ow ?U ls ` ?U) ?U s"
have [transfer_rule]: "Domainp A = (λx. x ∈ Collect (Domainp A))" by auto
interpret oow: order_ow ?U le ls by (rule oow)
interpret co: order le' ls' by transfer (rule oow)
have ineq_fold:
"lessThan.with ls y ≡ {x. ls x y}"
"greaterThan.with ls y ≡ {x. ls y x}"
for ls :: "'c ⇒ 'c ⇒ bool" and y
unfolding lessThan.with_def greaterThan.with_def by auto
have
"τ' = generate_topology (
range (ord.lessThan ls') ∪ range (ord.greaterThan ls')
)"
unfolding co.lessThan_def co.greaterThan_def
unfolding ineq_fold[symmetric]
by (transfer, intro allI impI) (auto simp: τ)
from co.order_axioms this show
"class.order le' ls' ∧
τ' = generate_topology (
range (ord.lessThan ls') ∪ range (ord.greaterThan ls')
)"
by simp
next
let ?U = "Collect (Domainp A)"
fix le :: "['a, 'a] ⇒ bool"
and le' :: "['b, 'b] ⇒ bool"
and ls :: "['a, 'a] ⇒ bool"
and ls' :: "['b, 'b] ⇒ bool"
and τ :: "'a set ⇒ bool"
and τ' :: "'b set ⇒ bool"
assume [transfer_rule]: "(A ===> A ===> (=)) le le'"
and [transfer_rule]: "(A ===> A ===> (=)) ls ls'"
and [transfer_rule]: "(rel_set A ===> (=)) τ τ'"
and co: "class.order le' ls'"
and τ': "τ' = generate_topology
(range (ord.lessThan ls') ∪ range (ord.greaterThan ls'))"
have [transfer_rule]: "Domainp A = (λx. x ∈ Collect (Domainp A))" by auto
interpret co: order le' ls' by (rule co)
have ineq_fold:
"lessThan.with ls y ≡ {x. ls x y}"
"greaterThan.with ls y ≡ {x. ls y x}"
for ls :: "'c ⇒ 'c ⇒ bool" and y
unfolding lessThan.with_def greaterThan.with_def by auto
from co have "order_ow ?U le ls" by transfer
moreover have
"∀s⊆Collect (Domainp A). τ s =
SML_Topological_Space.generate_topology_on
(lessThan_ow ?U ls ` ?U ∪ greaterThan_ow ?U ls ` ?U) ?U s"
by
(
rule τ'[
unfolded co.lessThan_def co.greaterThan_def,
folded ineq_fold,
untransferred
]
)
ultimately show
"order_ow ?U le ls ∧
(
∀s⊆Collect (Domainp A). τ s =
SML_Topological_Space.generate_topology_on
(lessThan_ow ?U ls ` ?U ∪ greaterThan_ow ?U ls ` ?U) ?U s
)"
by simp
qed

end

subsubsection‹Relativization›

context order_topology_ow
begin

tts_context
tts: (?'a to U)
substituting order_topology_ow_axioms
eliminating ‹?U ≠ {}› through simp
begin

tts_lemma open_greaterThan:
assumes "a ∈ U"
shows "τ {a<⇩o⇩w..}"
is order_topology_class.open_greaterThan.

tts_lemma open_lessThan:
assumes "a ∈ U"
shows "τ {..<⇩o⇩wa}"
is order_topology_class.open_lessThan.

tts_lemma open_greaterThanLessThan:
assumes "a ∈ U" and "b ∈ U"
shows "τ {a<⇩o⇩w..<⇩o⇩wb}"
is order_topology_class.open_greaterThanLessThan.

end

end

subsection‹Linearly ordered topological space›

subsubsection‹Definitions and common properties›

locale linorder_topology_ow =
linorder_ow U le ls + order_topology_ow U le ls τ
for U :: "'at set" and le ls τ

locale ts_lt_ow =
ts: topological_space_ow U⇩1 τ⇩1 + lt: linorder_topology_ow U⇩2 le⇩2 ls⇩2 τ⇩2
for U⇩1 :: "'at set" and τ⇩1 and U⇩2 :: "'bt set" and le⇩2 ls⇩2 τ⇩2
begin

sublocale ts_ot_ow U⇩1 τ⇩1 U⇩2 le⇩2 ls⇩2 τ⇩2 ..

end

locale ot_lt_ow =
ot: order_topology_ow U⇩1 le⇩1 ls⇩1 τ⇩1 + lt: linorder_topology_ow U⇩2 le⇩2 ls⇩2 τ⇩2
for U⇩1 :: "'at set" and le⇩1 ls⇩1 τ⇩1 and U⇩2 :: "'bt set" and le⇩2 ls⇩2 τ⇩2
begin

sublocale ts_lt_ow U⇩1 τ⇩1 U⇩2 le⇩2 ls⇩2 τ⇩2 ..
sublocale order_topology_pair_ow U⇩1 le⇩1 ls⇩1 τ⇩1 U⇩2 le⇩2 ls⇩2 τ⇩2 ..

end

locale linorder_topology_pair_ow =
lt⇩1: linorder_topology_ow U⇩1 le⇩1 ls⇩1 τ⇩1 + lt⇩2: linorder_topology_ow U⇩2 le⇩2 ls⇩2 τ⇩2
for U⇩1 :: "'at set" and le⇩1 ls⇩1 τ⇩1 and U⇩2 :: "'bt set" and le⇩2 ls⇩2 τ⇩2
begin

sublocale ot_lt_ow U⇩1 le⇩1 ls⇩1 τ⇩1 U⇩2 le⇩2 ls⇩2 τ⇩2 ..

end

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

lemma linorder_topology_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"(
(A ===> A ===> (=)) ===>
(A ===> A ===> (=)) ===>
(rel_set A ===> (=)) ===>
(=)
)
(linorder_topology_ow (Collect (Domainp A))) class.linorder_topology"
unfolding linorder_topology_ow_def class.linorder_topology_def
by transfer_prover

end

subsubsection‹Relativization›

context linorder_topology_ow
begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting linorder_topology_ow_axioms
eliminating ‹?U ≠ {}› through clarsimp
begin

tts_lemma open_right:
assumes "S ⊆ U"
and "x ∈ U"
and "y ∈ U"
and "τ S"
and "x ∈ S"
and "x <⇩o⇩w y"
shows "∃z∈U. x <⇩o⇩w z ∧ (on U with (≤⇩o⇩w) (<⇩o⇩w) : {x..<z}) ⊆ S"
is linorder_topology_class.open_right.

tts_lemma open_left:
assumes "S ⊆ U"
and "x ∈ U"
and "y ∈ U"
and "τ S"
and "x ∈ S"
and "y <⇩o⇩w x"
shows "∃z∈U. z <⇩o⇩w x ∧ {z<⇩o⇩w..x} ⊆ S"
is linorder_topology_class.open_left.

tts_lemma connectedD_interval:
assumes "U ⊆ U"
and "x ∈ U"
and "y ∈ U"
and "z ∈ U"
and "connected U"
and "x ∈ U"
and "y ∈ U"
and "x ≤⇩o⇩w z"
and "z ≤⇩o⇩w y"
shows "z ∈ U"
is linorder_topology_class.connectedD_interval.

tts_lemma connected_contains_Icc:
assumes "A ⊆ U"
and "a ∈ U"
and "b ∈ U"
and "connected A"
and "a ∈ A"
and "b ∈ A"
shows "{a..⇩o⇩wb} ⊆ A"
is Topological_Spaces.connected_contains_Icc.

tts_lemma connected_contains_Ioo:
assumes "A ⊆ U"
and "a ∈ U"
and "b ∈ U"
and "connected A"
and "a ∈ A"
and "b ∈ A"
shows "{a<⇩o⇩w..<⇩o⇩wb} ⊆ A"
is Topological_Spaces.connected_contains_Ioo.

end

tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting linorder_topology_ow_axioms
eliminating ‹?U ≠ {}› through clarsimp
begin

tts_lemma not_in_connected_cases:
assumes "S ⊆ U"
and "x ∈ U"
and "connected S"
and "x ∉ S"
and "S ≠ {}"
and "⟦bdd_above S; ⋀y. ⟦y ∈ U; y ∈ S⟧ ⟹ y ≤⇩o⇩w x⟧ ⟹ thesis"
and "⟦bdd_below S; ⋀y. ⟦y ∈ U; y ∈ S⟧ ⟹ x ≤⇩o⇩w y⟧ ⟹ thesis"
shows thesis
is linorder_topology_class.not_in_connected_cases.

tts_lemma compact_attains_sup:
assumes "S ⊆ U"
and "compact S"
and "S ≠ {}"
shows "∃x∈S. ∀y∈S. y ≤⇩o⇩w x"
is linorder_topology_class.compact_attains_sup.

tts_lemma compact_attains_inf:
assumes "S ⊆ U"
and "compact S"
and "S ≠ {}"
shows "∃x∈S. Ball S ((≤⇩o⇩w) x)"
is linorder_topology_class.compact_attains_inf.

end

end

text‹\newpage›

end```