We will prove finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology ∧ finer_than R_standard_topology R_finite_complement_topology ∧ finer_than R_standard_topology R_ray_topology.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove finer_than R_upper_limit_topology R_standard_topology.
We will prove R_standard_topology ⊆ R_upper_limit_topology.
Let U be given.
Assume HU: U ∈ R_standard_topology.
We prove the intermediate claim HUinPow: U ∈ 𝒫 R.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b0 ∈ R_standard_basis, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim HUpropUpper: ∀x ∈ U, ∃b0 ∈ R_upper_limit_basis, x ∈ b0 ∧ b0 ⊆ U.
Let x be given.
Assume HxU.
We prove the intermediate claim HexStd: ∃bStd ∈ R_standard_basis, x ∈ bStd ∧ bStd ⊆ U.
An exact proof term for the current goal is (HUprop x HxU).
Apply HexStd to the current goal.
Let bStd be given.
Assume HbStdPair.
We prove the intermediate claim HbStdIn: bStd ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (bStd ∈ R_standard_basis) (x ∈ bStd ∧ bStd ⊆ U) HbStdPair).
We prove the intermediate claim HbStdProp: x ∈ bStd ∧ bStd ⊆ U.
An exact proof term for the current goal is (andER (bStd ∈ R_standard_basis) (x ∈ bStd ∧ bStd ⊆ U) HbStdPair).
We prove the intermediate claim HxInbStd: x ∈ bStd.
An exact proof term for the current goal is (andEL (x ∈ bStd) (bStd ⊆ U) HbStdProp).
We prove the intermediate claim HbStdSubU: bStd ⊆ U.
An exact proof term for the current goal is (andER (x ∈ bStd) (bStd ⊆ U) HbStdProp).
We prove the intermediate claim Hexa0: ∃a0 ∈ R, bStd ∈ {open_interval a0 b0|b0 ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b0|b0 ∈ R}) bStd HbStdIn).
Apply Hexa0 to the current goal.
Let a0 be given.
Assume Ha0Pair.
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (andEL (a0 ∈ R) (bStd ∈ {open_interval a0 b0|b0 ∈ R}) Ha0Pair).
We prove the intermediate claim HbStdFam: bStd ∈ {open_interval a0 b0|b0 ∈ R}.
An exact proof term for the current goal is (andER (a0 ∈ R) (bStd ∈ {open_interval a0 b0|b0 ∈ R}) Ha0Pair).
We prove the intermediate claim Hexb0: ∃b0 ∈ R, bStd = open_interval a0 b0.
An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ open_interval a0 b0) bStd HbStdFam).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0Pair.
We prove the intermediate claim Hb0R: b0 ∈ R.
An exact proof term for the current goal is (andEL (b0 ∈ R) (bStd = open_interval a0 b0) Hb0Pair).
We prove the intermediate claim HbStdEq: bStd = open_interval a0 b0.
An exact proof term for the current goal is (andER (b0 ∈ R) (bStd = open_interval a0 b0) Hb0Pair).
We prove the intermediate claim HxInI: x ∈ open_interval a0 b0.
rewrite the current goal using HbStdEq (from right to left).
An exact proof term for the current goal is HxInbStd.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a0 x0 ∧ Rlt x0 b0) x HxInI).
We prove the intermediate claim HxIProp: Rlt a0 x ∧ Rlt x b0.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a0 x0 ∧ Rlt x0 b0) x HxInI).
We prove the intermediate claim Ha0x: Rlt a0 x.
An exact proof term for the current goal is (andEL (Rlt a0 x) (Rlt x b0) HxIProp).
We prove the intermediate claim Hxb0: Rlt x b0.
An exact proof term for the current goal is (andER (Rlt a0 x) (Rlt x b0) HxIProp).
Set bUpper to be the term halfopen_interval_right a0 x.
We use bUpper to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HbFamUpper: bUpper ∈ {halfopen_interval_right a0 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a0 bb) x HxR).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a0 bUpper Ha0R HbFamUpper).
Apply andI to the current goal.
An exact proof term for the current goal is (halfopen_interval_right_rightmem a0 x Ha0x).
Let y be given.
Assume HyUpper: y ∈ bUpper.
We will prove y ∈ U.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λy0 : set ⇒ Rlt a0 y0 ∧ ¬ (Rlt x y0)) y HyUpper).
We prove the intermediate claim HyProp: Rlt a0 y ∧ ¬ (Rlt x y).
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ Rlt a0 y0 ∧ ¬ (Rlt x y0)) y HyUpper).
We prove the intermediate claim Ha0y: Rlt a0 y.
An exact proof term for the current goal is (andEL (Rlt a0 y) (¬ (Rlt x y)) HyProp).
We prove the intermediate claim HnotRltxy: ¬ (Rlt x y).
An exact proof term for the current goal is (andER (Rlt a0 y) (¬ (Rlt x y)) HyProp).
We prove the intermediate claim Hnot_xlt_y: ¬ (x < y).
Assume Hxy: x < y.
We prove the intermediate claim HxyRlt: Rlt x y.
An exact proof term for the current goal is (RltI x y HxR HyR Hxy).
An exact proof term for the current goal is (HnotRltxy HxyRlt).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hb0S: SNo b0.
An exact proof term for the current goal is (real_SNo b0 Hb0R).
We prove the intermediate claim Hxltb0: x < b0.
An exact proof term for the current goal is (RltE_lt x b0 Hxb0).
We prove the intermediate claim Hyltb0: y < b0.
Apply (SNoLt_trichotomy_or_impred y x HyS HxS (y < b0)) to the current goal.
Assume Hyltx: y < x.
An exact proof term for the current goal is (SNoLt_tra y x b0 HyS HxS Hb0S Hyltx Hxltb0).
Assume Heyx: y = x.
rewrite the current goal using Heyx (from left to right).
An exact proof term for the current goal is Hxltb0.
Assume HxltY: x < y.
We prove the intermediate claim HxyFalse: False.
An exact proof term for the current goal is (Hnot_xlt_y HxltY).
An exact proof term for the current goal is (FalseE HxyFalse (y < b0)).
We prove the intermediate claim HyRltb0: Rlt y b0.
An exact proof term for the current goal is (RltI y b0 HyR Hb0R Hyltb0).
We prove the intermediate claim HyConj: Rlt a0 y ∧ Rlt y b0.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0y.
An exact proof term for the current goal is HyRltb0.
We prove the intermediate claim HyInI: y ∈ open_interval a0 b0.
An exact proof term for the current goal is (SepI R (λy0 : set ⇒ Rlt a0 y0 ∧ Rlt y0 b0) y HyR HyConj).
We prove the intermediate claim HyInbStd: y ∈ bStd.
rewrite the current goal using HbStdEq (from left to right) at position 1.
An exact proof term for the current goal is HyInI.
An exact proof term for the current goal is (HbStdSubU y HyInbStd).
An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_upper_limit_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HUinPow HUpropUpper).
We will prove finer_than R_K_topology R_standard_topology.
We will prove R_standard_topology ⊆ R_K_topology.
Let U be given.
Assume HU: U ∈ R_standard_topology.
We prove the intermediate claim HUinPow: U ∈ 𝒫 R.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b0 ∈ R_standard_basis, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim HUpropK: ∀x ∈ U, ∃b0 ∈ (R_standard_basis ∪ R_K_basis), x ∈ b0 ∧ b0 ⊆ U.
Let x be given.
Assume HxU.
We prove the intermediate claim Hexb: ∃b0 ∈ R_standard_basis, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUprop x HxU).
Apply Hexb to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0Std: b0 ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (b0 ∈ R_standard_basis) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hb0prop: x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (andER (b0 ∈ R_standard_basis) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hxb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) Hb0prop).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) Hb0prop).
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 R_standard_basis R_K_basis b0 Hb0Std).
Apply andI to the current goal.
An exact proof term for the current goal is Hxb0.
An exact proof term for the current goal is Hb0subU.
An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ (R_standard_basis ∪ R_K_basis), x0 ∈ b0 ∧ b0 ⊆ U0) U HUinPow HUpropK).
We will prove finer_than R_standard_topology R_finite_complement_topology.
We will prove R_finite_complement_topology ⊆ R_standard_topology.
Let U be given.
Assume HU: U ∈ R_finite_complement_topology.
We prove the intermediate claim HUpow: U ∈ 𝒫 R.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ finite (R ∖ U0) ∨ U0 = Empty) U HU).
We prove the intermediate claim HUsub: U ⊆ R.
An exact proof term for the current goal is (PowerE R U HUpow).
We prove the intermediate claim HUcases: finite (R ∖ U) ∨ U = Empty.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ finite (R ∖ U0) ∨ U0 = Empty) U HU).
Apply (HUcases (U ∈ R_standard_topology)) to the current goal.
Assume HFin: finite (R ∖ U).
We will prove U ∈ R_standard_topology.
We prove the intermediate claim HFsubR: (R ∖ U) ⊆ R.
An exact proof term for the current goal is (setminus_Subq R U).
We prove the intermediate claim Hopen: R ∖ (R ∖ U) ∈ R_standard_topology.
An exact proof term for the current goal is (finite_complement_open_in_R_standard_topology (R ∖ U) HFin HFsubR).
rewrite the current goal using (setminus_setminus_eq R U HUsub) (from right to left).
An exact proof term for the current goal is Hopen.
Assume HUe: U = Empty.
rewrite the current goal using HUe (from left to right).
An exact proof term for the current goal is (topology_has_empty R R_standard_topology (R_standard_topology_is_topology_local)).
We will prove finer_than R_standard_topology R_ray_topology.
Let U be given.
Assume HU: U ∈ R_ray_topology.
We prove the intermediate claim HUcases: U = Empty ∨ U = R ∨ ∃a ∈ R, U = {x ∈ R|Rlt x a}.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ U0 = Empty ∨ U0 = R ∨ ∃a0 ∈ R, U0 = {x ∈ R|Rlt x a0}) U HU).
We prove the intermediate claim Hempty: Empty ∈ R_standard_topology.
An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) Empty (Empty_In_Power R) (λx0 Hx0 ⇒ EmptyE x0 Hx0 (∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ Empty))).
We prove the intermediate claim Hall: R ∈ R_standard_topology.
We prove the intermediate claim HRpow: R ∈ 𝒫 R.
Apply PowerI to the current goal.
An exact proof term for the current goal is (Subq_ref R).
We prove the intermediate claim HRprop: ∀x ∈ R, ∃b0 ∈ R_standard_basis, x ∈ b0 ∧ b0 ⊆ R.
Let x be given.
Assume HxR.
Set a0 to be the term add_SNo x (minus_SNo 1).
Set b0 to be the term add_SNo x 1.
Set I to be the term open_interval a0 b0.
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR (minus_SNo 1) Hm1R).
We prove the intermediate claim Hb0R: b0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (real_SNo (minus_SNo 1) Hm1R).
We prove the intermediate claim Ha0lt: a0 < x.
We prove the intermediate claim Hlt: a0 < add_SNo x 0.
An exact proof term for the current goal is (add_SNo_Lt2 x (minus_SNo 1) 0 HxS Hm1S SNo_0 minus_1_lt_0).
rewrite the current goal using (add_SNo_0R x HxS) (from right to left) at position 2.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hxb0: x < b0.
We prove the intermediate claim Hlt: add_SNo x 0 < b0.
An exact proof term for the current goal is (add_SNo_Lt2 x 0 1 HxS SNo_0 (real_SNo 1 real_1) SNoLt_0_1).
rewrite the current goal using (add_SNo_0R x HxS) (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim HxInI: x ∈ I.
We prove the intermediate claim Hax: Rlt a0 x.
An exact proof term for the current goal is (RltI a0 x Ha0R HxR Ha0lt).
We prove the intermediate claim Hxb: Rlt x b0.
An exact proof term for the current goal is (RltI x b0 HxR Hb0R Hxb0).
We prove the intermediate claim Hconj: Rlt a0 x ∧ Rlt x b0.
Apply andI to the current goal.
An exact proof term for the current goal is Hax.
An exact proof term for the current goal is Hxb.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a0 x0 ∧ Rlt x0 b0) x HxR Hconj).
We prove the intermediate claim HIStd: I ∈ R_standard_basis.
We prove the intermediate claim HIa: I ∈ {open_interval a0 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a0 bb) b0 Hb0R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a0 I Ha0R HIa).
We use I to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HIStd.
Apply andI to the current goal.
An exact proof term for the current goal is HxInI.
An exact proof term for the current goal is (open_interval_Subq_R a0 b0).
An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) R HRpow HRprop).
We prove the intermediate claim Hcase1: U = Empty → U ∈ R_standard_topology.
Assume Heq.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hempty.
We prove the intermediate claim Hcase2: U = R → U ∈ R_standard_topology.
Assume Heq.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hall.
We prove the intermediate claim Hcase3: (∃a0 ∈ R, U = {x ∈ R|Rlt x a0}) → U ∈ R_standard_topology.
Assume Hex.
Apply Hex to the current goal.
Let a0 be given.
Assume Ha0pair: a0 ∈ R ∧ U = {x ∈ R|Rlt x a0}.
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (andEL (a0 ∈ R) (U = {x ∈ R|Rlt x a0}) Ha0pair).
We prove the intermediate claim Heq: U = {x ∈ R|Rlt x a0}.
An exact proof term for the current goal is (andER (a0 ∈ R) (U = {x ∈ R|Rlt x a0}) Ha0pair).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (open_left_ray_in_R_standard_topology a0 Ha0R).
We will prove U ∈ R_standard_topology.
Apply (HUcases (U ∈ R_standard_topology)) to the current goal.
Assume HUR: U = Empty ∨ U = R.
Apply (HUR (U ∈ R_standard_topology)) to the current goal.
An exact proof term for the current goal is Hcase1.
An exact proof term for the current goal is Hcase2.
An exact proof term for the current goal is Hcase3.
∎