QuantumLib.Ctopology
Require Export Polynomial.
Require Import Setoid.
Declare Scope topology_scope.
Delimit Scope topology_scope with T.
Open Scope topology_scope.
Definition Cset := C → Prop.
Definition union (A B : Cset) : Cset :=
fun c ⇒ A c ∨ B c.
Definition intersection (A B : Cset) : Cset :=
fun c ⇒ A c ∧ B c.
Definition complement (A : Cset) : Cset :=
fun c ⇒ not (A c).
Definition setminus (A B : Cset) : Cset :=
intersection A (complement B).
Definition is_in (a : C) (A : Cset) : Prop := A a.
Definition subset (A B : Cset) : Prop :=
∀ c, A c → B c.
Definition eq_set (A B : Cset) : Prop :=
∀ c, A c ↔ B c.
Definition ϵ_disk (a : C) (ϵ : R) : Cset :=
fun c ⇒ Cmod (c - a) < ϵ.
Definition open_square (cen : C) (s : R) : Cset :=
fun c ⇒ Rabs (fst c - fst cen) < s ∧ Rabs (snd c - snd cen) < s.
Definition open_rect (cen : C) (s1 s2 : R) : Cset :=
fun c ⇒ Rabs (fst c - fst cen) < s1 ∧ Rabs (snd c - snd cen) < s2.
Definition bounded (A : Cset) : Prop :=
∃ ϵ, subset A (ϵ_disk C0 ϵ).
Definition image (f : C → C) (A : Cset) : Cset :=
fun c ⇒ (∃ c', A c' ∧ f c' = c).
Definition preimage (f : C → C) (B : Cset) : Cset :=
fun c ⇒ B (f c).
Definition continuous_on (f : C → C) (A : Cset) : Prop :=
∀ c, A c → continuous_at f c.
Infix "∪" := union (at level 50, left associativity) : topology_scope.
Infix "∩" := intersection (at level 40, left associativity) : topology_scope.
Infix "⊂" := subset (at level 0) : topology_scope.
Infix "⩦" := eq_set (at level 0) : topology_scope.
Infix "\" := setminus (at level 0) : topology_scope.
Infix "@" := image (at level 0) : topology_scope.
Notation "f *{ A }" := (preimage f A) (at level 0) : topology_scope.
Notation "A `" := (complement A) (at level 0) : topology_scope.
Infix "∈" := is_in (at level 0) : topology_scope.
Notation "B( a , ϵ )" := (ϵ_disk a ϵ) (at level 30, no associativity) : topology_scope.
Definition open (A : Cset) : Prop :=
∀ c, A c → ∃ ϵ, ϵ > 0 ∧ B(c,ϵ) ⊂ A.
Definition closed (A : Cset) : Prop :=
open (A`).
Definition empty_set : Cset :=
fun _ ⇒ False.
Definition C_ : Cset :=
fun _ ⇒ True.
Require Import Setoid.
Declare Scope topology_scope.
Delimit Scope topology_scope with T.
Open Scope topology_scope.
Definition Cset := C → Prop.
Definition union (A B : Cset) : Cset :=
fun c ⇒ A c ∨ B c.
Definition intersection (A B : Cset) : Cset :=
fun c ⇒ A c ∧ B c.
Definition complement (A : Cset) : Cset :=
fun c ⇒ not (A c).
Definition setminus (A B : Cset) : Cset :=
intersection A (complement B).
Definition is_in (a : C) (A : Cset) : Prop := A a.
Definition subset (A B : Cset) : Prop :=
∀ c, A c → B c.
Definition eq_set (A B : Cset) : Prop :=
∀ c, A c ↔ B c.
Definition ϵ_disk (a : C) (ϵ : R) : Cset :=
fun c ⇒ Cmod (c - a) < ϵ.
Definition open_square (cen : C) (s : R) : Cset :=
fun c ⇒ Rabs (fst c - fst cen) < s ∧ Rabs (snd c - snd cen) < s.
Definition open_rect (cen : C) (s1 s2 : R) : Cset :=
fun c ⇒ Rabs (fst c - fst cen) < s1 ∧ Rabs (snd c - snd cen) < s2.
Definition bounded (A : Cset) : Prop :=
∃ ϵ, subset A (ϵ_disk C0 ϵ).
Definition image (f : C → C) (A : Cset) : Cset :=
fun c ⇒ (∃ c', A c' ∧ f c' = c).
Definition preimage (f : C → C) (B : Cset) : Cset :=
fun c ⇒ B (f c).
Definition continuous_on (f : C → C) (A : Cset) : Prop :=
∀ c, A c → continuous_at f c.
Infix "∪" := union (at level 50, left associativity) : topology_scope.
Infix "∩" := intersection (at level 40, left associativity) : topology_scope.
Infix "⊂" := subset (at level 0) : topology_scope.
Infix "⩦" := eq_set (at level 0) : topology_scope.
Infix "\" := setminus (at level 0) : topology_scope.
Infix "@" := image (at level 0) : topology_scope.
Notation "f *{ A }" := (preimage f A) (at level 0) : topology_scope.
Notation "A `" := (complement A) (at level 0) : topology_scope.
Infix "∈" := is_in (at level 0) : topology_scope.
Notation "B( a , ϵ )" := (ϵ_disk a ϵ) (at level 30, no associativity) : topology_scope.
Definition open (A : Cset) : Prop :=
∀ c, A c → ∃ ϵ, ϵ > 0 ∧ B(c,ϵ) ⊂ A.
Definition closed (A : Cset) : Prop :=
open (A`).
Definition empty_set : Cset :=
fun _ ⇒ False.
Definition C_ : Cset :=
fun _ ⇒ True.
showing that all the above def's are preserved by eq_set
Lemma eq_set_refl : ∀ (A : Cset), A ⩦ A.
Lemma eq_set_symm : ∀ (A B : Cset), A ⩦ B → B ⩦ A.
Lemma eq_set_trans : ∀ (A B C : Cset),
A ⩦ B → B ⩦ C → A ⩦ C.
Add Parametric Relation : Cset eq_set
reflexivity proved by eq_set_refl
symmetry proved by eq_set_symm
transitivity proved by eq_set_trans
as eq_set_equiv_rel.
Add Parametric Morphism : subset
with signature eq_set ==> eq_set ==> iff as subset_mor.
Add Parametric Morphism : union
with signature eq_set ==> eq_set ==> eq_set as union_mor.
Add Parametric Morphism : intersection
with signature eq_set ==> eq_set ==> eq_set as intersection_mor.
Add Parametric Morphism : bounded
with signature eq_set ==> iff as bounded_mor.
Add Parametric Morphism : open
with signature eq_set ==> iff as open_mor.
Lemma Cmod_lt_helper : ∀ (c : C) (ϵ : R),
Cmod c < ϵ → Rabs (fst c) < ϵ ∧ Rabs (snd c) < ϵ.
Subset lemmas
Lemma subset_cup_l : ∀ (A B : Cset),
A ⊂ (A ∪ B).
Lemma subset_cup_r : ∀ (A B : Cset),
B ⊂ (A ∪ B).
Lemma subset_cap_l : ∀ (A B : Cset),
(A ∩ B) ⊂ A.
Lemma subset_cap_r : ∀ (A B : Cset),
(A ∩ B) ⊂ B.
Lemma subset_self : ∀ (A : Cset),
A ⊂ A.
Lemma subset_transitive : ∀ (A B C : Cset),
A ⊂ B → B ⊂ C → A ⊂ C.
#[global] Hint Resolve subset_cup_l subset_cup_r subset_cap_l subset_cap_r subset_self subset_transitive : Csub_db.
Lemma subset_cup_reduce : ∀ (A B C : Cset),
A ⊂ B ∨ A ⊂ C → A ⊂ (B ∪ C).
Lemma subset_cap_reduce : ∀ (A B C : Cset),
A ⊂ B ∧ A ⊂ C → A ⊂ (B ∩ C).
Lemma subset_ball_l : ∀ (a : C) (ϵ1 ϵ2 : R),
B(a, Rmin ϵ1 ϵ2) ⊂ B(a, ϵ1).
Lemma subset_ball_r : ∀ (a : C) (ϵ1 ϵ2 : R),
B(a, Rmin ϵ1 ϵ2) ⊂ B(a, ϵ2).
Lemma subset_C_ : ∀ (A : Cset),
A ⊂ C_.
#[global] Hint Resolve subset_cup_reduce subset_cap_reduce subset_ball_l subset_ball_r subset_C_ : Csub_db.
Lemma subset_equal : ∀ (A B : Cset),
A ⊂ B → B ⊂ A → A ⩦ B.
Lemma subset_not : ∀ (A B : Cset),
¬ (A ⊂ B) → (∃ a, A a ∧ B` a).
Lemma subset_image : ∀ (A B : Cset) (f : C → C),
A ⊂ B → (f @ A) ⊂ (f @ B).
Lemma circle_in_square : ∀ (cen : C) (s : R),
(ϵ_disk cen s) ⊂ (open_square cen s).
Lemma square_in_circle : ∀ (cen : C) (ϵ : R),
(open_square cen (ϵ / √ 2)) ⊂ (ϵ_disk cen ϵ).
Lemma square_is_rectangle : ∀ (cen : C) (s : R),
(open_square cen s) ⩦ (open_rect cen s s).
Lemma square_in_rect_at_point : ∀ (cen c : C) (s1 s2 : R),
s1 > 0 → s2 > 0 →
(open_rect cen s1 s2) c →
∃ s, s > 0 ∧ (open_square c s) ⊂ (open_rect cen s1 s2).
Lemma square_contains_center : ∀ (cen : C) (s : R),
s > 0 → open_square cen s cen.
some lemmas about open/closed sets
Lemma emptyset_open : open empty_set.
Lemma C_open : open C_.
Lemma ball_open : ∀ (a : C) (ϵ : R),
ϵ > 0 → open (B(a,ϵ)).
Lemma closed_ball_complement_open : ∀ (c : C) (r : R),
open (fun c' ⇒ Cmod (c' - c) > r).
Lemma closed_ball_closed : ∀ (a : C) (ϵ : R),
closed (fun c' ⇒ Cmod (c' - a) ≤ ϵ).
Lemma rect_open : ∀ (cen : C) (s1 s2 : R),
s1 > 0 → s2 > 0 → open (open_rect cen s1 s2).
Lemma cup_open : ∀ (A B : Cset),
open A → open B → open (A ∪ B).
Lemma cap_open : ∀ (A B : Cset),
open A → open B → open (A ∩ B).
lemmas about preimage
some lemmas showing basic properties
Lemma complement_involutive : ∀ (A : Cset),
(A`)` ⩦ A.
Lemma bounded_cup : ∀ (A B : Cset),
bounded A → bounded B → bounded (A ∪ B).
Definition Ccover := Cset → Prop.
Definition WF_cover (G : Ccover) : Prop :=
∀ A A', (A ⩦ A' ∧ G A) → G A'.
Definition WFify_cover (G : Ccover) : Ccover :=
fun A ⇒ ∃ A', A ⩦ A' ∧ G A'.
Definition open_cover (G : Ccover) : Prop :=
∀ A, G A → open A.
Definition subcover (G1 G2 : Ccover) : Prop :=
∀ A, G1 A → G2 A.
Definition eq_cover (G1 G2 : Ccover) : Prop :=
∀ A, G1 A ↔ G2 A.
Fixpoint In' (A : Cset) (l : list Cset) : Prop :=
match l with
| [] ⇒ False
| (A' :: l) ⇒ A ⩦ A' ∨ In' A l
end.
Definition list_to_cover (l : list Cset) : Ccover :=
fun A ⇒ In' A l.
Definition finite_cover (G : Ccover) : Prop :=
∃ l, eq_cover G (list_to_cover l).
Definition big_cup (G : Ccover) : Cset :=
fun c ⇒ (∃ A, G A ∧ A c).
Definition big_cap (G : Ccover) : Cset :=
fun c ⇒ (∀ A, G A → A c).
Definition compact (A : Cset) : Prop :=
∀ G, open_cover G → WF_cover G → A ⊂ (big_cup G) →
(∃ G', finite_cover G' ∧ subcover G' G ∧ A ⊂ (big_cup G')).
Lemma WF_WFify : ∀ (G : Ccover),
WF_cover (WFify_cover G).
Lemma WF_finitecover : ∀ (l : list Cset),
WF_cover (list_to_cover l).
Lemma WFify_is_projection : ∀ (G : Ccover),
WF_cover G →
eq_cover G (WFify_cover G).
Lemma eq_cover_refl : ∀ (G : Ccover), eq_cover G G.
Lemma eq_cover_symm : ∀ (G1 G2 : Ccover), eq_cover G1 G2 → eq_cover G2 G1.
Lemma eq_cover_trans : ∀ (G1 G2 G3 : Ccover),
eq_cover G1 G2 → eq_cover G2 G3 → eq_cover G1 G3.
Add Parametric Relation : Ccover eq_cover
reflexivity proved by eq_cover_refl
symmetry proved by eq_cover_symm
transitivity proved by eq_cover_trans
as eq_cover_equiv_rel.
Add Parametric Morphism : subcover
with signature eq_cover ==> eq_cover ==> iff as subcover_mor.
Add Parametric Morphism : open_cover
with signature eq_cover ==> iff as opencover_mor.
Add Parametric Morphism : big_cup
with signature eq_cover ==> eq_set as bigcup_mor.
Add Parametric Morphism : big_cap
with signature eq_cover ==> eq_set as bigcap_mor.
Add Parametric Morphism : compact
with signature eq_set ==> iff as compact_mor.
now some lemmas
Lemma list_to_cover_reduce : ∀ (A A0 : Cset) (l : list Cset),
list_to_cover (A :: l) A0 ↔
A ⩦ A0 ∨ list_to_cover l A0.
Lemma open_cover_reduce : ∀ (l : list Cset) (A : Cset),
open_cover (list_to_cover (A :: l)) →
open A ∧ open_cover (list_to_cover l).
Lemma subcover_reduce : ∀ (l : list Cset) (A : Cset) (G : Ccover),
subcover (list_to_cover (A :: l)) G →
G A ∧ subcover (list_to_cover l) G.
Lemma finite_cover_subset : ∀ (l : list Cset) (G : Ccover),
WF_cover G → subcover G (list_to_cover l) →
finite_cover G.
Lemma big_cup_extend_l : ∀ (l : list Cset) (A : Cset),
(A ∪ (big_cup (list_to_cover l))) ⩦ (big_cup (list_to_cover (A :: l))).
Lemma big_cap_extend_l : ∀ (l : list Cset) (A : Cset),
(A ∩ (big_cap (list_to_cover l))) ⩦ (big_cap (list_to_cover (A :: l))).
Lemma app_union : ∀ (l1 l2 : list Cset),
(big_cup (list_to_cover (l1 ++ l2))) ⩦
((big_cup (list_to_cover l1)) ∪ (big_cup (list_to_cover l2))).
Lemma In'_app_or : ∀ (l1 l2 : list Cset) (A : Cset),
In' A (l1 ++ l2) → In' A l1 ∨ In' A l2.
Lemma In'_map : ∀ {X} (l : list X) (f : X → Cset) (A : Cset),
In' A (map f l) → ∃ (x : X), (f x) ⩦ A ∧ In x l.
Lemma arb_cup_open : ∀ (G : Ccover),
open_cover G → open (big_cup G).
Lemma ltc_open : ∀ (l : list Cset),
open_cover (list_to_cover l) → open (big_cap (list_to_cover l)).
Lemma fin_cap_open : ∀ (G : Ccover),
open_cover G → finite_cover G → open (big_cap G).
Lemma continuous_preimage_open : ∀ (f : C → C),
continuous_on f C_ → (∀ A, open A → open f*{A}).
Lemma preimage_open_continuous : ∀ (f : C → C),
(∀ A, open A → open f*{A}) → continuous_on f C_.
Definition preimage_cover (f : C → C) (G : Ccover) : Ccover :=
fun A ⇒ (∃ A', G A' ∧ A ⩦ (f*{A'})).
Lemma open_cover_preimage_open : ∀ (f : C → C) (G : Ccover),
open_cover G → continuous_on f C_ →
open_cover (preimage_cover f G).
Lemma WF_preimage_cover : ∀ (f : C → C) (G : Ccover),
WF_cover (preimage_cover f G).
Lemma subset_preimage_pres : ∀ (f : C → C) (A : Cset) (G : Ccover),
((f) @ (A)) ⊂ (big_cup G) →
A ⊂ (big_cup (preimage_cover f G)).
Lemma extract_finite_image : ∀ (f : C → C) (l : list Cset) (A : Cset) (G : Ccover),
WF_cover G →
subcover (list_to_cover l) (preimage_cover f G) →
A ⊂ (big_cup (list_to_cover l)) →
∃ l', subcover (list_to_cover l') G ∧ (f @ A) ⊂ (big_cup (list_to_cover l')).
Lemma continuous_image_compact : ∀ (f : C → C) (A : Cset),
continuous_on f C_ → compact A →
compact (f @ A).
Definition cube_cover (G : Ccover) : Prop :=
∀ A, G A → ∃ s cen, s > 0 ∧ A ⩦ (open_square cen s).
Definition cube_compact (A : Cset) : Prop :=
∀ G, cube_cover G → WF_cover G → A ⊂ (big_cup G) →
(∃ G', finite_cover G' ∧ subcover G' G ∧ A ⊂ (big_cup G')).
Definition cover_to_cube_cover (G : Ccover) : Ccover :=
fun A ⇒ (∃ s cen A', s > 0 ∧ (A ⩦ (open_square cen s)) ∧ G A' ∧ (open_square cen s) ⊂ A').
Lemma cube_cover_open_cover : ∀ (G : Ccover),
cube_cover G → open_cover G.
Lemma WF_ctcc : ∀ (G : Ccover),
WF_cover (cover_to_cube_cover G).
Lemma cube_cover_ctcc : ∀ (G : Ccover),
cube_cover (cover_to_cube_cover G).
Lemma ctcc_in_cover : ∀ (G : Ccover),
open_cover G → (big_cup G) ⩦ (big_cup (cover_to_cube_cover G)).
Lemma fin_cubecover_gives_fin_cover : ∀ (l : list Cset) (G : Ccover),
WF_cover G →
subcover (list_to_cover l) (cover_to_cube_cover G) →
∃ l', subcover (list_to_cover l') G ∧
(big_cup (list_to_cover l)) ⊂ (big_cup (list_to_cover l')).
Lemma compact_is_cube_compact : ∀ (A : Cset),
compact A ↔ cube_compact A.
Definition unit_line : Cset :=
fun c ⇒ 0 ≤ fst c ≤ 1 ∧ snd c = 0.
Definition partial_line (x : R) : Cset :=
fun c ⇒ 0 ≤ fst c ≤ x ∧ snd c = 0.
Definition partial_line_covered (G : Ccover) (x : R) : Prop :=
∃ G', finite_cover G' ∧ subcover G' G ∧ (partial_line x) ⊂ (big_cup G').
Lemma zero_always_covered : ∀ (G : Ccover),
WF_cover G → unit_line ⊂ (big_cup G) →
partial_line_covered G 0.
Lemma plc_le_subset : ∀ (x x' : R),
x' ≤ x →
(partial_line x') ⊂ (partial_line x).
Lemma plc_less : ∀ (x x' : R) (G : Ccover),
x' ≤ x →
partial_line_covered G x →
partial_line_covered G x'.
Lemma not_ub_implies_larger_elem : ∀ (E : R → Prop) (a b : R),
E a → ¬ (is_upper_bound E b) →
∃ a', E a' ∧ b < a'.
Lemma extract_elem_lt_lub : ∀ (E : R → Prop) (a lub ϵ : R),
E a → ϵ > 0 → is_lub E lub →
∃ x, (E x ∧ lub - ϵ < x).
Theorem unit_line_compact : compact unit_line.
Definition horiz_Cline (a b h : R) : Cset :=
fun c ⇒ a ≤ fst c ≤ b ∧ snd c = h.
Definition horiz_from_01_poly (a b h : R) : Polynomial := [(a, h) ; ((b - a)%R, 0)].
Lemma horiz_Cline_image : ∀ (a b h : R),
a ≤ b → ((Peval (horiz_from_01_poly a b h)) @ unit_line) ⩦ (horiz_Cline a b h).
Lemma horiz_Cline_compact : ∀ (a b h : R),
compact (horiz_Cline a b h).
Definition verti_Cline (a b h : R) : Cset :=
fun c ⇒ a ≤ snd c ≤ b ∧ fst c = h.
Definition switch_pair (c : C) : C := (snd c, fst c).
Lemma switch_pair_Cmod : ∀ c, Cmod c = Cmod (switch_pair c).
Lemma switch_pair_minus : ∀ c c0, switch_pair (c - c0) = switch_pair c - switch_pair c0.
Lemma switch_pair_continuous_on_C : continuous_on switch_pair C_.
Lemma verti_Cline_image : ∀ (a b h : R),
switch_pair @ (horiz_Cline a b h) ⩦ (verti_Cline a b h).
Lemma verti_Cline_compact : ∀ (a b h : R),
compact (verti_Cline a b h).
Definition center_square (s : R) : Cset :=
fun c ⇒ -s ≤ fst c ≤ s ∧ -s ≤ snd c ≤ s.
Definition partial_center_square (s x : R) : Cset :=
fun c ⇒ -s ≤ fst c ≤ x ∧ -s ≤ snd c ≤ s.
Definition partial_center_square_covered (G : Ccover) (s x : R) : Prop :=
∃ G', finite_cover G' ∧ subcover G' G ∧ (partial_center_square s x) ⊂ (big_cup G').
Lemma line_in_square : ∀ (s h : R),
-s ≤ h ≤ s →
((verti_Cline (-s) s h) ⊂ (center_square s)).
Lemma zero_width_square : ∀ (s : R),
(partial_center_square s (-s)) ⩦ (verti_Cline (-s) s (-s)).
Lemma negc_always_covered : ∀ (G : Ccover) (s : R),
s > 0 →
WF_cover G → open_cover G →
(center_square s) ⊂ (big_cup G) →
partial_center_square_covered G s (-s).
Lemma pcs_le_subset : ∀ (s x x' : R),
x' ≤ x →
(partial_center_square s x') ⊂ (partial_center_square s x).
Lemma pcs_less : ∀ (s x x' : R) (G : Ccover),
x' ≤ x →
partial_center_square_covered G s x →
partial_center_square_covered G s x'.
Definition cover_to_centered_cube_cover (G : Ccover) (a b h : R) : Ccover :=
fun A ⇒ (∃ s y A', s > 0 ∧ A ⩦ (open_square (h, y) s) ∧ G A' ∧ (open_square (h, y) s) ⊂ A').
Lemma WF_ctccc : ∀ (G : Ccover) (a b h : R),
WF_cover (cover_to_centered_cube_cover G a b h).
Lemma cube_cover_ctccc : ∀ (G : Ccover) (a b h : R),
cube_cover (cover_to_centered_cube_cover G a b h).
Lemma ctccc_smaller : ∀ (G : Ccover) (a b h : R),
(big_cup (cover_to_centered_cube_cover G a b h)) ⊂ (big_cup G).
Lemma ctccc_big_enough : ∀ (G : Ccover) (a b h : R),
open_cover G → (verti_Cline a b h) ⊂ (big_cup G) →
(verti_Cline a b h) ⊂ (big_cup (cover_to_centered_cube_cover G a b h)).
Definition pair_to_sqaures (w : R) (p : R × R) : Cset := open_square (w, (fst p)) (snd p).
Lemma pts_gives_cube_cover : ∀ (h : R) (l : list (R × R)),
(∀ p, In p l → snd p > 0) →
cube_cover (list_to_cover (map (pair_to_sqaures h) l)).
Lemma gen_ccc_list : ∀ (G : Ccover) (a b h : R) (l : list Cset),
subcover (list_to_cover l) (cover_to_centered_cube_cover G a b h) →
∃ l', (∀ p, In p l' → snd p > 0) ∧
eq_cover (list_to_cover (map (pair_to_sqaures h) l')) (list_to_cover l).
Lemma min_side_length : ∀ (p0 : R × R) (l : list (R × R)),
(∀ p, In p (p0 :: l) → snd p > 0) →
(∃ min, 0 < min ∧ (∀ p, In p (p0 :: l) → min < snd p)).
Lemma boost_line : ∀ (a b h : R) (O : Cset),
a < b →
open O → (verti_Cline a b h) ⊂ O →
∃ ϵ, ϵ > 0 ∧ (verti_Cline (a - ϵ) (b + ϵ) h) ⊂ O.
Lemma rect_within_centered_sqaures : ∀ (a b h : R) (l : list (R × R)),
a < b → (∀ p, In p l → snd p > 0) →
(verti_Cline a b h) ⊂ (big_cup (list_to_cover (map (pair_to_sqaures h) l))) →
∃ h' s1 s2, s1 > 0 ∧ s2 > 0 ∧ (verti_Cline a b h) ⊂ (open_rect (h, h') s1 s2) ∧
(open_rect (h, h') s1 s2) ⊂ (big_cup (list_to_cover (map (pair_to_sqaures h) l))).
Lemma rect_within_fin_cubecover : ∀ (a b h : R) (l : list Cset),
a < b →
cube_cover (list_to_cover l) →
(verti_Cline a b h) ⊂ (big_cup (list_to_cover l)) →
∃ h' s1 s2, s1 > 0 ∧ s2 > 0 ∧ (verti_Cline a b h) ⊂ (open_rect (h, h') s1 s2) ∧
(open_rect (h, h') s1 s2) ⊂ (big_cup (list_to_cover l)).
TODO: write a program that reads this proof and makes a more efficient FTA proof.
There must be a better way than this...
Theorem center_square_compact : ∀ (s : R),
s > 0 → compact (center_square s).
Definition ball_cover : Ccover :=
fun G ⇒ open G ∧ ∃ r, r > 0 ∧ G ⊂ B(0,r).
Lemma open_cover_ball_cover : open_cover ball_cover.
Lemma WF_ball_cover : WF_cover ball_cover.
Lemma ball_cover_elems_bounded : ∀ (A : Cset),
ball_cover A → bounded A.
Lemma C_subset_ball_cover :
C_ ⊂ (big_cup ball_cover).
Lemma list_cover_ball_cover_bounded : ∀ (l : list Cset),
subcover (list_to_cover l) ball_cover →
bounded (big_cup (list_to_cover l)).
Lemma fin_subcover_ball_cover_bounded : ∀ (G : Ccover),
finite_cover G → subcover G ball_cover →
bounded (big_cup G).
Lemma compact_implies_bounded : ∀ (A : Cset),
compact A → bounded A.
Definition bad_point_cover (c : C) : Ccover :=
fun G ⇒ open G ∧ ∃ r, r > 0 ∧ G ⊂ (fun c' ⇒ Cmod (c' - c) > r).
Lemma open_cover_bpc : ∀ c, open_cover (bad_point_cover c).
Lemma WF_bpc : ∀ c, WF_cover (bad_point_cover c).
Lemma bpc_covers_almost_all : ∀ (c : C) (A : Cset),
A` c → A ⊂ (big_cup (bad_point_cover c)).
Lemma bpc_separates_from_c : ∀ (c : C) (l : list Cset),
subcover (list_to_cover l) (bad_point_cover c) →
∃ r, r > 0 ∧ (big_cup (list_to_cover l)) ⊂ (fun c' ⇒ Cmod (c' - c) > r).
Lemma compact_implies_closed : ∀ (A : Cset),
compact A → closed A.
Lemma add_comp_covers_all : ∀ (A : Cset) (G : Ccover),
WF_cover G → A ⊂ (big_cup G) →
C_ ⊂ (big_cup (fun A' : Cset ⇒ G A' ∨ (A') ⩦ ((A) `) )).
Lemma closed_subset_compact : ∀ (A B : Cset),
A ⊂ B → compact B → closed A →
compact A.
Lemma closed_bounded_implies_compact : ∀ (A : Cset),
closed A → bounded A →
compact A.
Theorem Heine_Borel : ∀ (A : Cset),
compact A ↔ closed A ∧ bounded A.
s > 0 → compact (center_square s).
Definition ball_cover : Ccover :=
fun G ⇒ open G ∧ ∃ r, r > 0 ∧ G ⊂ B(0,r).
Lemma open_cover_ball_cover : open_cover ball_cover.
Lemma WF_ball_cover : WF_cover ball_cover.
Lemma ball_cover_elems_bounded : ∀ (A : Cset),
ball_cover A → bounded A.
Lemma C_subset_ball_cover :
C_ ⊂ (big_cup ball_cover).
Lemma list_cover_ball_cover_bounded : ∀ (l : list Cset),
subcover (list_to_cover l) ball_cover →
bounded (big_cup (list_to_cover l)).
Lemma fin_subcover_ball_cover_bounded : ∀ (G : Ccover),
finite_cover G → subcover G ball_cover →
bounded (big_cup G).
Lemma compact_implies_bounded : ∀ (A : Cset),
compact A → bounded A.
Definition bad_point_cover (c : C) : Ccover :=
fun G ⇒ open G ∧ ∃ r, r > 0 ∧ G ⊂ (fun c' ⇒ Cmod (c' - c) > r).
Lemma open_cover_bpc : ∀ c, open_cover (bad_point_cover c).
Lemma WF_bpc : ∀ c, WF_cover (bad_point_cover c).
Lemma bpc_covers_almost_all : ∀ (c : C) (A : Cset),
A` c → A ⊂ (big_cup (bad_point_cover c)).
Lemma bpc_separates_from_c : ∀ (c : C) (l : list Cset),
subcover (list_to_cover l) (bad_point_cover c) →
∃ r, r > 0 ∧ (big_cup (list_to_cover l)) ⊂ (fun c' ⇒ Cmod (c' - c) > r).
Lemma compact_implies_closed : ∀ (A : Cset),
compact A → closed A.
Lemma add_comp_covers_all : ∀ (A : Cset) (G : Ccover),
WF_cover G → A ⊂ (big_cup G) →
C_ ⊂ (big_cup (fun A' : Cset ⇒ G A' ∨ (A') ⩦ ((A) `) )).
Lemma closed_subset_compact : ∀ (A B : Cset),
A ⊂ B → compact B → closed A →
compact A.
Lemma closed_bounded_implies_compact : ∀ (A : Cset),
closed A → bounded A →
compact A.
Theorem Heine_Borel : ∀ (A : Cset),
compact A ↔ closed A ∧ bounded A.
showing that closed sets have a minimum norm element
Definition nonneg_real_line : Cset :=
fun c ⇒ fst c ≥ 0 ∧ snd c = 0.
Lemma continuous_Cmod : continuous_on Cmod C_.
Lemma image_nnp : Cmod @ C_ ⩦ nonneg_real_line.
Lemma not_lb_implies_smaller_elem : ∀ (E : R → Prop) (a b : R),
E a → ¬ (is_lower_bound E b) →
∃ a', E a' ∧ a' < b.
Lemma extract_elem_gt_glb : ∀ (E : R → Prop) (a glb ϵ : R),
E a → ϵ > 0 → is_glb E glb →
∃ x, (E x ∧ x < glb + ϵ).
Lemma closed_line_has_min : ∀ (A : Cset),
closed A → A ⊂ nonneg_real_line →
(∃ c, A c) →
∃ min, A (min, 0) ∧ (∀ p, A p → min ≤ fst p).
Lemma compact_contains_min_norn_elem : ∀ (A : Cset),
(∃ c, A c) → compact A →
(∃ mne, A mne ∧ (∀ c, A c → Cmod mne ≤ Cmod c)).