Let X, dX, Y, dY and f be given.
Assume HdX: metric_on X dX.
Assume HdY: metric_on Y dY.
Assume Hf: function_on f X Y.
We will prove continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f ↔ ∀seq x : set, sequence_converges_metric X dX seq x → sequence_converges_metric Y dY ({(n,apply_fun f (apply_fun seq n))|n ∈ ω}) (apply_fun f x).
Apply iffI to the current goal.
Assume Hcont: continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f.
Let seq and x be given.
Assume Hseq: sequence_converges_metric X dX seq x.
We will prove sequence_converges_metric Y dY ({(n,apply_fun f (apply_fun seq n))|n ∈ ω}) (apply_fun f x).
Set seqY to be the term {(n,apply_fun f (apply_fun seq n))|n ∈ ω}.
We prove the intermediate claim Hseqon: sequence_on seq X.
An exact proof term for the current goal is (sequence_converges_metric_sequence_on X dX seq x Hseq).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (sequence_converges_metric_point_in_X X dX seq x Hseq).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hf x HxX).
We prove the intermediate claim HseqYfun: function_on seqY ω Y.
Let n be given.
Assume Hnomega: n ∈ ω.
We prove the intermediate claim Hseqfun: function_on seq ω X.
An exact proof term for the current goal is Hseqon.
We prove the intermediate claim HseqnX: apply_fun seq n ∈ X.
An exact proof term for the current goal is (Hseqfun n Hnomega).
We prove the intermediate claim HfseqnY: apply_fun f (apply_fun seq n) ∈ Y.
An exact proof term for the current goal is (Hf (apply_fun seq n) HseqnX).
We prove the intermediate claim Hfunc: functional_graph seqY.
An exact proof term for the current goal is (functional_graph_graph ω (λn0 : set ⇒ apply_fun f (apply_fun seq n0))).
We prove the intermediate claim HpairIn: (n,apply_fun f (apply_fun seq n)) ∈ seqY.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ (n0,apply_fun f (apply_fun seq n0))) n Hnomega).
We prove the intermediate claim Happ: apply_fun seqY n = apply_fun f (apply_fun seq n).
An exact proof term for the current goal is (functional_graph_apply_fun_eq seqY n (apply_fun f (apply_fun seq n)) Hfunc HpairIn).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HfseqnY.
We prove the intermediate claim HseqYon: sequence_on seqY Y.
An exact proof term for the current goal is HseqYfun.
We will prove sequence_converges_metric Y dY seqY (apply_fun f x).
We will prove (metric_on Y dY ∧ sequence_on seqY Y) ∧ (apply_fun f x ∈ Y) ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun dY (apply_fun seqY n,apply_fun f x)) eps.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HdY.
An exact proof term for the current goal is HseqYon.
An exact proof term for the current goal is HfxY.
Let eps be given.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
We prove the intermediate claim Hedcont: ∀x0 : set, x0 ∈ X → ∀eps0 : set, eps0 ∈ R ∧ Rlt 0 eps0 → ∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x1 : set, x1 ∈ X → Rlt (apply_fun dX (x1,x0)) delta → Rlt (apply_fun dY (apply_fun f x1,apply_fun f x0)) eps0).
An exact proof term for the current goal is (iffEL (continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f) (∀x0 : set, x0 ∈ X → ∀eps0 : set, eps0 ∈ R ∧ Rlt 0 eps0 → ∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x1 : set, x1 ∈ X → Rlt (apply_fun dX (x1,x0)) delta → Rlt (apply_fun dY (apply_fun f x1,apply_fun f x0)) eps0)) (metric_epsilon_delta_continuity X dX Y dY f HdX HdY Hf) Hcont).
Apply (Hedcont x HxX eps Heps) to the current goal.
Let delta be given.
Assume Hdelta.
We prove the intermediate claim Hdelta12: delta ∈ R ∧ Rlt 0 delta.
An exact proof term for the current goal is (andEL (delta ∈ R ∧ Rlt 0 delta) (∀x1 : set, x1 ∈ X → Rlt (apply_fun dX (x1,x)) delta → Rlt (apply_fun dY (apply_fun f x1,apply_fun f x)) eps) Hdelta).
We prove the intermediate claim HdeltaImp: ∀x1 : set, x1 ∈ X → Rlt (apply_fun dX (x1,x)) delta → Rlt (apply_fun dY (apply_fun f x1,apply_fun f x)) eps.
An exact proof term for the current goal is (andER (delta ∈ R ∧ Rlt 0 delta) (∀x1 : set, x1 ∈ X → Rlt (apply_fun dX (x1,x)) delta → Rlt (apply_fun dY (apply_fun f x1,apply_fun f x)) eps) Hdelta).
Apply (sequence_converges_metric_eps X dX seq x Hseq delta Hdelta12) to the current goal.
Let N be given.
Assume HNpair.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun dX (apply_fun seq n,x)) delta) HNpair).
Let n be given.
Assume Hnomega: n ∈ ω.
Assume HNsubn: N ⊆ n.
We prove the intermediate claim HNprop: ∀n0 : set, n0 ∈ ω → N ⊆ n0 → Rlt (apply_fun dX (apply_fun seq n0,x)) delta.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n0 : set, n0 ∈ ω → N ⊆ n0 → Rlt (apply_fun dX (apply_fun seq n0,x)) delta) HNpair).
We prove the intermediate claim Hdx: Rlt (apply_fun dX (apply_fun seq n,x)) delta.
An exact proof term for the current goal is (HNprop n Hnomega HNsubn).
We prove the intermediate claim Hseqfun: function_on seq ω X.
An exact proof term for the current goal is Hseqon.
We prove the intermediate claim HseqnX: apply_fun seq n ∈ X.
An exact proof term for the current goal is (Hseqfun n Hnomega).
We prove the intermediate claim Hdy: Rlt (apply_fun dY (apply_fun f (apply_fun seq n),apply_fun f x)) eps.
An exact proof term for the current goal is (HdeltaImp (apply_fun seq n) HseqnX Hdx).
We prove the intermediate claim Hfunc: functional_graph seqY.
An exact proof term for the current goal is (functional_graph_graph ω (λn0 : set ⇒ apply_fun f (apply_fun seq n0))).
We prove the intermediate claim HpairIn: (n,apply_fun f (apply_fun seq n)) ∈ seqY.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ (n0,apply_fun f (apply_fun seq n0))) n Hnomega).
We prove the intermediate claim Happ: apply_fun seqY n = apply_fun f (apply_fun seq n).
An exact proof term for the current goal is (functional_graph_apply_fun_eq seqY n (apply_fun f (apply_fun seq n)) Hfunc HpairIn).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is Hdy.
Assume Hseqcont: ∀seq x : set, sequence_converges_metric X dX seq x → sequence_converges_metric Y dY ({(n,apply_fun f (apply_fun seq n))|n ∈ ω}) (apply_fun f x).
We will prove continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f.
We prove the intermediate claim Hed: ∀x0 : set, x0 ∈ X → ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps).
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Let eps be given.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
Apply dneg to the current goal.
Assume Hno: ¬ (∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps)).
We will prove False.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim Hepspos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim Hbad: ∀delta : set, delta ∈ R ∧ Rlt 0 delta → ∃x : set, x ∈ X ∧ Rlt (apply_fun dX (x,x0)) delta ∧ ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps).
Let delta be given.
Assume Hdelta: delta ∈ R ∧ Rlt 0 delta.
Apply dneg to the current goal.
Assume Hnobad: ¬ (∃x : set, x ∈ X ∧ Rlt (apply_fun dX (x,x0)) delta ∧ ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps)).
We will prove False.
Apply Hno to the current goal.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hdelta.
Let x be given.
Assume HxX: x ∈ X.
Assume Hdx: Rlt (apply_fun dX (x,x0)) delta.
Apply dneg to the current goal.
Assume HnRlt: ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps).
We will prove False.
Apply Hnobad to the current goal.
We use x to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is Hdx.
An exact proof term for the current goal is HnRlt.
Set g to be the term λn : set ⇒ Eps_i (λx : set ⇒ x ∈ X ∧ Rlt (apply_fun dX (x,x0)) (eps_ n) ∧ ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps)).
Set seq to be the term {(n,g n)|n ∈ ω}.
We prove the intermediate claim Hseqfun: function_on seq ω X.
We prove the intermediate claim HgAll: ∀n : set, n ∈ ω → g n ∈ X.
Let n be given.
Assume Hnomega: n ∈ ω.
We prove the intermediate claim Hgnreal: eps_ n ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ n) (SNo_eps_SNoS_omega n Hnomega)).
We prove the intermediate claim HgnposS: 0 < eps_ n.
An exact proof term for the current goal is (SNo_eps_pos n Hnomega).
We prove the intermediate claim Hgnpos: Rlt 0 (eps_ n).
An exact proof term for the current goal is (RltI 0 (eps_ n) real_0 Hgnreal HgnposS).
We prove the intermediate claim Hexbad: ∃x : set, x ∈ X ∧ Rlt (apply_fun dX (x,x0)) (eps_ n) ∧ ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps).
An exact proof term for the current goal is (Hbad (eps_ n) (andI (eps_ n ∈ R) (Rlt 0 (eps_ n)) Hgnreal Hgnpos)).
We prove the intermediate claim Hgprop: g n ∈ X ∧ Rlt (apply_fun dX (g n,x0)) (eps_ n) ∧ ¬ (Rlt (apply_fun dY (apply_fun f (g n),apply_fun f x0)) eps).
An exact proof term for the current goal is (Eps_i_ex (λx : set ⇒ x ∈ X ∧ Rlt (apply_fun dX (x,x0)) (eps_ n) ∧ ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps)) Hexbad).
We prove the intermediate claim Hg12: g n ∈ X ∧ Rlt (apply_fun dX (g n,x0)) (eps_ n).
An exact proof term for the current goal is (andEL (g n ∈ X ∧ Rlt (apply_fun dX (g n,x0)) (eps_ n)) (¬ (Rlt (apply_fun dY (apply_fun f (g n),apply_fun f x0)) eps)) Hgprop).
An exact proof term for the current goal is (andEL (g n ∈ X) (Rlt (apply_fun dX (g n,x0)) (eps_ n)) Hg12).
We prove the intermediate claim Hrng: graph_range_subset seq X.
An exact proof term for the current goal is (graph_range_subset_graph ω X (λn0 : set ⇒ g n0) HgAll).
Let n be given.
Assume Hnomega: n ∈ ω.
We prove the intermediate claim HpairIn: (n,g n) ∈ seq.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ (n0,g n0)) n Hnomega).
We prove the intermediate claim HpairApp: (n,apply_fun seq n) ∈ seq.
An exact proof term for the current goal is (Eps_i_ax (λy0 : set ⇒ (n,y0) ∈ seq) (g n) HpairIn).
An exact proof term for the current goal is (Hrng n (apply_fun seq n) HpairApp).
We prove the intermediate claim Hseqconv: sequence_converges_metric X dX seq x0.
We will prove (metric_on X dX ∧ sequence_on seq X) ∧ x0 ∈ X ∧ ∀eps0 : set, eps0 ∈ R ∧ Rlt 0 eps0 → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun dX (apply_fun seq n,x0)) eps0.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HdX.
An exact proof term for the current goal is Hseqfun.
An exact proof term for the current goal is Hx0X.
Let eps0 be given.
Assume Heps0: eps0 ∈ R ∧ Rlt 0 eps0.
We prove the intermediate claim Heps0R: eps0 ∈ R.
An exact proof term for the current goal is (andEL (eps0 ∈ R) (Rlt 0 eps0) Heps0).
We prove the intermediate claim Heps0pos: Rlt 0 eps0.
An exact proof term for the current goal is (andER (eps0 ∈ R) (Rlt 0 eps0) Heps0).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < eps0.
An exact proof term for the current goal is (exists_eps_lt_pos eps0 Heps0R Heps0pos).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < eps0) HNpair).
We prove the intermediate claim HepsNlt: eps_ N < eps0.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < eps0) HNpair).
We prove the intermediate claim HepsNR: eps_ N ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim HepsNltR: Rlt (eps_ N) eps0.
An exact proof term for the current goal is (RltI (eps_ N) eps0 HepsNR Heps0R HepsNlt).
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNomega.
Let n be given.
Assume Hnomega: n ∈ ω.
Assume HNsubn: N ⊆ n.
We prove the intermediate claim HepsnR: eps_ n ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ n) (SNo_eps_SNoS_omega n Hnomega)).
We prove the intermediate claim HordN: ordinal N.
An exact proof term for the current goal is (nat_p_ordinal N (omega_nat_p N HNomega)).
We prove the intermediate claim Hordn: ordinal n.
An exact proof term for the current goal is (nat_p_ordinal n (omega_nat_p n Hnomega)).
We prove the intermediate claim Hnot_nInN: ¬ (n ∈ N).
Assume HninN: n ∈ N.
We prove the intermediate claim Hnn: n ∈ n.
An exact proof term for the current goal is (HNsubn n HninN).
An exact proof term for the current goal is ((In_irref n) Hnn).
We prove the intermediate claim Hfunc: functional_graph seq.
An exact proof term for the current goal is (functional_graph_graph ω (λn0 : set ⇒ g n0)).
We prove the intermediate claim HpairIn: (n,g n) ∈ seq.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ (n0,g n0)) n Hnomega).
We prove the intermediate claim Happ: apply_fun seq n = g n.
An exact proof term for the current goal is (functional_graph_apply_fun_eq seq n (g n) Hfunc HpairIn).
We prove the intermediate claim HgnposS: 0 < eps_ n.
An exact proof term for the current goal is (SNo_eps_pos n Hnomega).
We prove the intermediate claim Hgnpos: Rlt 0 (eps_ n).
An exact proof term for the current goal is (RltI 0 (eps_ n) real_0 HepsnR HgnposS).
We prove the intermediate claim Hexbad: ∃x : set, x ∈ X ∧ Rlt (apply_fun dX (x,x0)) (eps_ n) ∧ ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps).
An exact proof term for the current goal is (Hbad (eps_ n) (andI (eps_ n ∈ R) (Rlt 0 (eps_ n)) HepsnR Hgnpos)).
We prove the intermediate claim Hgprop: g n ∈ X ∧ Rlt (apply_fun dX (g n,x0)) (eps_ n) ∧ ¬ (Rlt (apply_fun dY (apply_fun f (g n),apply_fun f x0)) eps).
An exact proof term for the current goal is (Eps_i_ex (λx : set ⇒ x ∈ X ∧ Rlt (apply_fun dX (x,x0)) (eps_ n) ∧ ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps)) Hexbad).
We prove the intermediate claim Hg12: g n ∈ X ∧ Rlt (apply_fun dX (g n,x0)) (eps_ n).
An exact proof term for the current goal is (andEL (g n ∈ X ∧ Rlt (apply_fun dX (g n,x0)) (eps_ n)) (¬ (Rlt (apply_fun dY (apply_fun f (g n),apply_fun f x0)) eps)) Hgprop).
We prove the intermediate claim Hdxlt_epsn: Rlt (apply_fun dX (g n,x0)) (eps_ n).
An exact proof term for the current goal is (andER (g n ∈ X) (Rlt (apply_fun dX (g n,x0)) (eps_ n)) Hg12).
We prove the intermediate claim Hdxlt_epsn2: Rlt (apply_fun dX (apply_fun seq n,x0)) (eps_ n).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is Hdxlt_epsn.
We prove the intermediate claim Hepsnlt_eps0: Rlt (eps_ n) eps0.
Apply (ordinal_trichotomy_or_impred N n HordN Hordn (Rlt (eps_ n) eps0)) to the current goal.
Assume HNin: N ∈ n.
We prove the intermediate claim Hepsnlt_epsN: eps_ n < eps_ N.
An exact proof term for the current goal is (SNo_eps_decr n Hnomega N HNin).
We prove the intermediate claim Hepsnlt_epsNR: Rlt (eps_ n) (eps_ N).
An exact proof term for the current goal is (RltI (eps_ n) (eps_ N) HepsnR HepsNR Hepsnlt_epsN).
An exact proof term for the current goal is (Rlt_tra (eps_ n) (eps_ N) eps0 Hepsnlt_epsNR HepsNltR).
Assume Heq: N = n.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HepsNltR.
Assume HninN: n ∈ N.
Apply FalseE to the current goal.
We will prove False.
An exact proof term for the current goal is (Hnot_nInN HninN).
An exact proof term for the current goal is (Rlt_tra (apply_fun dX (apply_fun seq n,x0)) (eps_ n) eps0 Hdxlt_epsn2 Hepsnlt_eps0).
Set seqY to be the term {(n,apply_fun f (apply_fun seq n))|n ∈ ω}.
We prove the intermediate claim Himgconv: sequence_converges_metric Y dY seqY (apply_fun f x0).
An exact proof term for the current goal is (Hseqcont seq x0 Hseqconv).
We prove the intermediate claim HexNimg: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun dY (apply_fun seqY n,apply_fun f x0)) eps.
An exact proof term for the current goal is (sequence_converges_metric_eps Y dY seqY (apply_fun f x0) Himgconv eps Heps).
Apply HexNimg to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun dY (apply_fun seqY n,apply_fun f x0)) eps) HNpair).
We prove the intermediate claim HNprop: ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun dY (apply_fun seqY n,apply_fun f x0)) eps.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun dY (apply_fun seqY n,apply_fun f x0)) eps) HNpair).
We prove the intermediate claim HNsubN: N ⊆ N.
An exact proof term for the current goal is (Subq_ref N).
We prove the intermediate claim Hdylt: Rlt (apply_fun dY (apply_fun seqY N,apply_fun f x0)) eps.
An exact proof term for the current goal is (HNprop N HNomega HNsubN).
We prove the intermediate claim HfuncY: functional_graph seqY.
An exact proof term for the current goal is (functional_graph_graph ω (λn0 : set ⇒ apply_fun f (apply_fun seq n0))).
We prove the intermediate claim HpairY: (N,apply_fun f (apply_fun seq N)) ∈ seqY.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ (n0,apply_fun f (apply_fun seq n0))) N HNomega).
We prove the intermediate claim HappY: apply_fun seqY N = apply_fun f (apply_fun seq N).
An exact proof term for the current goal is (functional_graph_apply_fun_eq seqY N (apply_fun f (apply_fun seq N)) HfuncY HpairY).
We prove the intermediate claim HfuncX: functional_graph seq.
An exact proof term for the current goal is (functional_graph_graph ω (λn0 : set ⇒ g n0)).
We prove the intermediate claim HpairX: (N,g N) ∈ seq.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ (n0,g n0)) N HNomega).
We prove the intermediate claim HappX: apply_fun seq N = g N.
An exact proof term for the current goal is (functional_graph_apply_fun_eq seq N (g N) HfuncX HpairX).
We prove the intermediate claim Hgnreal: eps_ N ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim HgnposS: 0 < eps_ N.
An exact proof term for the current goal is (SNo_eps_pos N HNomega).
We prove the intermediate claim Hgnpos: Rlt 0 (eps_ N).
An exact proof term for the current goal is (RltI 0 (eps_ N) real_0 Hgnreal HgnposS).
We prove the intermediate claim Hexbad: ∃x : set, x ∈ X ∧ Rlt (apply_fun dX (x,x0)) (eps_ N) ∧ ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps).
An exact proof term for the current goal is (Hbad (eps_ N) (andI (eps_ N ∈ R) (Rlt 0 (eps_ N)) Hgnreal Hgnpos)).
We prove the intermediate claim Hgprop: g N ∈ X ∧ Rlt (apply_fun dX (g N,x0)) (eps_ N) ∧ ¬ (Rlt (apply_fun dY (apply_fun f (g N),apply_fun f x0)) eps).
An exact proof term for the current goal is (Eps_i_ex (λx : set ⇒ x ∈ X ∧ Rlt (apply_fun dX (x,x0)) (eps_ N) ∧ ¬ (Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps)) Hexbad).
We prove the intermediate claim Hnot: ¬ (Rlt (apply_fun dY (apply_fun f (g N),apply_fun f x0)) eps).
An exact proof term for the current goal is (andER (g N ∈ X ∧ Rlt (apply_fun dX (g N,x0)) (eps_ N)) (¬ (Rlt (apply_fun dY (apply_fun f (g N),apply_fun f x0)) eps)) Hgprop).
We prove the intermediate claim Hdylt2: Rlt (apply_fun dY (apply_fun f (g N),apply_fun f x0)) eps.
We prove the intermediate claim HeqY: apply_fun seqY N = apply_fun f (g N).
rewrite the current goal using HappY (from left to right).
rewrite the current goal using HappX (from left to right).
Use reflexivity.
rewrite the current goal using HeqY (from right to left) at position 1.
An exact proof term for the current goal is Hdylt.
An exact proof term for the current goal is (Hnot Hdylt2).
An exact proof term for the current goal is (iffER (continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f) (∀x0 : set, x0 ∈ X → ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps)) (metric_epsilon_delta_continuity X dX Y dY f HdX HdY Hf) Hed).
∎