Let f be given.

Assume Hf: f ∈ bounded_sequences_Romega.

We prove the intermediate claim HfX: f ∈ X.

An exact proof term for the current goal is (SepE1 R_omega_space (λf0 : set ⇒ bounded_sequence_Romega f0) f Hf).

We prove the intermediate claim Hb: bounded_sequence_Romega f.

An exact proof term for the current goal is (SepE2 R_omega_space (λf0 : set ⇒ bounded_sequence_Romega f0) f Hf).

Apply Hb to the current goal.

Let M be given.

Assume HMconj.

We prove the intermediate claim HMR: M ∈ R.

An exact proof term for the current goal is (andEL (M ∈ R) (∀n : set, n ∈ ω → apply_fun f n ∈ open_interval (minus_SNo M) M) HMconj).

We prove the intermediate claim Hbnd: ∀n : set, n ∈ ω → apply_fun f n ∈ open_interval (minus_SNo M) M.

An exact proof term for the current goal is (andER (M ∈ R) (∀n : set, n ∈ ω → apply_fun f n ∈ open_interval (minus_SNo M) M) HMconj).

We prove the intermediate claim H0omega: 0 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 0 nat_0).

We prove the intermediate claim Hf0In: apply_fun f 0 ∈ open_interval (minus_SNo M) M.

An exact proof term for the current goal is (Hbnd 0 H0omega).

We prove the intermediate claim Hf0prop: Rlt (minus_SNo M) (apply_fun f 0) ∧ Rlt (apply_fun f 0) M.

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo M) x0 ∧ Rlt x0 M) (apply_fun f 0) Hf0In).

We prove the intermediate claim Hm0: Rlt (minus_SNo M) (apply_fun f 0).

An exact proof term for the current goal is (andEL (Rlt (minus_SNo M) (apply_fun f 0)) (Rlt (apply_fun f 0) M) Hf0prop).

We prove the intermediate claim H0m: Rlt (apply_fun f 0) M.

An exact proof term for the current goal is (andER (Rlt (minus_SNo M) (apply_fun f 0)) (Rlt (apply_fun f 0) M) Hf0prop).

We prove the intermediate claim HMlt: Rlt (minus_SNo M) M.

An exact proof term for the current goal is (Rlt_tra (minus_SNo M) (apply_fun f 0) M Hm0 H0m).

We prove the intermediate claim HopenI: open_interval (minus_SNo M) M ∈ R_standard_topology.

An exact proof term for the current goal is (open_interval_in_R_standard_topology (minus_SNo M) M HMlt).

We prove the intermediate claim HX0: apply_fun Xi 0 = (R,R_standard_topology).

An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology 0 H0omega).

We prove the intermediate claim HT0: space_family_topology Xi 0 = R_standard_topology.

We prove the intermediate claim Hdef: space_family_topology Xi 0 = (apply_fun Xi 0) 1.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

rewrite the current goal using HX0 (from left to right).

An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).

We prove the intermediate claim HTfam: R_standard_topology ∈ {space_family_topology Xi i|i ∈ ω}.

Apply ReplEq ω (λi : set ⇒ space_family_topology Xi i) R_standard_topology to the current goal.

Assume _ H2.

Apply H2 to the current goal.

We will prove ∃i ∈ ω, R_standard_topology = space_family_topology Xi i.

We use 0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H0omega.

Use symmetry.

An exact proof term for the current goal is HT0.

We prove the intermediate claim HintervalTU: open_interval (minus_SNo M) M ∈ TU.

An exact proof term for the current goal is (UnionI {space_family_topology Xi i|i ∈ ω} (open_interval (minus_SNo M) M) R_standard_topology HopenI HTfam).

Set Um to be the term const_fun ω (open_interval (minus_SNo M) M).

Set bM to be the term {g ∈ X|∀i : set, i ∈ ω → apply_fun g i ∈ apply_fun Um i}.

We use bM to witness the existential quantifier.

Apply andI to the current goal.

We will prove bM ∈ B.

We prove the intermediate claim HbMsub: bM ⊆ X.

Let g be given.

Assume Hg: g ∈ bM.

We will prove g ∈ X.

An exact proof term for the current goal is (SepE1 X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun Um i) g Hg).

We prove the intermediate claim HbMpow: bM ∈ 𝒫 X.

An exact proof term for the current goal is (PowerI X bM HbMsub).

We prove the intermediate claim Htot: total_function_on Um ω TU.

An exact proof term for the current goal is (const_fun_total_function_on ω TU (open_interval (minus_SNo M) M) HintervalTU).

We prove the intermediate claim HUmgraph: functional_graph Um.

An exact proof term for the current goal is (functional_graph_const_fun ω (open_interval (minus_SNo M) M)).

We prove the intermediate claim HUmcoords: ∀i : set, i ∈ ω → apply_fun Um i ∈ space_family_topology Xi i.

Let i be given.

Assume Hi: i ∈ ω.

We will prove apply_fun Um i ∈ space_family_topology Xi i.

We prove the intermediate claim Happ: apply_fun Um i = open_interval (minus_SNo M) M.

An exact proof term for the current goal is (const_fun_apply ω (open_interval (minus_SNo M) M) i Hi).

rewrite the current goal using Happ (from left to right).

We prove the intermediate claim HXi: apply_fun Xi i = (R,R_standard_topology).

An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology i Hi).

We prove the intermediate claim HTi: space_family_topology Xi i = R_standard_topology.

We prove the intermediate claim Hdef: space_family_topology Xi i = (apply_fun Xi i) 1.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

rewrite the current goal using HXi (from left to right).

An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).

rewrite the current goal using HTi (from left to right).

An exact proof term for the current goal is HopenI.

We prove the intermediate claim HexU: ∃U : set, total_function_on U ω TU ∧ functional_graph U ∧ (∀i : set, i ∈ ω → apply_fun U i ∈ space_family_topology Xi i) ∧ bM = {f ∈ X|∀i : set, i ∈ ω → apply_fun f i ∈ apply_fun U i}.

We use Um to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Htot.

An exact proof term for the current goal is HUmgraph.

An exact proof term for the current goal is HUmcoords.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 X) (λB0 : set ⇒ ∃U : set, total_function_on U ω TU ∧ functional_graph U ∧ (∀i : set, i ∈ ω → apply_fun U i ∈ space_family_topology Xi i) ∧ B0 = {f ∈ X|∀i : set, i ∈ ω → apply_fun f i ∈ apply_fun U i}) bM HbMpow HexU).

Apply andI to the current goal.

We will prove f ∈ bM.

Apply (SepI X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun Um i) f HfX) to the current goal.

Let i be given.

Assume Hi: i ∈ ω.

We will prove apply_fun f i ∈ apply_fun Um i.

We prove the intermediate claim Happ: apply_fun Um i = open_interval (minus_SNo M) M.

An exact proof term for the current goal is (const_fun_apply ω (open_interval (minus_SNo M) M) i Hi).

rewrite the current goal using Happ (from left to right).

An exact proof term for the current goal is (Hbnd i Hi).

Let g be given.

Assume Hg: g ∈ bM.

We will prove g ∈ bounded_sequences_Romega.

We prove the intermediate claim HgX: g ∈ X.

An exact proof term for the current goal is (SepE1 X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun Um i) g Hg).

We prove the intermediate claim Hgprop: ∀i : set, i ∈ ω → apply_fun g i ∈ apply_fun Um i.

An exact proof term for the current goal is (SepE2 X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun Um i) g Hg).

We prove the intermediate claim Hbseqg: bounded_sequence_Romega g.

We prove the intermediate claim Hbndg: ∀n : set, n ∈ ω → apply_fun g n ∈ open_interval (minus_SNo M) M.

Let n be given.

Assume HnO: n ∈ ω.

We prove the intermediate claim Hgn: apply_fun g n ∈ apply_fun Um n.

An exact proof term for the current goal is (Hgprop n HnO).

We prove the intermediate claim Happ: apply_fun Um n = open_interval (minus_SNo M) M.

An exact proof term for the current goal is (const_fun_apply ω (open_interval (minus_SNo M) M) n HnO).

rewrite the current goal using Happ (from right to left).

An exact proof term for the current goal is Hgn.

An exact proof term for the current goal is (λP Hp ⇒ Hp M (andI (M ∈ R) (∀n : set, n ∈ ω → apply_fun g n ∈ open_interval (minus_SNo M) M) HMR Hbndg)).

An exact proof term for the current goal is (SepI R_omega_space (λh : set ⇒ bounded_sequence_Romega h) g HgX Hbseqg).