Let X, Tx, Y, Ty and f be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
We will prove continuous_map X Tx Y Ty f → ∀x seq : set, sequence_on seq X → converges_to X Tx seq x → converges_to Y Ty (map_sequence f seq) (apply_fun f x).
Assume Hcont: continuous_map X Tx Y Ty f.
Let x and seq be given.
Assume Hseqon: sequence_on seq X.
Assume Hconv: converges_to X Tx seq x.
We will prove converges_to Y Ty (map_sequence f seq) (apply_fun f x).
We prove the intermediate claim Hcont_left: (topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y.
An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hcont).
We prove the intermediate claim Hfun: function_on f X Y.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) Hcont_left).
We prove the intermediate claim Hpre: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (andER ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hcont).
We prove the intermediate claim Hconv_left: (topology_on X Tx ∧ sequence_on seq X) ∧ x ∈ X.
An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ sequence_on seq X) ∧ x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U) Hconv).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ sequence_on seq X) (x ∈ X) Hconv_left).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfun x HxX).
We will prove topology_on Y Ty ∧ sequence_on (map_sequence f seq) Y ∧ apply_fun f x ∈ Y ∧ ∀V : set, V ∈ Ty → apply_fun f x ∈ V → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun (map_sequence f seq) n ∈ V.
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 HTy.
We will prove sequence_on (map_sequence f seq) Y.
Let n be given.
Assume Hn: n ∈ ω.
We will prove apply_fun (map_sequence f seq) n ∈ Y.
We prove the intermediate claim HseqnX: apply_fun seq n ∈ X.
An exact proof term for the current goal is (Hseqon n Hn).
We prove the intermediate claim Hcomp: apply_fun (map_sequence f seq) n = apply_fun f (apply_fun seq n).
An exact proof term for the current goal is (compose_fun_apply ω seq f n Hn).
rewrite the current goal using Hcomp (from left to right).
An exact proof term for the current goal is (Hfun (apply_fun seq n) HseqnX).
An exact proof term for the current goal is HfxY.
Let V be given.
Assume HV: V ∈ Ty.
Assume HfxV: apply_fun f x ∈ V.
Set U to be the term preimage_of X f V.
We prove the intermediate claim HUDef: U = preimage_of X f V.
Use reflexivity.
We prove the intermediate claim HUopen: U ∈ Tx.
rewrite the current goal using HUDef (from left to right).
An exact proof term for the current goal is (Hpre V HV).
We prove the intermediate claim HxU: x ∈ U.
rewrite the current goal using HUDef (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxX HfxV).
We prove the intermediate claim Htail0: ∀W : set, W ∈ Tx → x ∈ W → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ W.
An exact proof term for the current goal is (andER ((topology_on X Tx ∧ sequence_on seq X) ∧ x ∈ X) (∀W : set, W ∈ Tx → x ∈ W → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ W) Hconv).
We prove the intermediate claim Hevent: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
An exact proof term for the current goal is (Htail0 U HUopen HxU).
Apply Hevent 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 → apply_fun seq n ∈ U) HNpair).
We prove the intermediate claim Htail: ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U) HNpair).
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 Hn: n ∈ ω.
Assume HNsub: N ⊆ n.
We prove the intermediate claim HseqnU: apply_fun seq n ∈ U.
An exact proof term for the current goal is (Htail n Hn HNsub).
We prove the intermediate claim HseqnU0: apply_fun seq n ∈ preimage_of X f V.
rewrite the current goal using HUDef (from right to left).
An exact proof term for the current goal is HseqnU.
We prove the intermediate claim HfnV: apply_fun f (apply_fun seq n) ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ V) (apply_fun seq n) HseqnU0).
We prove the intermediate claim Hcomp: apply_fun (map_sequence f seq) n = apply_fun f (apply_fun seq n).
An exact proof term for the current goal is (compose_fun_apply ω seq f n Hn).
rewrite the current goal using Hcomp (from left to right).
An exact proof term for the current goal is HfnV.
∎