Let X, d and seq be given.
Assume Hd: metric_on X d.
Assume Hcomp: compact_space X (metric_topology X d).
Assume Hseq: sequence_on seq X.
We will prove ∃subseq : set, ∃x : set, subsequence_of seq subseq ∧ converges_to X (metric_topology X d) subseq x.
Set Tx to be the term metric_topology X d.
Set net0 to be the term sequence_as_net seq.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
We prove the intermediate claim HdirO: directed_set ω (inclusion_rel ω).
An exact proof term for the current goal is omega_directed_by_inclusion_rel.
We prove the intermediate claim Hseqval: ∀n : set, n ∈ ω → apply_fun seq n ∈ X.
Let n be given.
Assume HnO: n ∈ ω.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim Htotnet: total_function_on net0 ω X.
We prove the intermediate claim Hdef: net0 = graph ω (λn : set ⇒ apply_fun seq n).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (total_function_on_graph ω X (λn : set ⇒ apply_fun seq n) Hseqval).
We prove the intermediate claim Hgraphnet: functional_graph net0.
We prove the intermediate claim Hdef: net0 = graph ω (λn : set ⇒ apply_fun seq n).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (functional_graph_graph ω (λn : set ⇒ apply_fun seq n)).
We prove the intermediate claim Hdomnet: graph_domain_subset net0 ω.
We prove the intermediate claim Hdef: net0 = graph ω (λn : set ⇒ apply_fun seq n).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (graph_domain_subset_graph ω (λn : set ⇒ apply_fun seq n)).
We prove the intermediate claim Hexx0: ∃x0 : set, accumulation_point_of_net_on X Tx net0 ω (inclusion_rel ω) x0.
An exact proof term for the current goal is (compact_space_net_has_accumulation_point_on X Tx net0 ω (inclusion_rel ω) Hcomp HdirO Htotnet Hgraphnet Hdomnet).
Apply Hexx0 to the current goal.
Let x0 be given.
Assume Hacc: accumulation_point_of_net_on X Tx net0 ω (inclusion_rel ω) x0.
Apply Hacc to the current goal.
Assume HaccCore HaccTail.
Apply HaccCore to the current goal.
Assume HaccCore6 Hx0X.
Apply HaccCore6 to the current goal.
Assume HaccCore5 Hdomnet2.
Apply HaccCore5 to the current goal.
Assume HaccCore4 Hgraphnet2.
Apply HaccCore4 to the current goal.
Assume HaccCore3 Htotnet2.
Apply HaccCore3 to the current goal.
Assume HaccCore2 HdirO2.
Apply HaccCore2 to the current goal.
Assume _ HTx2.
Set Ball to be the term (λn : set ⇒ open_ball X d x0 (inv_nat (ordsucc n))).
We prove the intermediate claim HBallOpen: ∀n : set, n ∈ ω → Ball n ∈ Tx.
Let n be given.
Assume HnO: n ∈ ω.
We will prove Ball n ∈ Tx.
We prove the intermediate claim HsuccO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HsuccNot0: ordsucc n ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HsuccO.
Assume Hmem0: ordsucc n ∈ {0}.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) Hmem0).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
We prove the intermediate claim HinvR: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) HsuccO).
We prove the intermediate claim HinvPos: Rlt 0 (inv_nat (ordsucc n)).
An exact proof term for the current goal is (inv_nat_pos (ordsucc n) HsuccNot0).
An exact proof term for the current goal is (open_ball_in_metric_topology X d x0 (inv_nat (ordsucc n)) Hd Hx0X HinvPos).
We prove the intermediate claim Hx0inBall: ∀n : set, n ∈ ω → x0 ∈ Ball n.
Let n be given.
Assume HnO: n ∈ ω.
We will prove x0 ∈ Ball n.
We prove the intermediate claim HsuccO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HsuccNot0: ordsucc n ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HsuccO.
Assume Hmem0: ordsucc n ∈ {0}.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) Hmem0).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
We prove the intermediate claim HinvPos: Rlt 0 (inv_nat (ordsucc n)).
An exact proof term for the current goal is (inv_nat_pos (ordsucc n) HsuccNot0).
An exact proof term for the current goal is (center_in_open_ball X d x0 (inv_nat (ordsucc n)) Hd Hx0X HinvPos).
Set BasePred to be the term (λj : set ⇒ j ∈ ω ∧ apply_fun net0 j ∈ Ball 0).
We prove the intermediate claim HexBase: ∃j : set, BasePred j.
We prove the intermediate claim H0O: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HB0open: Ball 0 ∈ Tx.
An exact proof term for the current goal is (HBallOpen 0 H0O).
We prove the intermediate claim Hx0B0: x0 ∈ Ball 0.
An exact proof term for the current goal is (Hx0inBall 0 H0O).
We prove the intermediate claim Hexj: ∃j : set, j ∈ ω ∧ (0,j) ∈ inclusion_rel ω ∧ apply_fun net0 j ∈ Ball 0.
An exact proof term for the current goal is (HaccTail (Ball 0) HB0open Hx0B0 0 H0O).
Apply Hexj to the current goal.
Let j be given.
Assume Hjpack.
We prove the intermediate claim HjO: j ∈ ω.
We prove the intermediate claim Hleft: j ∈ ω ∧ (0,j) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andEL (j ∈ ω ∧ (0,j) ∈ inclusion_rel ω) (apply_fun net0 j ∈ Ball 0) Hjpack).
An exact proof term for the current goal is (andEL (j ∈ ω) ((0,j) ∈ inclusion_rel ω) Hleft).
We prove the intermediate claim Hjrest: (0,j) ∈ inclusion_rel ω ∧ apply_fun net0 j ∈ Ball 0.
We prove the intermediate claim Hleft: j ∈ ω ∧ (0,j) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andEL (j ∈ ω ∧ (0,j) ∈ inclusion_rel ω) (apply_fun net0 j ∈ Ball 0) Hjpack).
We prove the intermediate claim Hjle: (0,j) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andER (j ∈ ω) ((0,j) ∈ inclusion_rel ω) Hleft).
Apply andI to the current goal.
An exact proof term for the current goal is Hjle.
An exact proof term for the current goal is (andER (j ∈ ω ∧ (0,j) ∈ inclusion_rel ω) (apply_fun net0 j ∈ Ball 0) Hjpack).
We prove the intermediate claim HjB0: apply_fun net0 j ∈ Ball 0.
An exact proof term for the current goal is (andER ((0,j) ∈ inclusion_rel ω) (apply_fun net0 j ∈ Ball 0) Hjrest).
We use j to witness the existential quantifier.
An exact proof term for the current goal is (andI (j ∈ ω) (apply_fun net0 j ∈ Ball 0) HjO HjB0).
Set base to be the term Eps_i BasePred.
We prove the intermediate claim Hbase: BasePred base.
An exact proof term for the current goal is (Eps_i_ex BasePred HexBase).
Set StepPred to be the term (λk r j : set ⇒ j ∈ ω ∧ (ordsucc r ⊆ j) ∧ apply_fun net0 j ∈ Ball (ordsucc k)).
Set Step to be the term (λk r : set ⇒ Eps_i (λj : set ⇒ StepPred k r j)).
We prove the intermediate claim HStepSpec: ∀k r : set, k ∈ ω → r ∈ ω → StepPred k r (Step k r).
Let k and r be given.
Assume HkO: k ∈ ω.
Assume HrO: r ∈ ω.
Set U to be the term Ball (ordsucc k).
We prove the intermediate claim HskO: ordsucc k ∈ ω.
An exact proof term for the current goal is (omega_ordsucc k HkO).
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (HBallOpen (ordsucc k) HskO).
We prove the intermediate claim Hx0U: x0 ∈ U.
An exact proof term for the current goal is (Hx0inBall (ordsucc k) HskO).
We prove the intermediate claim HsrO: ordsucc r ∈ ω.
An exact proof term for the current goal is (omega_ordsucc r HrO).
We prove the intermediate claim Hexj: ∃j : set, j ∈ ω ∧ (ordsucc r,j) ∈ inclusion_rel ω ∧ apply_fun net0 j ∈ U.
An exact proof term for the current goal is (HaccTail U HUopen Hx0U (ordsucc r) HsrO).
We prove the intermediate claim HexStep: ∃j : set, StepPred k r j.
Apply Hexj to the current goal.
Let j be given.
Assume Hjpack.
We prove the intermediate claim HjO: j ∈ ω.
We prove the intermediate claim Hleft: j ∈ ω ∧ (ordsucc r,j) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andEL (j ∈ ω ∧ (ordsucc r,j) ∈ inclusion_rel ω) (apply_fun net0 j ∈ U) Hjpack).
An exact proof term for the current goal is (andEL (j ∈ ω) ((ordsucc r,j) ∈ inclusion_rel ω) Hleft).
We prove the intermediate claim Hjrest: (ordsucc r,j) ∈ inclusion_rel ω ∧ apply_fun net0 j ∈ U.
We prove the intermediate claim Hleft: j ∈ ω ∧ (ordsucc r,j) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andEL (j ∈ ω ∧ (ordsucc r,j) ∈ inclusion_rel ω) (apply_fun net0 j ∈ U) Hjpack).
We prove the intermediate claim Hjle0: (ordsucc r,j) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andER (j ∈ ω) ((ordsucc r,j) ∈ inclusion_rel ω) Hleft).
Apply andI to the current goal.
An exact proof term for the current goal is Hjle0.
An exact proof term for the current goal is (andER (j ∈ ω ∧ (ordsucc r,j) ∈ inclusion_rel ω) (apply_fun net0 j ∈ U) Hjpack).
We prove the intermediate claim Hjle: (ordsucc r,j) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andEL ((ordsucc r,j) ∈ inclusion_rel ω) (apply_fun net0 j ∈ U) Hjrest).
We prove the intermediate claim HjU: apply_fun net0 j ∈ U.
An exact proof term for the current goal is (andER ((ordsucc r,j) ∈ inclusion_rel ω) (apply_fun net0 j ∈ U) Hjrest).
We prove the intermediate claim Hsub: ordsucc r ⊆ j.
An exact proof term for the current goal is (andER ((ordsucc r,j) ∈ setprod ω ω) (ordsucc r ⊆ j) (inclusion_relE ω (ordsucc r) j Hjle)).
We use j to witness the existential quantifier.
An exact proof term for the current goal is (andI (j ∈ ω ∧ ordsucc r ⊆ j) (apply_fun net0 j ∈ Ball (ordsucc k)) (andI (j ∈ ω) (ordsucc r ⊆ j) HjO Hsub) HjU).
An exact proof term for the current goal is (Eps_i_ex (λj : set ⇒ StepPred k r j) HexStep).
Set fval to be the term (λn : set ⇒ nat_primrec base Step n).
Set f to be the term graph ω fval.
Set subseq to be the term compose_fun ω f seq.
Set Inv to be the term (λn : set ⇒ nat_p n → (fval n ∈ ω ∧ apply_fun net0 (fval n) ∈ Ball n)).
We prove the intermediate claim HInv0: Inv 0.
Assume H0nat: nat_p 0.
We will prove fval 0 ∈ ω ∧ apply_fun net0 (fval 0) ∈ Ball 0.
We prove the intermediate claim Hdef0: fval 0 = nat_primrec base Step 0.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
We prove the intermediate claim Hprim0: nat_primrec base Step 0 = base.
An exact proof term for the current goal is (nat_primrec_0 base Step).
rewrite the current goal using Hprim0 (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (base ∈ ω) (apply_fun net0 base ∈ Ball 0) Hbase).
An exact proof term for the current goal is (andER (base ∈ ω) (apply_fun net0 base ∈ Ball 0) Hbase).
We prove the intermediate claim HInvS: ∀n : set, nat_p n → Inv n → Inv (ordsucc n).
Let n be given.
Assume HnNat: nat_p n.
Assume HInvn: Inv n.
Assume HsnNat: nat_p (ordsucc n).
We will prove fval (ordsucc n) ∈ ω ∧ apply_fun net0 (fval (ordsucc n)) ∈ Ball (ordsucc n).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (nat_p_omega n HnNat).
We prove the intermediate claim Hfn: fval n ∈ ω.
An exact proof term for the current goal is (andEL (fval n ∈ ω) (apply_fun net0 (fval n) ∈ Ball n) (HInvn HnNat)).
We prove the intermediate claim HdefS: fval (ordsucc n) = nat_primrec base Step (ordsucc n).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec base Step (ordsucc n) = Step n (nat_primrec base Step n).
An exact proof term for the current goal is (nat_primrec_S base Step n HnNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HprimN: nat_primrec base Step n = fval n.
Use reflexivity.
rewrite the current goal using HprimN (from left to right).
We prove the intermediate claim Hstep: StepPred n (fval n) (Step n (fval n)).
An exact proof term for the current goal is (HStepSpec n (fval n) HnO Hfn).
Apply Hstep to the current goal.
Assume Hleft HstepU.
Apply Hleft to the current goal.
Assume HstepIn _.
An exact proof term for the current goal is (andI (Step n (fval n) ∈ ω) (apply_fun net0 (Step n (fval n)) ∈ Ball (ordsucc n)) HstepIn HstepU).
We prove the intermediate claim HInvAll: ∀n : set, nat_p n → Inv n.
Apply nat_ind to the current goal.
An exact proof term for the current goal is HInv0.
Let n be given.
Assume HnNat.
Assume HInvn.
An exact proof term for the current goal is (HInvS n HnNat HInvn).
We prove the intermediate claim HfOmega: ∀n : set, n ∈ ω → fval n ∈ ω.
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
An exact proof term for the current goal is (andEL (fval n ∈ ω) (apply_fun net0 (fval n) ∈ Ball n) (HInvAll n HnNat HnNat)).
We prove the intermediate claim HSubseqBall: ∀n : set, n ∈ ω → apply_fun subseq n ∈ Ball n.
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HnetIn: apply_fun net0 (fval n) ∈ Ball n.
An exact proof term for the current goal is (andER (fval n ∈ ω) (apply_fun net0 (fval n) ∈ Ball n) (HInvAll n HnNat HnNat)).
We prove the intermediate claim HdefNet: net0 = graph ω (λt : set ⇒ apply_fun seq t).
Use reflexivity.
We prove the intermediate claim HdefSub: subseq = graph ω (λt : set ⇒ apply_fun seq (apply_fun f t)).
Use reflexivity.
We prove the intermediate claim Hfapp: apply_fun f n = fval n.
rewrite the current goal using (apply_fun_graph ω fval n HnO) (from left to right).
Use reflexivity.
We prove the intermediate claim Hsubapp: apply_fun subseq n = apply_fun seq (fval n).
rewrite the current goal using HdefSub (from left to right).
rewrite the current goal using (apply_fun_graph ω (λt : set ⇒ apply_fun seq (apply_fun f t)) n HnO) (from left to right).
rewrite the current goal using Hfapp (from left to right).
Use reflexivity.
We prove the intermediate claim Hnetapp: apply_fun net0 (fval n) = apply_fun seq (fval n).
rewrite the current goal using HdefNet (from left to right).
Apply (apply_fun_graph ω (λt : set ⇒ apply_fun seq t) (fval n)) to the current goal.
An exact proof term for the current goal is (HfOmega n HnO).
rewrite the current goal using Hsubapp (from left to right).
rewrite the current goal using Hnetapp (from right to left).
An exact proof term for the current goal is HnetIn.
We prove the intermediate claim HfTot: total_function_on f ω ω.
An exact proof term for the current goal is (total_function_on_graph ω ω fval HfOmega).
We prove the intermediate claim HfFG: functional_graph f.
An exact proof term for the current goal is (functional_graph_graph ω fval).
We prove the intermediate claim HfDom: graph_domain_subset f ω.
An exact proof term for the current goal is (graph_domain_subset_graph ω fval).
We prove the intermediate claim HfStepSub: ∀n : set, nat_p n → ordsucc (fval n) ⊆ fval (ordsucc n).
Let n be given.
Assume HnNat: nat_p n.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (nat_p_omega n HnNat).
We prove the intermediate claim HfnO: fval n ∈ ω.
An exact proof term for the current goal is (HfOmega n HnO).
We prove the intermediate claim Hstep: StepPred n (fval n) (Step n (fval n)).
An exact proof term for the current goal is (HStepSpec n (fval n) HnO HfnO).
We prove the intermediate claim Hleft: (Step n (fval n)) ∈ ω ∧ ordsucc (fval n) ⊆ Step n (fval n).
An exact proof term for the current goal is (andEL ((Step n (fval n)) ∈ ω ∧ ordsucc (fval n) ⊆ Step n (fval n)) (apply_fun net0 (Step n (fval n)) ∈ Ball (ordsucc n)) Hstep).
We prove the intermediate claim Hsub: ordsucc (fval n) ⊆ Step n (fval n).
An exact proof term for the current goal is (andER ((Step n (fval n)) ∈ ω) (ordsucc (fval n) ⊆ Step n (fval n)) Hleft).
We will prove ordsucc (fval n) ⊆ fval (ordsucc n).
Let x be given.
Assume Hx: x ∈ ordsucc (fval n).
We will prove x ∈ fval (ordsucc n).
We prove the intermediate claim HxStep: x ∈ Step n (fval n).
An exact proof term for the current goal is (Hsub x Hx).
We prove the intermediate claim Heq: fval (ordsucc n) = Step n (fval n).
An exact proof term for the current goal is (nat_primrec_S base Step n HnNat).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HxStep.
We prove the intermediate claim HfInc: omega_strictly_increasing f.
We will prove omega_strictly_increasing f.
Let m and n be given.
Assume HmO: m ∈ ω.
Assume HnO: n ∈ ω.
Assume Hmn: m ∈ n.
We will prove apply_fun f m ∈ apply_fun f n.
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (omega_nat_p m HmO).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim Hfappm: apply_fun f m = fval m.
rewrite the current goal using (apply_fun_graph ω fval m HmO) (from left to right).
Use reflexivity.
We prove the intermediate claim Hfappn: apply_fun f n = fval n.
rewrite the current goal using (apply_fun_graph ω fval n HnO) (from left to right).
Use reflexivity.
rewrite the current goal using Hfappm (from left to right).
rewrite the current goal using Hfappn (from left to right).
Set P to be the term (λt : set ⇒ nat_p t → ∀s : set, s ∈ t → fval s ∈ fval t).
We prove the intermediate claim HP0: P 0.
Assume _.
Let s be given.
Assume Hs: s ∈ 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE s Hs).
We prove the intermediate claim HPS: ∀t : set, nat_p t → P t → P (ordsucc t).
Let t be given.
Assume HtNat: nat_p t.
Assume HPt: P t.
Assume HstNat: nat_p (ordsucc t).
Let s be given.
Assume Hs: s ∈ ordsucc t.
Apply (ordsuccE t s Hs) to the current goal.
Assume HsIn: s ∈ t.
We prove the intermediate claim Hslt: fval s ∈ fval t.
An exact proof term for the current goal is (HPt HtNat s HsIn).
We prove the intermediate claim HtO: t ∈ ω.
An exact proof term for the current goal is (nat_p_omega t HtNat).
We prove the intermediate claim HftO: fval t ∈ ω.
An exact proof term for the current goal is (HfOmega t HtO).
We prove the intermediate claim HftSuccO: fval (ordsucc t) ∈ ω.
An exact proof term for the current goal is (HfOmega (ordsucc t) (omega_ordsucc t HtO)).
We prove the intermediate claim Hsub: ordsucc (fval t) ⊆ fval (ordsucc t).
An exact proof term for the current goal is (HfStepSub t HtNat).
We prove the intermediate claim HftInSucc: fval t ∈ ordsucc (fval t).
An exact proof term for the current goal is (ordsuccI2 (fval t)).
We prove the intermediate claim HftIn: fval t ∈ fval (ordsucc t).
An exact proof term for the current goal is (Hsub (fval t) HftInSucc).
We prove the intermediate claim Htrans: TransSet (fval (ordsucc t)).
We prove the intermediate claim Hord: ordinal (fval (ordsucc t)).
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal (fval (ordsucc t)) HftSuccO).
An exact proof term for the current goal is (ordinal_TransSet (fval (ordsucc t)) Hord).
We prove the intermediate claim HtSub: fval t ⊆ fval (ordsucc t).
An exact proof term for the current goal is (Htrans (fval t) HftIn).
An exact proof term for the current goal is (HtSub (fval s) Hslt).
Assume Hseq: s = t.
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim HtO: t ∈ ω.
An exact proof term for the current goal is (nat_p_omega t HtNat).
We prove the intermediate claim HftO: fval t ∈ ω.
An exact proof term for the current goal is (HfOmega t HtO).
We prove the intermediate claim Hsub: ordsucc (fval t) ⊆ fval (ordsucc t).
An exact proof term for the current goal is (HfStepSub t HtNat).
We prove the intermediate claim HftInSucc: fval t ∈ ordsucc (fval t).
An exact proof term for the current goal is (ordsuccI2 (fval t)).
An exact proof term for the current goal is (Hsub (fval t) HftInSucc).
We prove the intermediate claim HPn: P n.
An exact proof term for the current goal is (nat_ind P HP0 HPS n HnNat).
An exact proof term for the current goal is (HPn HnNat m Hmn).
We use subseq to witness the existential quantifier.
We use x0 to witness the existential quantifier.
Apply andI to the current goal.
We will prove subsequence_of seq subseq.
We will prove ∃f0 : set, total_function_on f0 ω ω ∧ functional_graph f0 ∧ graph_domain_subset f0 ω ∧ omega_strictly_increasing f0 ∧ subseq = compose_fun ω f0 seq.
We use f to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is HfTot.
An exact proof term for the current goal is HfFG.
An exact proof term for the current goal is HfDom.
An exact proof term for the current goal is HfInc.
Use reflexivity.
We will prove converges_to X Tx subseq x0.
We will prove topology_on X Tx ∧ sequence_on subseq X ∧ x0 ∈ X ∧ ∀U : set, U ∈ Tx → x0 ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun subseq n ∈ U.
Apply and4I to the current goal.
An exact proof term for the current goal is HTx.
We will prove sequence_on subseq X.
We prove the intermediate claim HfFun: function_on f ω ω.
An exact proof term for the current goal is (total_function_on_function_on f ω ω HfTot).
We prove the intermediate claim HsubFun: function_on subseq ω X.
An exact proof term for the current goal is (function_on_compose_fun ω ω X f seq HfFun Hseq).
An exact proof term for the current goal is HsubFun.
An exact proof term for the current goal is Hx0X.
Let U be given.
Assume HU: U ∈ Tx.
Assume Hx0U: x0 ∈ U.
We will prove ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun subseq n ∈ U.
Set B0 to be the term famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HBasis: basis_on X B0.
An exact proof term for the current goal is (open_balls_form_basis X d Hd).
We prove the intermediate claim HBgen: generated_topology X B0 = Tx.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology X B0.
rewrite the current goal using HBgen (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim Hexb0: ∃b0 ∈ B0, x0 ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (generated_topology_local_refine X B0 U x0 HUgen Hx0U).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B0: b0 ∈ B0.
An exact proof term for the current goal is (andEL (b0 ∈ B0) (x0 ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hb0rest: x0 ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (andER (b0 ∈ B0) (x0 ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hx0b0: x0 ∈ b0.
An exact proof term for the current goal is (andEL (x0 ∈ b0) (b0 ⊆ U) Hb0rest).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (x0 ∈ b0) (b0 ⊆ U) Hb0rest).
We prove the intermediate claim HexBall: ∃r : set, r ∈ R ∧ Rlt 0 r ∧ open_ball X d x0 r ⊆ U.
Apply (famunionE_impred X (λc : set ⇒ {open_ball X d c r0|r0 ∈ R, Rlt 0 r0}) b0 Hb0B0 (∃r : set, r ∈ R ∧ Rlt 0 r ∧ open_ball X d x0 r ⊆ U)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume Hb0In: b0 ∈ {open_ball X d c r0|r0 ∈ R, Rlt 0 r0}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c r0) b0 Hb0In (∃r : set, r ∈ R ∧ Rlt 0 r ∧ open_ball X d x0 r ⊆ U)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hb0eq: b0 = open_ball X d c r0.
We prove the intermediate claim Hx0inBall0: x0 ∈ open_ball X d c r0.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hx0b0.
We prove the intermediate claim Hball0subU: open_ball X d c r0 ⊆ U.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hb0subU.
We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d x0 s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (open_ball_refine_center X d c x0 r0 Hd HcX Hx0X Hr0R Hr0pos Hx0inBall0).
Apply Hexs to the current goal.
Let s be given.
Assume Hspack.
We prove the intermediate claim Hs12: s ∈ R ∧ Rlt 0 s.
An exact proof term for the current goal is (andEL (s ∈ R ∧ Rlt 0 s) (open_ball X d x0 s ⊆ open_ball X d c r0) Hspack).
We prove the intermediate claim HsubBall: open_ball X d x0 s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball X d x0 s ⊆ open_ball X d c r0) Hspack).
We prove the intermediate claim HsubU: open_ball X d x0 s ⊆ U.
An exact proof term for the current goal is (Subq_tra (open_ball X d x0 s) (open_ball X d c r0) U HsubBall Hball0subU).
We use s to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hs12.
An exact proof term for the current goal is HsubU.
Apply HexBall to the current goal.
Let r be given.
Assume Hrpack.
We prove the intermediate claim Hr12: r ∈ R ∧ Rlt 0 r.
An exact proof term for the current goal is (andEL (r ∈ R ∧ Rlt 0 r) (open_ball X d x0 r ⊆ U) Hrpack).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r) Hr12).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r) Hr12).
We prove the intermediate claim HballsubU: open_ball X d x0 r ⊆ U.
An exact proof term for the current goal is (andER (r ∈ R ∧ Rlt 0 r) (open_ball X d x0 r ⊆ U) Hrpack).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) r.
An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt r HrR Hrpos).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (Rlt (inv_nat (ordsucc N)) r) HNpack).
We prove the intermediate claim HinvLt: Rlt (inv_nat (ordsucc N)) r.
An exact proof term for the current goal is (andER (N ∈ ω) (Rlt (inv_nat (ordsucc N)) r) HNpack).
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNO.
Let n be given.
Assume HnO: n ∈ ω.
Assume HNsubn: N ⊆ n.
We will prove apply_fun subseq n ∈ U.
We prove the intermediate claim HsubnBalln: apply_fun subseq n ∈ Ball n.
An exact proof term for the current goal is (HSubseqBall n HnO).
We prove the intermediate claim HBallNsubU: Ball N ⊆ U.
An exact proof term for the current goal is (Subq_tra (Ball N) (open_ball X d x0 r) U (open_ball_radius_mono X d x0 (inv_nat (ordsucc N)) r HinvLt) HballsubU).
We prove the intermediate claim HBallnsubBallN: Ball n ⊆ Ball N.
Apply (xm (n = N)) to the current goal.
Assume HnEq: n = N.
rewrite the current goal using HnEq (from left to right).
An exact proof term for the current goal is (Subq_ref (Ball N)).
Assume HnNe: ¬ (n = N).
We prove the intermediate claim HordN: ordinal N.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal N HNO).
We prove the intermediate claim Hordn: ordinal n.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n HnO).
We prove the intermediate claim HNin: N ∈ n.
Apply (ordinal_trichotomy_or_impred N n HordN Hordn (N ∈ n)) to the current goal.
Assume H: N ∈ n.
An exact proof term for the current goal is H.
Assume Heq: N = n.
Apply FalseE to the current goal.
We prove the intermediate claim HnEq: n = N.
Use symmetry.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HnNe HnEq).
Assume HnIn: n ∈ N.
We prove the intermediate claim HtN: TransSet N.
An exact proof term for the current goal is (ordinal_TransSet N HordN).
We prove the intermediate claim HnSubN: n ⊆ N.
An exact proof term for the current goal is (HtN n HnIn).
We prove the intermediate claim HNeq: N = n.
An exact proof term for the current goal is (set_ext N n HNsubn HnSubN).
Apply FalseE to the current goal.
We prove the intermediate claim HnEq: n = N.
Use symmetry.
An exact proof term for the current goal is HNeq.
An exact proof term for the current goal is (HnNe HnEq).
We prove the intermediate claim HinvLt2: Rlt (inv_nat (ordsucc n)) (inv_nat (ordsucc N)).
An exact proof term for the current goal is (inv_nat_ordsucc_antitone_local2 N n HNO HnO HNin).
An exact proof term for the current goal is (open_ball_radius_mono X d x0 (inv_nat (ordsucc n)) (inv_nat (ordsucc N)) HinvLt2).
We prove the intermediate claim HsubnBallN: apply_fun subseq n ∈ Ball N.
An exact proof term for the current goal is (HBallnsubBallN (apply_fun subseq n) HsubnBalln).
An exact proof term for the current goal is (HBallNsubU (apply_fun subseq n) HsubnBallN).
∎