Let X, Tx and A be given.
Assume Hnorm: normal_space X Tx.
Assume HAcl: closed_in X Tx A.
Assume HGd: Gdelta_simple X Tx A.
We will prove ∃f : set, continuous_map X Tx unit_interval unit_interval_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → x ∉ A → Rlt 0 (apply_fun f x)).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
Apply HGd to the current goal.
Let Fam be given.
Assume Hpack: countable_set Fam ∧ Fam ⊆ Tx ∧ A = intersection_of_family X Fam.
We prove the intermediate claim Hpair: countable_set Fam ∧ Fam ⊆ Tx.
An exact proof term for the current goal is (andEL (countable_set Fam ∧ Fam ⊆ Tx) (A = intersection_of_family X Fam) Hpack).
We prove the intermediate claim HAEq: A = intersection_of_family X Fam.
An exact proof term for the current goal is (andER (countable_set Fam ∧ Fam ⊆ Tx) (A = intersection_of_family X Fam) Hpack).
We prove the intermediate claim Hcount: countable_set Fam.
An exact proof term for the current goal is (andEL (countable_set Fam) (Fam ⊆ Tx) Hpair).
We prove the intermediate claim HFsub: Fam ⊆ Tx.
An exact proof term for the current goal is (andER (countable_set Fam) (Fam ⊆ Tx) Hpair).
Apply Hcount to the current goal.
Let i of type set → set be given.
Assume Hiinj: inj Fam ω i.
We prove the intermediate claim Hi_to_omega: ∀U ∈ Fam, i U ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ Fam, i u ∈ ω) (∀u v ∈ Fam, i u = i v → u = v) Hiinj).
We prove the intermediate claim Hi_inj: ∀U V ∈ Fam, i U = i V → U = V.
An exact proof term for the current goal is (andER (∀u ∈ Fam, i u ∈ ω) (∀u v ∈ Fam, i u = i v → u = v) Hiinj).
Set U_of to be the term (λn : set ⇒ if (∃U : set, U ∈ Fam ∧ i U = n) then (Eps_i (λU : set ⇒ U ∈ Fam ∧ i U = n)) else X).
We prove the intermediate claim HU_of_in_Tx: ∀n : set, n ∈ ω → U_of n ∈ Tx.
Let n be given.
Assume HnO: n ∈ ω.
Apply (xm (∃U : set, U ∈ Fam ∧ i U = n)) to the current goal.
Assume HexU: ∃U : set, U ∈ Fam ∧ i U = n.
Set P to be the term (λU : set ⇒ U ∈ Fam ∧ i U = n).
We prove the intermediate claim HP: P (Eps_i P).
Apply HexU to the current goal.
Let U be given.
Assume HPU: U ∈ Fam ∧ i U = n.
An exact proof term for the current goal is (Eps_i_ax P U HPU).
We prove the intermediate claim HUinFam: (Eps_i P) ∈ Fam.
An exact proof term for the current goal is (andEL ((Eps_i P) ∈ Fam) (i (Eps_i P) = n) HP).
We prove the intermediate claim HUeq: U_of n = Eps_i P.
We prove the intermediate claim HUdef: U_of n = if (∃U : set, U ∈ Fam ∧ i U = n) then (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n)) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
rewrite the current goal using (If_i_1 (∃U : set, U ∈ Fam ∧ i U = n) (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n)) X HexU) (from left to right).
Use reflexivity.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (HFsub (Eps_i P) HUinFam).
Assume HnexU: ¬ (∃U : set, U ∈ Fam ∧ i U = n).
We prove the intermediate claim HUeq: U_of n = X.
We prove the intermediate claim HUdef: U_of n = if (∃U : set, U ∈ Fam ∧ i U = n) then (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n)) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
rewrite the current goal using (If_i_0 (∃U : set, U ∈ Fam ∧ i U = n) (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n)) X HnexU) (from left to right).
Use reflexivity.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HA_sub_Uof: ∀n : set, n ∈ ω → A ⊆ U_of n.
Let n be given.
Assume HnO: n ∈ ω.
Let x be given.
Assume HxA: x ∈ A.
We will prove x ∈ U_of n.
Apply (xm (∃U : set, U ∈ Fam ∧ i U = n)) to the current goal.
Assume HexU: ∃U : set, U ∈ Fam ∧ i U = n.
Set P to be the term (λU : set ⇒ U ∈ Fam ∧ i U = n).
We prove the intermediate claim HP: P (Eps_i P).
Apply HexU to the current goal.
Let U be given.
Assume HPU: U ∈ Fam ∧ i U = n.
An exact proof term for the current goal is (Eps_i_ax P U HPU).
We prove the intermediate claim HUinFam: (Eps_i P) ∈ Fam.
An exact proof term for the current goal is (andEL ((Eps_i P) ∈ Fam) (i (Eps_i P) = n) HP).
We prove the intermediate claim HUeq: U_of n = Eps_i P.
We prove the intermediate claim HUdef: U_of n = if (∃U : set, U ∈ Fam ∧ i U = n) then (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n)) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
rewrite the current goal using (If_i_1 (∃U : set, U ∈ Fam ∧ i U = n) (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n)) X HexU) (from left to right).
Use reflexivity.
We prove the intermediate claim HxInt: x ∈ intersection_of_family X Fam.
rewrite the current goal using HAEq (from right to left).
An exact proof term for the current goal is HxA.
We prove the intermediate claim HxU: x ∈ Eps_i P.
An exact proof term for the current goal is (intersection_of_familyE2 X Fam x HxInt (Eps_i P) HUinFam).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HxU.
Assume HnexU: ¬ (∃U : set, U ∈ Fam ∧ i U = n).
We prove the intermediate claim HUeq: U_of n = X.
We prove the intermediate claim HUdef: U_of n = if (∃U : set, U ∈ Fam ∧ i U = n) then (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n)) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
rewrite the current goal using (If_i_0 (∃U : set, U ∈ Fam ∧ i U = n) (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n)) X HnexU) (from left to right).
Use reflexivity.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).
An exact proof term for the current goal is (HAsubX x HxA).
Set B_of to be the term (λn : set ⇒ X ∖ (U_of n)).
We prove the intermediate claim HB_of_closed: ∀n : set, n ∈ ω → closed_in X Tx (B_of n).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HUnTx: U_of n ∈ Tx.
An exact proof term for the current goal is (HU_of_in_Tx n HnO).
An exact proof term for the current goal is (closed_of_open_complement X Tx (U_of n) HTx HUnTx).
We prove the intermediate claim HA_B_disj: ∀n : set, n ∈ ω → A ∩ (B_of n) = Empty.
Let n be given.
Assume HnO: n ∈ ω.
Apply set_ext to the current goal.
Let x be given.
Assume HxAB: x ∈ A ∩ (B_of n).
Apply FalseE to the current goal.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A (B_of n) x HxAB).
We prove the intermediate claim HxB: x ∈ B_of n.
An exact proof term for the current goal is (binintersectE2 A (B_of n) x HxAB).
We prove the intermediate claim HxUn: x ∈ U_of n.
An exact proof term for the current goal is (HA_sub_Uof n HnO x HxA).
We prove the intermediate claim HxnotUn: x ∉ U_of n.
An exact proof term for the current goal is (setminusE2 X (U_of n) x HxB).
An exact proof term for the current goal is (HxnotUn HxUn).
An exact proof term for the current goal is (Subq_Empty (A ∩ (B_of n))).
We prove the intermediate claim Hbump_exists: ∀n : set, n ∈ ω → ∃f : set, n ∈ ω ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun f x = eps_ (ordsucc n)).
Let n be given.
Assume HnO: n ∈ ω.
Set epsn to be the term eps_ (ordsucc 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 HepsR: epsn ∈ R.
An exact proof term for the current goal is (SNoS_omega_real epsn (SNo_eps_SNoS_omega (ordsucc n) HsuccO)).
We prove the intermediate claim HepsPosS: 0 < epsn.
An exact proof term for the current goal is (SNo_eps_pos (ordsucc n) HsuccO).
We prove the intermediate claim HepsPos: Rlt 0 epsn.
An exact proof term for the current goal is (RltI 0 epsn real_0 HepsR HepsPosS).
We prove the intermediate claim H0le: Rle 0 epsn.
An exact proof term for the current goal is (Rlt_implies_Rle 0 epsn HepsPos).
We prove the intermediate claim HBcl: closed_in X Tx (B_of n).
An exact proof term for the current goal is (HB_of_closed n HnO).
We prove the intermediate claim Hdisj: A ∩ (B_of n) = Empty.
An exact proof term for the current goal is (HA_B_disj n HnO).
We prove the intermediate claim HexUry: ∃uI : set, continuous_map X Tx (closed_interval 0 epsn) (closed_interval_topology 0 epsn) uI ∧ (∀x : set, x ∈ A → apply_fun uI x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun uI x = epsn).
An exact proof term for the current goal is (Urysohn_lemma X Tx A (B_of n) 0 epsn H0le Hnorm HAcl HBcl Hdisj).
Apply HexUry to the current goal.
Let uI be given.
Assume HuIpack: continuous_map X Tx (closed_interval 0 epsn) (closed_interval_topology 0 epsn) uI ∧ (∀x : set, x ∈ A → apply_fun uI x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun uI x = epsn).
We prove the intermediate claim HuIcore: continuous_map X Tx (closed_interval 0 epsn) (closed_interval_topology 0 epsn) uI ∧ (∀x : set, x ∈ A → apply_fun uI x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 epsn) (closed_interval_topology 0 epsn) uI ∧ (∀x : set, x ∈ A → apply_fun uI x = 0)) (∀x : set, x ∈ (B_of n) → apply_fun uI x = epsn) HuIpack).
We prove the intermediate claim HuIcontI: continuous_map X Tx (closed_interval 0 epsn) (closed_interval_topology 0 epsn) uI.
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 epsn) (closed_interval_topology 0 epsn) uI) (∀x : set, x ∈ A → apply_fun uI x = 0) HuIcore).
We prove the intermediate claim HuIA0: ∀x : set, x ∈ A → apply_fun uI x = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 epsn) (closed_interval_topology 0 epsn) uI) (∀x : set, x ∈ A → apply_fun uI x = 0) HuIcore).
We prove the intermediate claim HuIB: ∀x : set, x ∈ (B_of n) → apply_fun uI x = epsn.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 epsn) (closed_interval_topology 0 epsn) uI ∧ (∀x : set, x ∈ A → apply_fun uI x = 0)) (∀x : set, x ∈ (B_of n) → apply_fun uI x = epsn) HuIpack).
We prove the intermediate claim HI_sub_R: closed_interval 0 epsn ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R 0 epsn).
We prove the intermediate claim HTiEq: closed_interval_topology 0 epsn = subspace_topology R R_standard_topology (closed_interval 0 epsn).
Use reflexivity.
We prove the intermediate claim HuIcontR: continuous_map X Tx R R_standard_topology uI.
An exact proof term for the current goal is (continuous_map_range_expand X Tx (closed_interval 0 epsn) (closed_interval_topology 0 epsn) R R_standard_topology uI HuIcontI HI_sub_R R_standard_topology_is_topology_local HTiEq).
We prove the intermediate claim HepsDef: epsn = eps_ (ordsucc n).
Use reflexivity.
We use uI to witness the existential quantifier.
We will prove n ∈ ω ∧ continuous_map X Tx R R_standard_topology uI ∧ (∀x : set, x ∈ A → apply_fun uI x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun uI x = eps_ (ordsucc n)).
Apply andI to the current goal.
We will prove (n ∈ ω ∧ continuous_map X Tx R R_standard_topology uI) ∧ (∀x : set, x ∈ A → apply_fun uI x = 0).
Apply andI to the current goal.
We will prove n ∈ ω ∧ continuous_map X Tx R R_standard_topology uI.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
An exact proof term for the current goal is HuIcontR.
An exact proof term for the current goal is HuIA0.
Let x be given.
Assume HxB: x ∈ (B_of n).
rewrite the current goal using HepsDef (from right to left).
An exact proof term for the current goal is (HuIB x HxB).
Set bump_pred to be the term (λn f : set ⇒ continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun f x = eps_ (ordsucc n))).
We prove the intermediate claim Hbump_exists2: ∀n : set, n ∈ ω → ∃f : set, bump_pred n f.
Let n be given.
Assume HnO: n ∈ ω.
Apply (Hbump_exists n HnO) to the current goal.
Let f be given.
Assume Hfpack: n ∈ ω ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun f x = eps_ (ordsucc n)).
We prove the intermediate claim Hleft: (n ∈ ω ∧ continuous_map X Tx R R_standard_topology f) ∧ (∀x : set, x ∈ A → apply_fun f x = 0).
An exact proof term for the current goal is (andEL ((n ∈ ω ∧ continuous_map X Tx R R_standard_topology f) ∧ (∀x : set, x ∈ A → apply_fun f x = 0)) (∀x : set, x ∈ (B_of n) → apply_fun f x = eps_ (ordsucc n)) Hfpack).
We prove the intermediate claim HfB: ∀x : set, x ∈ (B_of n) → apply_fun f x = eps_ (ordsucc n).
An exact proof term for the current goal is (andER ((n ∈ ω ∧ continuous_map X Tx R R_standard_topology f) ∧ (∀x : set, x ∈ A → apply_fun f x = 0)) (∀x : set, x ∈ (B_of n) → apply_fun f x = eps_ (ordsucc n)) Hfpack).
We prove the intermediate claim HfAcore: n ∈ ω ∧ continuous_map X Tx R R_standard_topology f.
An exact proof term for the current goal is (andEL (n ∈ ω ∧ continuous_map X Tx R R_standard_topology f) (∀x : set, x ∈ A → apply_fun f x = 0) Hleft).
We prove the intermediate claim HfA: ∀x : set, x ∈ A → apply_fun f x = 0.
An exact proof term for the current goal is (andER (n ∈ ω ∧ continuous_map X Tx R R_standard_topology f) (∀x : set, x ∈ A → apply_fun f x = 0) Hleft).
We prove the intermediate claim Hfcont: continuous_map X Tx R R_standard_topology f.
An exact proof term for the current goal is (andER (n ∈ ω) (continuous_map X Tx R R_standard_topology f) HfAcore).
We use f to witness the existential quantifier.
We will prove bump_pred n f.
We prove the intermediate claim Hbdef: bump_pred n f = (continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun f x = eps_ (ordsucc n))).
Use reflexivity.
rewrite the current goal using Hbdef (from left to right).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hfcont.
An exact proof term for the current goal is HfA.
An exact proof term for the current goal is HfB.
Set u_of to be the term (λn : set ⇒ Eps_i (λf : set ⇒ bump_pred n f)).
We prove the intermediate claim Hu_of_prop: ∀n : set, n ∈ ω → bump_pred n (u_of n).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim Hex: ∃f : set, bump_pred n f.
An exact proof term for the current goal is (Hbump_exists2 n HnO).
Apply Hex to the current goal.
Let f be given.
Assume Hfp: bump_pred n f.
An exact proof term for the current goal is (Eps_i_ax (λf0 : set ⇒ bump_pred n f0) f Hfp).
We prove the intermediate claim Hu_of_cont: ∀n : set, n ∈ ω → continuous_map X Tx R R_standard_topology (u_of n).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim Hup: bump_pred n (u_of n).
An exact proof term for the current goal is (Hu_of_prop n HnO).
We prove the intermediate claim Hupdef: bump_pred n (u_of n) = (continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x : set, x ∈ A → apply_fun (u_of n) x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun (u_of n) x = eps_ (ordsucc n))).
Use reflexivity.
We prove the intermediate claim Hexp: (continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x : set, x ∈ A → apply_fun (u_of n) x = 0)) ∧ (∀x : set, x ∈ (B_of n) → apply_fun (u_of n) x = eps_ (ordsucc n)).
rewrite the current goal using Hupdef (from right to left).
An exact proof term for the current goal is Hup.
We prove the intermediate claim Hleft: continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x : set, x ∈ A → apply_fun (u_of n) x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x : set, x ∈ A → apply_fun (u_of n) x = 0)) (∀x : set, x ∈ (B_of n) → apply_fun (u_of n) x = eps_ (ordsucc n)) Hexp).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology (u_of n)) (∀x : set, x ∈ A → apply_fun (u_of n) x = 0) Hleft).
We prove the intermediate claim Hu_of_A0: ∀n x : set, n ∈ ω → x ∈ A → apply_fun (u_of n) x = 0.
Let n and x be given.
Assume HnO: n ∈ ω.
Assume HxA: x ∈ A.
We prove the intermediate claim Hup: bump_pred n (u_of n).
An exact proof term for the current goal is (Hu_of_prop n HnO).
We prove the intermediate claim Hupdef: bump_pred n (u_of n) = (continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B_of n) → apply_fun (u_of n) x0 = eps_ (ordsucc n))).
Use reflexivity.
We prove the intermediate claim Hexp: (continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0)) ∧ (∀x0 : set, x0 ∈ (B_of n) → apply_fun (u_of n) x0 = eps_ (ordsucc n)).
rewrite the current goal using Hupdef (from right to left).
An exact proof term for the current goal is Hup.
We prove the intermediate claim Hleft: continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0)) (∀x0 : set, x0 ∈ (B_of n) → apply_fun (u_of n) x0 = eps_ (ordsucc n)) Hexp).
We prove the intermediate claim Hforall: ∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (u_of n)) (∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0) Hleft).
An exact proof term for the current goal is (Hforall x HxA).
We prove the intermediate claim Hu_of_Beps: ∀n x : set, n ∈ ω → x ∈ (B_of n) → apply_fun (u_of n) x = eps_ (ordsucc n).
Let n and x be given.
Assume HnO: n ∈ ω.
Assume HxB: x ∈ (B_of n).
We prove the intermediate claim Hup: bump_pred n (u_of n).
An exact proof term for the current goal is (Hu_of_prop n HnO).
We prove the intermediate claim Hupdef: bump_pred n (u_of n) = (continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B_of n) → apply_fun (u_of n) x0 = eps_ (ordsucc n))).
Use reflexivity.
We prove the intermediate claim Hexp: (continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0)) ∧ (∀x0 : set, x0 ∈ (B_of n) → apply_fun (u_of n) x0 = eps_ (ordsucc n)).
rewrite the current goal using Hupdef (from right to left).
An exact proof term for the current goal is Hup.
We prove the intermediate claim Hforall: ∀x0 : set, x0 ∈ (B_of n) → apply_fun (u_of n) x0 = eps_ (ordsucc n).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (u_of n) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0)) (∀x0 : set, x0 ∈ (B_of n) → apply_fun (u_of n) x0 = eps_ (ordsucc n)) Hexp).
An exact proof term for the current goal is (Hforall x HxB).
Set vI_of to be the term (λn : set ⇒ compose_fun X (u_of n) normalize01_fun).
We prove the intermediate claim HvI_cont: ∀n : set, n ∈ ω → continuous_map X Tx unit_interval unit_interval_topology (vI_of n).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim Hucont: continuous_map X Tx R R_standard_topology (u_of n).
An exact proof term for the current goal is (Hu_of_cont n HnO).
An exact proof term for the current goal is (composition_continuous X Tx R R_standard_topology unit_interval unit_interval_topology (u_of n) normalize01_fun Hucont normalize01_fun_continuous_to_unit_interval).
We prove the intermediate claim HvR_cont: ∀n : set, n ∈ ω → continuous_map X Tx R R_standard_topology (vI_of n).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HvI: continuous_map X Tx unit_interval unit_interval_topology (vI_of n).
An exact proof term for the current goal is (HvI_cont n HnO).
We prove the intermediate claim HUiEq: unit_interval_topology = subspace_topology R R_standard_topology unit_interval.
Use reflexivity.
An exact proof term for the current goal is (continuous_map_range_expand X Tx unit_interval unit_interval_topology R R_standard_topology (vI_of n) HvI unit_interval_sub_R R_standard_topology_is_topology_local HUiEq).
Set term_of to be the term (λn : set ⇒ compose_fun X (vI_of n) (mul_const_fun (eps_ (ordsucc n)))).
We prove the intermediate claim Hterm_cont: ∀n : set, n ∈ ω → continuous_map X Tx R R_standard_topology (term_of n).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HvR: continuous_map X Tx R R_standard_topology (vI_of n).
An exact proof term for the current goal is (HvR_cont n HnO).
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 HepsR: eps_ (ordsucc n) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc n)) (SNo_eps_SNoS_omega (ordsucc n) HsuccO)).
An exact proof term for the current goal is (scale_continuous_mul_const_pos X Tx (vI_of n) (eps_ (ordsucc n)) HTx HvR HepsR (SNo_eps_pos (ordsucc n) HsuccO)).
We prove the intermediate claim Hterm_A0: ∀n x : set, n ∈ ω → x ∈ A → apply_fun (term_of n) x = 0.
Let n and x be given.
Assume HnO: n ∈ ω.
Assume HxA: x ∈ A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HAcl x HxA).
We prove the intermediate claim Hu0: apply_fun (u_of n) x = 0.
An exact proof term for the current goal is (Hu_of_A0 n x HnO HxA).
We prove the intermediate claim HvIapp: apply_fun (vI_of n) x = apply_fun normalize01_fun (apply_fun (u_of n) x).
An exact proof term for the current goal is (compose_fun_apply X (u_of n) normalize01_fun x HxX).
We prove the intermediate claim Htermapp: apply_fun (term_of n) x = apply_fun (mul_const_fun (eps_ (ordsucc n))) (apply_fun (vI_of n) x).
An exact proof term for the current goal is (compose_fun_apply X (vI_of n) (mul_const_fun (eps_ (ordsucc n))) x HxX).
rewrite the current goal using Htermapp (from left to right).
rewrite the current goal using HvIapp (from left to right).
rewrite the current goal using Hu0 (from left to right).
rewrite the current goal using normalize01_fun_0 (from left to right).
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 HepsR: eps_ (ordsucc n) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc n)) (SNo_eps_SNoS_omega (ordsucc n) HsuccO)).
rewrite the current goal using (mul_const_fun_apply (eps_ (ordsucc n)) 0 HepsR real_0) (from left to right).
An exact proof term for the current goal is (mul_SNo_zeroL (eps_ (ordsucc n)) (real_SNo (eps_ (ordsucc n)) HepsR)).
We prove the intermediate claim Hterm_Bpos: ∀n x : set, n ∈ ω → x ∈ (B_of n) → Rlt 0 (apply_fun (term_of n) x).
Let n and x be given.
Assume HnO: n ∈ ω.
Assume HxB: x ∈ (B_of n).
We prove the intermediate claim HBdef: B_of n = X ∖ U_of n.
Use reflexivity.
We prove the intermediate claim HxBexp: x ∈ X ∖ U_of n.
rewrite the current goal using HBdef (from right to left).
An exact proof term for the current goal is HxB.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (U_of n) x HxBexp).
We prove the intermediate claim HuEq: apply_fun (u_of n) x = eps_ (ordsucc n).
An exact proof term for the current goal is (Hu_of_Beps n x HnO HxB).
We prove the intermediate claim HvIapp: apply_fun (vI_of n) x = apply_fun normalize01_fun (apply_fun (u_of n) x).
An exact proof term for the current goal is (compose_fun_apply X (u_of n) normalize01_fun x HxX).
We prove the intermediate claim Htermapp: apply_fun (term_of n) x = apply_fun (mul_const_fun (eps_ (ordsucc n))) (apply_fun (vI_of n) x).
An exact proof term for the current goal is (compose_fun_apply X (vI_of n) (mul_const_fun (eps_ (ordsucc n))) x HxX).
rewrite the current goal using Htermapp (from left to right).
rewrite the current goal using HvIapp (from left to right).
rewrite the current goal using HuEq (from left to right).
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 HepsR: eps_ (ordsucc n) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc n)) (SNo_eps_SNoS_omega (ordsucc n) HsuccO)).
We prove the intermediate claim HepsS: SNo (eps_ (ordsucc n)).
An exact proof term for the current goal is (real_SNo (eps_ (ordsucc n)) HepsR).
We prove the intermediate claim Hepspos: 0 < eps_ (ordsucc n).
An exact proof term for the current goal is (SNo_eps_pos (ordsucc n) HsuccO).
We prove the intermediate claim Hne0: eps_ (ordsucc n) ≠ 0.
An exact proof term for the current goal is (SNo_pos_ne0 (eps_ (ordsucc n)) HepsS Hepspos).
We prove the intermediate claim Hnormpos: Rlt 0 (apply_fun normalize01_fun (eps_ (ordsucc n))).
An exact proof term for the current goal is (normalize01_fun_pos_of_neq0 (eps_ (ordsucc n)) HepsR Hne0).
We prove the intermediate claim HnormR: apply_fun normalize01_fun (eps_ (ordsucc n)) ∈ R.
An exact proof term for the current goal is (normalize01_fun_value_in_R (eps_ (ordsucc n)) HepsR).
We prove the intermediate claim HnormS: SNo (apply_fun normalize01_fun (eps_ (ordsucc n))).
An exact proof term for the current goal is (real_SNo (apply_fun normalize01_fun (eps_ (ordsucc n))) HnormR).
rewrite the current goal using (mul_const_fun_apply (eps_ (ordsucc n)) (apply_fun normalize01_fun (eps_ (ordsucc n))) HepsR HnormR) (from left to right).
We prove the intermediate claim HmulposS: 0 < mul_SNo (apply_fun normalize01_fun (eps_ (ordsucc n))) (eps_ (ordsucc n)).
An exact proof term for the current goal is (mul_SNo_pos_pos (apply_fun normalize01_fun (eps_ (ordsucc n))) (eps_ (ordsucc n)) HnormS HepsS (RltE_lt 0 (apply_fun normalize01_fun (eps_ (ordsucc n))) Hnormpos) Hepspos).
We prove the intermediate claim HmulR: mul_SNo (apply_fun normalize01_fun (eps_ (ordsucc n))) (eps_ (ordsucc n)) ∈ R.
An exact proof term for the current goal is (real_mul_SNo (apply_fun normalize01_fun (eps_ (ordsucc n))) HnormR (eps_ (ordsucc n)) HepsR).
An exact proof term for the current goal is (RltI 0 (mul_SNo (apply_fun normalize01_fun (eps_ (ordsucc n))) (eps_ (ordsucc n))) real_0 HmulR HmulposS).
Set sum_step to be the term (λx : set ⇒ λk acc : set ⇒ add_SNo acc (apply_fun (term_of k) x)).
Set partial_sum to be the term (λx n : set ⇒ nat_primrec 0 (sum_step x) n).
Set s_fun to be the term (λn : set ⇒ graph X (λx : set ⇒ partial_sum x n)).
Set fn to be the term graph ω (λn : set ⇒ s_fun n).
We prove the intermediate claim Hfn: function_on fn ω (function_space X R).
Let n be given.
Assume HnO: n ∈ ω.
We will prove apply_fun fn n ∈ function_space X R.
We prove the intermediate claim Hfndef: fn = graph ω (λn0 : set ⇒ s_fun n0).
Use reflexivity.
rewrite the current goal using Hfndef (from left to right).
We prove the intermediate claim Happ: apply_fun (graph ω (λn0 : set ⇒ s_fun n0)) n = s_fun n.
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ s_fun n0) n HnO).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hsdef: s_fun n = graph X (λx : set ⇒ partial_sum x n).
Use reflexivity.
rewrite the current goal using Hsdef (from left to right).
Apply (graph_in_function_space X R (λx : set ⇒ partial_sum x n)) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We will prove partial_sum x n ∈ R.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
Set p to be the term (λm : set ⇒ partial_sum x m ∈ R).
We prove the intermediate claim Hp0: p 0.
We will prove partial_sum x 0 ∈ R.
We prove the intermediate claim Hdef0: partial_sum x 0 = nat_primrec 0 (sum_step x) 0.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (nat_primrec_0 0 (sum_step x)) (from left to right).
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hps: ∀m : set, nat_p m → p m → p (ordsucc m).
Let m be given.
Assume HmNat: nat_p m.
Assume HmIH: p m.
We will prove partial_sum x (ordsucc m) ∈ R.
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (nat_p_omega m HmNat).
We prove the intermediate claim HdefS: partial_sum x (ordsucc m) = nat_primrec 0 (sum_step x) (ordsucc m).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc m) = sum_step x m (nat_primrec 0 (sum_step x) m).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) m HmNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) m = partial_sum x m.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim HaccR: partial_sum x m ∈ R.
An exact proof term for the current goal is HmIH.
We prove the intermediate claim HtermC: continuous_map X Tx R R_standard_topology (term_of m).
An exact proof term for the current goal is (Hterm_cont m HmO).
We prove the intermediate claim HtermFun: function_on (term_of m) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (term_of m) HtermC).
We prove the intermediate claim HtermR: apply_fun (term_of m) x ∈ R.
An exact proof term for the current goal is (HtermFun x HxX).
We prove the intermediate claim Hstepdef: sum_step x m (partial_sum x m) = add_SNo (partial_sum x m) (apply_fun (term_of m) x).
Use reflexivity.
rewrite the current goal using Hstepdef (from left to right).
An exact proof term for the current goal is (real_add_SNo (partial_sum x m) HaccR (apply_fun (term_of m) x) HtermR).
An exact proof term for the current goal is (nat_ind p Hp0 Hps n HnNat).
We prove the intermediate claim Hfn_cont: ∀n : set, n ∈ ω → continuous_map X Tx R R_standard_topology (apply_fun fn n).
Let n be given.
Assume HnO: n ∈ ω.
We will prove continuous_map X Tx R R_standard_topology (apply_fun fn n).
We prove the intermediate claim Hfndef: fn = graph ω (λn0 : set ⇒ s_fun n0).
Use reflexivity.
We prove the intermediate claim Happ: apply_fun fn n = s_fun n.
rewrite the current goal using Hfndef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ s_fun n0) n HnO).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
Set p to be the term (λm : set ⇒ continuous_map X Tx R R_standard_topology (s_fun m)).
We prove the intermediate claim Hp0: p 0.
We will prove continuous_map X Tx R R_standard_topology (s_fun 0).
We prove the intermediate claim Hs0def: s_fun 0 = graph X (λx : set ⇒ partial_sum x 0).
Use reflexivity.
We prove the intermediate claim Hs0fun: function_on (s_fun 0) X R.
rewrite the current goal using Hs0def (from left to right).
We prove the intermediate claim Htot: total_function_on (graph X (λx : set ⇒ partial_sum x 0)) X R.
Apply (total_function_on_graph X R (λx : set ⇒ partial_sum x 0)) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We will prove partial_sum x 0 ∈ R.
We prove the intermediate claim Hdef0: partial_sum x 0 = nat_primrec 0 (sum_step x) 0.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (nat_primrec_0 0 (sum_step x)) (from left to right).
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is (andEL (function_on (graph X (λx : set ⇒ partial_sum x 0)) X R) (∀x : set, x ∈ X → ∃y : set, y ∈ R ∧ (x,y) ∈ graph X (λx : set ⇒ partial_sum x 0)) Htot).
We prove the intermediate claim Hc0cont: continuous_map X Tx R R_standard_topology (const_fun X 0).
An exact proof term for the current goal is (const_fun_continuous X Tx R R_standard_topology 0 HTx R_standard_topology_is_topology_local real_0).
We prove the intermediate claim Heq0: ∀x : set, x ∈ X → apply_fun (const_fun X 0) x = apply_fun (s_fun 0) x.
Let x be given.
Assume HxX: x ∈ X.
rewrite the current goal using (const_fun_apply X 0 x HxX) (from left to right).
We prove the intermediate claim Hs0app: apply_fun (s_fun 0) x = partial_sum x 0.
rewrite the current goal using Hs0def (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx : set ⇒ partial_sum x 0) x HxX).
rewrite the current goal using Hs0app (from left to right).
We prove the intermediate claim Hdef0: partial_sum x 0 = nat_primrec 0 (sum_step x) 0.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (nat_primrec_0 0 (sum_step x)) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (continuous_map_congr_on X Tx R R_standard_topology (const_fun X 0) (s_fun 0) Hc0cont Hs0fun Heq0).
We prove the intermediate claim Hps: ∀m : set, nat_p m → p m → p (ordsucc m).
Let m be given.
Assume HmNat: nat_p m.
Assume HmIH: p m.
We will prove continuous_map X Tx R R_standard_topology (s_fun (ordsucc m)).
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (nat_p_omega m HmNat).
Set t to be the term compose_fun X (pair_map X (s_fun m) (term_of m)) add_fun_R.
We prove the intermediate claim Htcont: continuous_map X Tx R R_standard_topology t.
An exact proof term for the current goal is (add_two_continuous_R X Tx (s_fun m) (term_of m) HTx HmIH (Hterm_cont m HmO)).
We prove the intermediate claim Htfun: function_on t X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology t Htcont).
We prove the intermediate claim HsSdef: s_fun (ordsucc m) = graph X (λx : set ⇒ partial_sum x (ordsucc m)).
Use reflexivity.
We prove the intermediate claim HsSfun: function_on (s_fun (ordsucc m)) X R.
rewrite the current goal using HsSdef (from left to right).
We prove the intermediate claim Htot: total_function_on (graph X (λx : set ⇒ partial_sum x (ordsucc m))) X R.
Apply (total_function_on_graph X R (λx : set ⇒ partial_sum x (ordsucc m))) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We will prove partial_sum x (ordsucc m) ∈ R.
We prove the intermediate claim HdefS: partial_sum x (ordsucc m) = nat_primrec 0 (sum_step x) (ordsucc m).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc m) = sum_step x m (nat_primrec 0 (sum_step x) m).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) m HmNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) m = partial_sum x m.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim Hsdef: s_fun m = graph X (λx : set ⇒ partial_sum x m).
Use reflexivity.
We prove the intermediate claim Hsfun: function_on (s_fun m) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (s_fun m) HmIH).
We prove the intermediate claim HaccR: partial_sum x m ∈ R.
We prove the intermediate claim Hsapp: apply_fun (s_fun m) x = partial_sum x m.
rewrite the current goal using Hsdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx : set ⇒ partial_sum x m) x HxX).
rewrite the current goal using Hsapp (from right to left).
An exact proof term for the current goal is (Hsfun x HxX).
We prove the intermediate claim HtermC: continuous_map X Tx R R_standard_topology (term_of m).
An exact proof term for the current goal is (Hterm_cont m HmO).
We prove the intermediate claim HtermFun: function_on (term_of m) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (term_of m) HtermC).
We prove the intermediate claim HtermR: apply_fun (term_of m) x ∈ R.
An exact proof term for the current goal is (HtermFun x HxX).
We prove the intermediate claim Hstepdef: sum_step x m (partial_sum x m) = add_SNo (partial_sum x m) (apply_fun (term_of m) x).
Use reflexivity.
rewrite the current goal using Hstepdef (from left to right).
An exact proof term for the current goal is (real_add_SNo (partial_sum x m) HaccR (apply_fun (term_of m) x) HtermR).
An exact proof term for the current goal is (andEL (function_on (graph X (λx : set ⇒ partial_sum x (ordsucc m))) X R) (∀x : set, x ∈ X → ∃y : set, y ∈ R ∧ (x,y) ∈ graph X (λx : set ⇒ partial_sum x (ordsucc m))) Htot).
We prove the intermediate claim HeqS: ∀x : set, x ∈ X → apply_fun t x = apply_fun (s_fun (ordsucc m)) x.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hsdef: s_fun m = graph X (λx : set ⇒ partial_sum x m).
Use reflexivity.
We prove the intermediate claim Hsfun: function_on (s_fun m) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (s_fun m) HmIH).
We prove the intermediate claim Hsapp: apply_fun (s_fun m) x = partial_sum x m.
rewrite the current goal using Hsdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx : set ⇒ partial_sum x m) x HxX).
We prove the intermediate claim HtermC: continuous_map X Tx R R_standard_topology (term_of m).
An exact proof term for the current goal is (Hterm_cont m HmO).
We prove the intermediate claim HtermFun: function_on (term_of m) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (term_of m) HtermC).
We prove the intermediate claim HsR: apply_fun (s_fun m) x ∈ R.
An exact proof term for the current goal is (Hsfun x HxX).
We prove the intermediate claim HtermR: apply_fun (term_of m) x ∈ R.
An exact proof term for the current goal is (HtermFun x HxX).
We prove the intermediate claim Htdef: t = compose_fun X (pair_map X (s_fun m) (term_of m)) add_fun_R.
Use reflexivity.
We prove the intermediate claim Hlhs: apply_fun t x = add_SNo (apply_fun (s_fun m) x) (apply_fun (term_of m) x).
rewrite the current goal using Htdef (from left to right).
An exact proof term for the current goal is (add_of_pair_map_apply X (s_fun m) (term_of m) x HxX HsR HtermR).
We prove the intermediate claim Hrhs: apply_fun (s_fun (ordsucc m)) x = add_SNo (apply_fun (s_fun m) x) (apply_fun (term_of m) x).
We prove the intermediate claim HsSuccApp: apply_fun (s_fun (ordsucc m)) x = partial_sum x (ordsucc m).
rewrite the current goal using HsSdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx : set ⇒ partial_sum x (ordsucc m)) x HxX).
rewrite the current goal using HsSuccApp (from left to right).
We prove the intermediate claim HdefS: partial_sum x (ordsucc m) = nat_primrec 0 (sum_step x) (ordsucc m).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc m) = sum_step x m (nat_primrec 0 (sum_step x) m).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) m HmNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) m = partial_sum x m.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim Hstepdef: sum_step x m (partial_sum x m) = add_SNo (partial_sum x m) (apply_fun (term_of m) x).
Use reflexivity.
rewrite the current goal using Hstepdef (from left to right).
rewrite the current goal using Hsapp (from left to right).
Use reflexivity.
rewrite the current goal using Hlhs (from left to right).
rewrite the current goal using Hrhs (from right to left).
Use reflexivity.
An exact proof term for the current goal is (continuous_map_congr_on X Tx R R_standard_topology t (s_fun (ordsucc m)) Htcont HsSfun HeqS).
We prove the intermediate claim Hscont: ∀m : set, nat_p m → p m.
An exact proof term for the current goal is (nat_ind p Hp0 Hps).
An exact proof term for the current goal is (Hscont n HnNat).
We prove the intermediate claim Huc: uniform_cauchy_metric X R R_bounded_metric fn.
Let eps be given.
Assume HepsR: eps ∈ R.
Assume HepsPos: Rlt 0 eps.
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < eps.
An exact proof term for the current goal is (exists_eps_lt_pos eps HepsR HepsPos).
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 < eps) HNpair).
We prove the intermediate claim HepsltS: eps_ N < eps.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < eps) 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 Hepslt: Rlt (eps_ N) eps.
An exact proof term for the current goal is (RltI (eps_ N) eps HepsNR HepsR HepsltS).
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 m and n be given.
Assume HmO: m ∈ ω.
Assume HnO: n ∈ ω.
Assume HNm: N ⊆ m.
Assume HNn: N ⊆ n.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Htail: Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m) x,apply_fun (apply_fun fn n) x)) (eps_ 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 HNnat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNomega).
We prove the intermediate claim Hordm: ordinal m.
An exact proof term for the current goal is (nat_p_ordinal m HmNat).
We prove the intermediate claim Hordn: ordinal n.
An exact proof term for the current goal is (nat_p_ordinal n HnNat).
We prove the intermediate claim HordN: ordinal N.
An exact proof term for the current goal is (nat_p_ordinal N HNnat).
We prove the intermediate claim HmR: metric_on R R_bounded_metric.
An exact proof term for the current goal is R_bounded_metric_is_metric_on_early.
We prove the intermediate claim HepsN_le: ∀t : set, t ∈ ω → nat_p t → N ⊆ t → Rle (eps_ t) (eps_ N).
Let t be given.
Assume HtO: t ∈ ω.
Assume HtNat: nat_p t.
Assume HNt: N ⊆ t.
Apply (xm (t = N)) to the current goal.
Assume Heq: t = N.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Rle_refl (eps_ N) HepsNR).
Assume Hneq: ¬ (t = N).
We prove the intermediate claim Htri: N ∈ t ∨ N = t ∨ t ∈ N.
An exact proof term for the current goal is (ordinal_trichotomy_or N t HordN (nat_p_ordinal t HtNat)).
Apply Htri to the current goal.
Assume Hleft: N ∈ t ∨ N = t.
Apply Hleft to the current goal.
Assume HNin: N ∈ t.
We prove the intermediate claim HepsltS': eps_ t < eps_ N.
An exact proof term for the current goal is (SNo_eps_decr t HtO N HNin).
We prove the intermediate claim Heps_tR: eps_ t ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ t) (SNo_eps_SNoS_omega t HtO)).
We prove the intermediate claim Hepslt': Rlt (eps_ t) (eps_ N).
An exact proof term for the current goal is (RltI (eps_ t) (eps_ N) Heps_tR HepsNR HepsltS').
An exact proof term for the current goal is (Rlt_implies_Rle (eps_ t) (eps_ N) Hepslt').
Assume HeqNt: N = t.
We prove the intermediate claim Heq: t = N.
rewrite the current goal using HeqNt (from left to right).
Use reflexivity.
An exact proof term for the current goal is (FalseE (Hneq Heq) (Rle (eps_ t) (eps_ N))).
Assume Htin: t ∈ N.
We prove the intermediate claim Htin2: t ∈ t.
An exact proof term for the current goal is (subset_elem N t t HNt Htin).
An exact proof term for the current goal is (FalseE (In_irref t Htin2) (Rle (eps_ t) (eps_ N))).
We prove the intermediate claim Hshift: ∀k : set, nat_p k → ∀t : set, t ∈ ω → nat_p t → Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn t) x,apply_fun (apply_fun fn (add_nat t k)) x)) (eps_ t).
Apply nat_ind to the current goal.
We will prove ∀t : set, t ∈ ω → nat_p t → Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn t) x,apply_fun (apply_fun fn (add_nat t 0)) x)) (eps_ t).
Let t be given.
Assume HtO: t ∈ ω.
Assume HtNat: nat_p t.
rewrite the current goal using (add_nat_0R t) (from left to right).
We prove the intermediate claim HtxR: apply_fun (apply_fun fn t) x ∈ R.
We prove the intermediate claim Hft: apply_fun fn t ∈ function_space X R.
An exact proof term for the current goal is (Hfn t HtO).
We prove the intermediate claim Hft_on: function_on (apply_fun fn t) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn t) X R Hft).
An exact proof term for the current goal is (Hft_on x HxX).
We prove the intermediate claim Hd0: apply_fun R_bounded_metric (apply_fun (apply_fun fn t) x,apply_fun (apply_fun fn t) x) = 0.
An exact proof term for the current goal is (metric_on_diag_zero R R_bounded_metric (apply_fun (apply_fun fn t) x) HmR HtxR).
rewrite the current goal using Hd0 (from left to right).
We prove the intermediate claim Heps_tR: eps_ t ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ t) (SNo_eps_SNoS_omega t HtO)).
We prove the intermediate claim H0ltS: 0 < eps_ t.
An exact proof term for the current goal is (SNo_eps_pos t HtO).
We prove the intermediate claim H0lt: Rlt 0 (eps_ t).
An exact proof term for the current goal is (RltI 0 (eps_ t) real_0 Heps_tR H0ltS).
An exact proof term for the current goal is H0lt.
Let k be given.
Assume HkNat: nat_p k.
Assume IH: ∀t : set, t ∈ ω → nat_p t → Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn t) x,apply_fun (apply_fun fn (add_nat t k)) x)) (eps_ t).
We will prove ∀t : set, t ∈ ω → nat_p t → Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn t) x,apply_fun (apply_fun fn (add_nat t (ordsucc k))) x)) (eps_ t).
Let t be given.
Assume HtO: t ∈ ω.
Assume HtNat: nat_p t.
We prove the intermediate claim HtSuccNat: nat_p (ordsucc t).
An exact proof term for the current goal is (nat_ordsucc t HtNat).
We prove the intermediate claim HtSuccO: ordsucc t ∈ ω.
An exact proof term for the current goal is (omega_ordsucc t HtO).
We prove the intermediate claim HaddR: add_nat t (ordsucc k) = ordsucc (add_nat t k).
An exact proof term for the current goal is (add_nat_SR t k HkNat).
We prove the intermediate claim HaddL: add_nat (ordsucc t) k = ordsucc (add_nat t k).
An exact proof term for the current goal is (add_nat_SL t HtNat k HkNat).
We prove the intermediate claim HaddEq: add_nat t (ordsucc k) = add_nat (ordsucc t) k.
rewrite the current goal using HaddR (from left to right).
rewrite the current goal using HaddL (from right to left).
Use reflexivity.
rewrite the current goal using HaddEq (from left to right).
Set a to be the term apply_fun (apply_fun fn t) x.
Set b to be the term apply_fun (apply_fun fn (ordsucc t)) x.
Set c to be the term apply_fun (apply_fun fn (add_nat (ordsucc t) k)) x.
We prove the intermediate claim HaR: a ∈ R.
We prove the intermediate claim Hft: apply_fun fn t ∈ function_space X R.
An exact proof term for the current goal is (Hfn t HtO).
We prove the intermediate claim Hft_on: function_on (apply_fun fn t) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn t) X R Hft).
An exact proof term for the current goal is (Hft_on x HxX).
We prove the intermediate claim HbR: b ∈ R.
We prove the intermediate claim Hft: apply_fun fn (ordsucc t) ∈ function_space X R.
An exact proof term for the current goal is (Hfn (ordsucc t) HtSuccO).
We prove the intermediate claim Hft_on: function_on (apply_fun fn (ordsucc t)) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn (ordsucc t)) X R Hft).
An exact proof term for the current goal is (Hft_on x HxX).
We prove the intermediate claim HcO: add_nat (ordsucc t) k ∈ ω.
An exact proof term for the current goal is (nat_p_omega (add_nat (ordsucc t) k) (add_nat_p (ordsucc t) HtSuccNat k HkNat)).
We prove the intermediate claim HcR: c ∈ R.
We prove the intermediate claim Hft: apply_fun fn (add_nat (ordsucc t) k) ∈ function_space X R.
An exact proof term for the current goal is (Hfn (add_nat (ordsucc t) k) HcO).
We prove the intermediate claim Hft_on: function_on (apply_fun fn (add_nat (ordsucc t) k)) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn (add_nat (ordsucc t) k)) X R Hft).
An exact proof term for the current goal is (Hft_on x HxX).
We prove the intermediate claim Htri: Rle (apply_fun R_bounded_metric (a,c)) (add_SNo (apply_fun R_bounded_metric (a,b)) (apply_fun R_bounded_metric (b,c))).
An exact proof term for the current goal is (metric_triangle_Rle R R_bounded_metric a b c HmR HaR HbR HcR).
We prove the intermediate claim HbcLt: Rlt (apply_fun R_bounded_metric (b,c)) (eps_ (ordsucc t)).
An exact proof term for the current goal is (IH (ordsucc t) HtSuccO HtSuccNat).
We prove the intermediate claim HabLe: Rle (apply_fun R_bounded_metric (a,b)) (eps_ (ordsucc t)).
Set u to be the term apply_fun (term_of t) x.
We prove the intermediate claim HutR: u ∈ R.
We prove the intermediate claim HtC: continuous_map X Tx R R_standard_topology (term_of t).
An exact proof term for the current goal is (Hterm_cont t HtO).
We prove the intermediate claim HtFun: function_on (term_of t) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (term_of t) HtC).
An exact proof term for the current goal is (HtFun x HxX).
We prove the intermediate claim HutS: SNo u.
An exact proof term for the current goal is (real_SNo u HutR).
We prove the intermediate claim Htdef: term_of t = compose_fun X (vI_of t) (mul_const_fun (eps_ (ordsucc t))).
Use reflexivity.
We prove the intermediate claim Hvt: apply_fun (vI_of t) x ∈ unit_interval.
We prove the intermediate claim HvI: continuous_map X Tx unit_interval unit_interval_topology (vI_of t).
An exact proof term for the current goal is (HvI_cont t HtO).
We prove the intermediate claim HvOn: function_on (vI_of t) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (vI_of t) HvI).
An exact proof term for the current goal is (HvOn x HxX).
We prove the intermediate claim HvR: apply_fun (vI_of t) x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (vI_of t) x) Hvt).
We prove the intermediate claim HvBounds: ¬ (Rlt (apply_fun (vI_of t) x) 0) ∧ ¬ (Rlt 1 (apply_fun (vI_of t) x)).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) (apply_fun (vI_of t) x) Hvt).
We prove the intermediate claim H0le_vR: Rle 0 (apply_fun (vI_of t) x).
An exact proof term for the current goal is (RleI 0 (apply_fun (vI_of t) x) real_0 HvR (andEL (¬ (Rlt (apply_fun (vI_of t) x) 0)) (¬ (Rlt 1 (apply_fun (vI_of t) x))) HvBounds)).
We prove the intermediate claim HvLe1R: Rle (apply_fun (vI_of t) x) 1.
An exact proof term for the current goal is (RleI (apply_fun (vI_of t) x) 1 HvR real_1 (andER (¬ (Rlt (apply_fun (vI_of t) x) 0)) (¬ (Rlt 1 (apply_fun (vI_of t) x))) HvBounds)).
We prove the intermediate claim H0le_v: 0 ≤ apply_fun (vI_of t) x.
An exact proof term for the current goal is (SNoLe_of_Rle 0 (apply_fun (vI_of t) x) H0le_vR).
We prove the intermediate claim HvLe1: apply_fun (vI_of t) x ≤ 1.
An exact proof term for the current goal is (SNoLe_of_Rle (apply_fun (vI_of t) x) 1 HvLe1R).
We prove the intermediate claim HtSuccO: ordsucc t ∈ ω.
An exact proof term for the current goal is (omega_ordsucc t HtO).
We prove the intermediate claim HepsSuccR: eps_ (ordsucc t) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc t)) (SNo_eps_SNoS_omega (ordsucc t) HtSuccO)).
We prove the intermediate claim HepsSuccS: SNo (eps_ (ordsucc t)).
An exact proof term for the current goal is (real_SNo (eps_ (ordsucc t)) HepsSuccR).
We prove the intermediate claim HepsPosS: 0 < eps_ (ordsucc t).
An exact proof term for the current goal is (SNo_eps_pos (ordsucc t) HtSuccO).
We prove the intermediate claim HepsPosR: Rlt 0 (eps_ (ordsucc t)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc t)) real_0 HepsSuccR HepsPosS).
We prove the intermediate claim H0le_epsR: Rle 0 (eps_ (ordsucc t)).
An exact proof term for the current goal is (Rlt_implies_Rle 0 (eps_ (ordsucc t)) HepsPosR).
We prove the intermediate claim H0le_eps: 0 ≤ eps_ (ordsucc t).
An exact proof term for the current goal is (SNoLe_of_Rle 0 (eps_ (ordsucc t)) H0le_epsR).
We prove the intermediate claim HmulEq: u = mul_SNo (apply_fun (vI_of t) x) (eps_ (ordsucc t)).
We prove the intermediate claim HuDef: u = apply_fun (term_of t) x.
Use reflexivity.
We prove the intermediate claim Hcomp: apply_fun (term_of t) x = apply_fun (mul_const_fun (eps_ (ordsucc t))) (apply_fun (vI_of t) x).
rewrite the current goal using Htdef (from left to right).
An exact proof term for the current goal is (compose_fun_apply X (vI_of t) (mul_const_fun (eps_ (ordsucc t))) x HxX).
rewrite the current goal using HuDef (from left to right).
rewrite the current goal using Hcomp (from left to right).
We prove the intermediate claim HmulApp: apply_fun (mul_const_fun (eps_ (ordsucc t))) (apply_fun (vI_of t) x) = mul_SNo (apply_fun (vI_of t) x) (eps_ (ordsucc t)).
An exact proof term for the current goal is (mul_const_fun_apply (eps_ (ordsucc t)) (apply_fun (vI_of t) x) HepsSuccR HvR).
rewrite the current goal using HmulApp (from left to right).
Use reflexivity.
We prove the intermediate claim H0le_u: 0 ≤ u.
rewrite the current goal using HmulEq (from left to right).
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg (apply_fun (vI_of t) x) (eps_ (ordsucc t)) (real_SNo (apply_fun (vI_of t) x) HvR) HepsSuccS H0le_v H0le_eps).
We prove the intermediate claim HmulLe: u ≤ eps_ (ordsucc t).
rewrite the current goal using HmulEq (from left to right).
An exact proof term for the current goal is (mul_SNo_Le1_nonneg_Le (apply_fun (vI_of t) x) (eps_ (ordsucc t)) (real_SNo (apply_fun (vI_of t) x) HvR) HepsSuccS HvLe1 H0le_eps).
We prove the intermediate claim HuLeR: Rle u (eps_ (ordsucc t)).
An exact proof term for the current goal is (Rle_of_SNoLe u (eps_ (ordsucc t)) HutR HepsSuccR HmulLe).
We prove the intermediate claim HaEq: a = partial_sum x t.
We prove the intermediate claim Hfnt: apply_fun fn t = s_fun t.
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ s_fun n0) t HtO).
rewrite the current goal using Hfnt (from left to right).
We prove the intermediate claim Hsdef: s_fun t = graph X (λx0 : set ⇒ partial_sum x0 t).
Use reflexivity.
rewrite the current goal using Hsdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 t) x HxX).
We prove the intermediate claim HbEq: b = add_SNo a u.
We prove the intermediate claim HfntS: apply_fun fn (ordsucc t) = s_fun (ordsucc t).
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ s_fun n0) (ordsucc t) HtSuccO).
rewrite the current goal using HfntS (from left to right).
We prove the intermediate claim HsSdef: s_fun (ordsucc t) = graph X (λx0 : set ⇒ partial_sum x0 (ordsucc t)).
Use reflexivity.
rewrite the current goal using HsSdef (from left to right).
We prove the intermediate claim HbApp: apply_fun (graph X (λx0 : set ⇒ partial_sum x0 (ordsucc t))) x = partial_sum x (ordsucc t).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 (ordsucc t)) x HxX).
rewrite the current goal using HbApp (from left to right).
We prove the intermediate claim HdefS: partial_sum x (ordsucc t) = nat_primrec 0 (sum_step x) (ordsucc t).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc t) = sum_step x t (nat_primrec 0 (sum_step x) t).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) t HtNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) t = partial_sum x t.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim Hstepdef: sum_step x t (partial_sum x t) = add_SNo (partial_sum x t) (apply_fun (term_of t) x).
Use reflexivity.
rewrite the current goal using Hstepdef (from left to right).
rewrite the current goal using HaEq (from right to left).
Use reflexivity.
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim Hm_aS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim Hm_uS: SNo (minus_SNo u).
An exact proof term for the current goal is (SNo_minus_SNo u HutS).
We prove the intermediate claim HdiffEq: add_SNo a (minus_SNo b) = minus_SNo u.
rewrite the current goal using HbEq (from left to right).
We prove the intermediate claim HmEq: minus_SNo (add_SNo a u) = add_SNo (minus_SNo a) (minus_SNo u).
An exact proof term for the current goal is (minus_add_SNo_distr a u HaS HutS).
rewrite the current goal using HmEq (from left to right).
An exact proof term for the current goal is (add_SNo_minus_SNo_prop2 a (minus_SNo u) HaS Hm_uS).
We prove the intermediate claim HabsEq: abs_SNo (add_SNo a (minus_SNo b)) = u.
rewrite the current goal using HdiffEq (from left to right).
We prove the intermediate claim Habsm: abs_SNo (minus_SNo u) = abs_SNo u.
An exact proof term for the current goal is (abs_SNo_minus u HutS).
rewrite the current goal using Habsm (from left to right).
An exact proof term for the current goal is (nonneg_abs_SNo u H0le_u).
We prove the intermediate claim HuLe: u ≤ eps_ (ordsucc t).
An exact proof term for the current goal is HmulLe.
We prove the intermediate claim H0in: 0 ∈ ordsucc t.
An exact proof term for the current goal is (nat_0_in_ordsucc t HtNat).
We prove the intermediate claim HepsLtE0: eps_ (ordsucc t) < eps_ 0.
An exact proof term for the current goal is (SNo_eps_decr (ordsucc t) HtSuccO 0 H0in).
We prove the intermediate claim HepsLt1S: eps_ (ordsucc t) < 1.
rewrite the current goal using (eps_0_1) (from right to left).
An exact proof term for the current goal is HepsLtE0.
We prove the intermediate claim HuLt1S: u < 1.
An exact proof term for the current goal is (SNoLeLt_tra u (eps_ (ordsucc t)) 1 HutS HepsSuccS SNo_1 HuLe HepsLt1S).
We prove the intermediate claim HuLt1R: Rlt u 1.
An exact proof term for the current goal is (RltI u 1 HutR real_1 HuLt1S).
We prove the intermediate claim HabsLt1: Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1.
rewrite the current goal using HabsEq (from left to right).
An exact proof term for the current goal is HuLt1R.
We prove the intermediate claim HmetricEq: apply_fun R_bounded_metric (a,b) = u.
We prove the intermediate claim Hmab: apply_fun R_bounded_metric (a,b) = R_bounded_distance a b.
An exact proof term for the current goal is (R_bounded_metric_apply_early a b HaR HbR).
rewrite the current goal using Hmab (from left to right).
We prove the intermediate claim Hbddef: R_bounded_distance a b = If_i (Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1) (abs_SNo (add_SNo a (minus_SNo b))) 1.
Use reflexivity.
rewrite the current goal using Hbddef (from left to right).
We prove the intermediate claim HifEq: If_i (Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1) (abs_SNo (add_SNo a (minus_SNo b))) 1 = abs_SNo (add_SNo a (minus_SNo b)).
An exact proof term for the current goal is (If_i_1 (Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1) (abs_SNo (add_SNo a (minus_SNo b))) 1 HabsLt1).
rewrite the current goal using HifEq (from left to right).
rewrite the current goal using HabsEq (from left to right).
Use reflexivity.
rewrite the current goal using HmetricEq (from left to right).
An exact proof term for the current goal is HuLeR.
Set d1 to be the term apply_fun R_bounded_metric (a,b).
Set d2 to be the term apply_fun R_bounded_metric (b,c).
We prove the intermediate claim Hd1S: SNo d1.
An exact proof term for the current goal is (real_SNo d1 (RleE_left d1 (eps_ (ordsucc t)) HabLe)).
We prove the intermediate claim Hd2S: SNo d2.
An exact proof term for the current goal is (real_SNo d2 (RltE_left d2 (eps_ (ordsucc t)) HbcLt)).
We prove the intermediate claim HepsSuccR: eps_ (ordsucc t) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc t)) (SNo_eps_SNoS_omega (ordsucc t) HtSuccO)).
We prove the intermediate claim HepsSuccS: SNo (eps_ (ordsucc t)).
An exact proof term for the current goal is (real_SNo (eps_ (ordsucc t)) HepsSuccR).
We prove the intermediate claim Hd1Le: d1 ≤ eps_ (ordsucc t).
An exact proof term for the current goal is (SNoLe_of_Rle d1 (eps_ (ordsucc t)) HabLe).
We prove the intermediate claim Hd2Lt: d2 < eps_ (ordsucc t).
An exact proof term for the current goal is (RltE_lt d2 (eps_ (ordsucc t)) HbcLt).
We prove the intermediate claim Hsum1: add_SNo d1 d2 < add_SNo d1 (eps_ (ordsucc t)).
An exact proof term for the current goal is (add_SNo_Lt2 d1 d2 (eps_ (ordsucc t)) Hd1S Hd2S HepsSuccS Hd2Lt).
We prove the intermediate claim Hsum2: add_SNo d1 (eps_ (ordsucc t)) ≤ add_SNo (eps_ (ordsucc t)) (eps_ (ordsucc t)).
An exact proof term for the current goal is (add_SNo_Le1 d1 (eps_ (ordsucc t)) (eps_ (ordsucc t)) Hd1S HepsSuccS HepsSuccS Hd1Le).
We prove the intermediate claim HepsHalf: add_SNo (eps_ (ordsucc t)) (eps_ (ordsucc t)) = eps_ t.
An exact proof term for the current goal is (eps_ordsucc_half_add t HtNat).
We prove the intermediate claim HsumLtS: add_SNo d1 d2 < eps_ t.
rewrite the current goal using HepsHalf (from right to left).
An exact proof term for the current goal is (SNoLtLe_tra (add_SNo d1 d2) (add_SNo d1 (eps_ (ordsucc t))) (add_SNo (eps_ (ordsucc t)) (eps_ (ordsucc t))) (SNo_add_SNo d1 d2 Hd1S Hd2S) (SNo_add_SNo d1 (eps_ (ordsucc t)) Hd1S HepsSuccS) (SNo_add_SNo (eps_ (ordsucc t)) (eps_ (ordsucc t)) HepsSuccS HepsSuccS) Hsum1 Hsum2).
We prove the intermediate claim HsumR: add_SNo d1 d2 ∈ R.
An exact proof term for the current goal is (real_add_SNo d1 (RleE_left d1 (eps_ (ordsucc t)) HabLe) d2 (RltE_left d2 (eps_ (ordsucc t)) HbcLt)).
We prove the intermediate claim Heps_tR: eps_ t ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ t) (SNo_eps_SNoS_omega t HtO)).
We prove the intermediate claim HsumLt: Rlt (add_SNo d1 d2) (eps_ t).
An exact proof term for the current goal is (RltI (add_SNo d1 d2) (eps_ t) HsumR Heps_tR HsumLtS).
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun R_bounded_metric (a,c)) (add_SNo d1 d2) (eps_ t) Htri HsumLt).
We prove the intermediate claim Hlin: m ⊆ n ∨ n ⊆ m.
An exact proof term for the current goal is (ordinal_linear m n Hordm Hordn).
Apply Hlin to the current goal.
Assume Hmn: m ⊆ n.
We prove the intermediate claim Hexk: ∃k : set, nat_p k ∧ n = add_nat k m.
An exact proof term for the current goal is (nat_Subq_add_ex m HmNat n HnNat Hmn).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpair.
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (andEL (nat_p k) (n = add_nat k m) Hkpair).
We prove the intermediate claim HnEq0: n = add_nat k m.
An exact proof term for the current goal is (andER (nat_p k) (n = add_nat k m) Hkpair).
We prove the intermediate claim Hcom: add_nat k m = add_nat m k.
An exact proof term for the current goal is (add_nat_com k HkNat m HmNat).
We prove the intermediate claim HnEq: n = add_nat m k.
rewrite the current goal using HnEq0 (from left to right).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
rewrite the current goal using HnEq (from left to right).
We prove the intermediate claim Hdist: Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m) x,apply_fun (apply_fun fn (add_nat m k)) x)) (eps_ m).
An exact proof term for the current goal is (Hshift k HkNat m HmO HmNat).
We prove the intermediate claim HepsmLe: Rle (eps_ m) (eps_ N).
An exact proof term for the current goal is (HepsN_le m HmO HmNat HNm).
An exact proof term for the current goal is (Rlt_Rle_tra (apply_fun R_bounded_metric (apply_fun (apply_fun fn m) x,apply_fun (apply_fun fn (add_nat m k)) x)) (eps_ m) (eps_ N) Hdist HepsmLe).
Assume Hnm: n ⊆ m.
We prove the intermediate claim Hsym: apply_fun R_bounded_metric (apply_fun (apply_fun fn m) x,apply_fun (apply_fun fn n) x) = apply_fun R_bounded_metric (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x).
We prove the intermediate claim HmxR: apply_fun (apply_fun fn m) x ∈ R.
We prove the intermediate claim Hfm: apply_fun fn m ∈ function_space X R.
An exact proof term for the current goal is (Hfn m HmO).
We prove the intermediate claim Hfm_on: function_on (apply_fun fn m) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn m) X R Hfm).
An exact proof term for the current goal is (Hfm_on x HxX).
We prove the intermediate claim HnxR: apply_fun (apply_fun fn n) x ∈ R.
We prove the intermediate claim Hfnn: apply_fun fn n ∈ function_space X R.
An exact proof term for the current goal is (Hfn n HnO).
We prove the intermediate claim Hfn_on: function_on (apply_fun fn n) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn n) X R Hfnn).
An exact proof term for the current goal is (Hfn_on x HxX).
An exact proof term for the current goal is (metric_on_symmetric R R_bounded_metric (apply_fun (apply_fun fn m) x) (apply_fun (apply_fun fn n) x) HmR HmxR HnxR).
rewrite the current goal using Hsym (from left to right).
We prove the intermediate claim Hexk: ∃k : set, nat_p k ∧ m = add_nat k n.
An exact proof term for the current goal is (nat_Subq_add_ex n HnNat m HmNat Hnm).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpair.
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (andEL (nat_p k) (m = add_nat k n) Hkpair).
We prove the intermediate claim HmEq0: m = add_nat k n.
An exact proof term for the current goal is (andER (nat_p k) (m = add_nat k n) Hkpair).
We prove the intermediate claim Hcom: add_nat k n = add_nat n k.
An exact proof term for the current goal is (add_nat_com k HkNat n HnNat).
We prove the intermediate claim HmEq: m = add_nat n k.
rewrite the current goal using HmEq0 (from left to right).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
rewrite the current goal using HmEq (from left to right).
We prove the intermediate claim Hdist: Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn (add_nat n k)) x)) (eps_ n).
An exact proof term for the current goal is (Hshift k HkNat n HnO HnNat).
We prove the intermediate claim HepsnLe: Rle (eps_ n) (eps_ N).
An exact proof term for the current goal is (HepsN_le n HnO HnNat HNn).
An exact proof term for the current goal is (Rlt_Rle_tra (apply_fun R_bounded_metric (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn (add_nat n k)) x)) (eps_ n) (eps_ N) Hdist HepsnLe).
An exact proof term for the current goal is (Rlt_tra (apply_fun R_bounded_metric (apply_fun (apply_fun fn m) x,apply_fun (apply_fun fn n) x)) (eps_ N) eps Htail Hepslt).
We prove the intermediate claim Hexlim: ∃g : set, function_on g X R ∧ uniform_limit_metric X R R_bounded_metric fn g ∧ continuous_map X Tx R R_standard_topology g.
An exact proof term for the current goal is (uniform_cauchy_continuous_to_R_has_continuous_limit X Tx fn HTx Hfn Hfn_cont Huc).
Apply Hexlim to the current goal.
Let g be given.
Assume Hgpack: function_on g X R ∧ uniform_limit_metric X R R_bounded_metric fn g ∧ continuous_map X Tx R R_standard_topology g.
Set f to be the term compose_fun X g normalize01_fun.
We use f to witness the existential quantifier.
We prove the intermediate claim Hgcont: continuous_map X Tx R R_standard_topology g.
An exact proof term for the current goal is (andER (function_on g X R ∧ uniform_limit_metric X R R_bounded_metric fn g) (continuous_map X Tx R R_standard_topology g) Hgpack).
We prove the intermediate claim Hfcont: continuous_map X Tx unit_interval unit_interval_topology f.
An exact proof term for the current goal is (composition_continuous X Tx R R_standard_topology unit_interval unit_interval_topology g normalize01_fun Hgcont normalize01_fun_continuous_to_unit_interval).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hfcont.
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun f x = 0.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HAcl x HxA).
We prove the intermediate claim Hleft: function_on g X R ∧ uniform_limit_metric X R R_bounded_metric fn g.
An exact proof term for the current goal is (andEL (function_on g X R ∧ uniform_limit_metric X R R_bounded_metric fn g) (continuous_map X Tx R R_standard_topology g) Hgpack).
We prove the intermediate claim Hgfun: function_on g X R.
An exact proof term for the current goal is (andEL (function_on g X R) (uniform_limit_metric X R R_bounded_metric fn g) Hleft).
We prove the intermediate claim Hgunif: uniform_limit_metric X R R_bounded_metric fn g.
An exact proof term for the current goal is (andER (function_on g X R) (uniform_limit_metric X R R_bounded_metric fn g) Hleft).
We prove the intermediate claim HfnA0: ∀n : set, n ∈ ω → apply_fun (apply_fun fn n) x = 0.
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 Hsapp: apply_fun (apply_fun fn n) x = partial_sum x n.
We prove the intermediate claim Hfndef: fn = graph ω (λn0 : set ⇒ s_fun n0).
Use reflexivity.
rewrite the current goal using Hfndef (from left to right).
We prove the intermediate claim Happ: apply_fun (graph ω (λn0 : set ⇒ s_fun n0)) n = s_fun n.
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ s_fun n0) n HnO).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hsdef: s_fun n = graph X (λx0 : set ⇒ partial_sum x0 n).
Use reflexivity.
rewrite the current goal using Hsdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 n) x HxX).
rewrite the current goal using Hsapp (from left to right).
Set p to be the term (λm : set ⇒ partial_sum x m = 0).
We prove the intermediate claim Hp0: p 0.
We will prove partial_sum x 0 = 0.
We prove the intermediate claim Hdef0: partial_sum x 0 = nat_primrec 0 (sum_step x) 0.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (nat_primrec_0 0 (sum_step x)) (from left to right).
Use reflexivity.
We prove the intermediate claim Hps: ∀m : set, nat_p m → p m → p (ordsucc m).
Let m be given.
Assume HmNat: nat_p m.
Assume HmIH: p m.
We will prove partial_sum x (ordsucc m) = 0.
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (nat_p_omega m HmNat).
We prove the intermediate claim HdefS: partial_sum x (ordsucc m) = nat_primrec 0 (sum_step x) (ordsucc m).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc m) = sum_step x m (nat_primrec 0 (sum_step x) m).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) m HmNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) m = partial_sum x m.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim Hstepdef: sum_step x m (partial_sum x m) = add_SNo (partial_sum x m) (apply_fun (term_of m) x).
Use reflexivity.
rewrite the current goal using Hstepdef (from left to right).
We prove the intermediate claim HmEq0: partial_sum x m = 0.
An exact proof term for the current goal is HmIH.
rewrite the current goal using HmEq0 (from left to right).
We prove the intermediate claim Hterm0: apply_fun (term_of m) x = 0.
An exact proof term for the current goal is (Hterm_A0 m x HmO HxA).
rewrite the current goal using Hterm0 (from left to right).
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (nat_ind p Hp0 Hps n HnNat).
We prove the intermediate claim Hseqgx: sequence_converges_metric R R_bounded_metric (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x)) (apply_fun g x).
An exact proof term for the current goal is (uniform_limit_metric_imp_sequence_converges_metric_at_point X R R_bounded_metric fn g x R_bounded_metric_is_metric_on_early Hfn Hgfun HxX Hgunif).
We prove the intermediate claim Hseq0: sequence_converges_metric R R_bounded_metric (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x)) 0.
We will prove (((metric_on R R_bounded_metric ∧ sequence_on (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x)) R) ∧ 0 ∈ R) ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun (graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x)) n,0)) 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 R_bounded_metric_is_metric_on_early.
An exact proof term for the current goal is (sequence_converges_metric_sequence_on R R_bounded_metric (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x)) (apply_fun g x) Hseqgx).
An exact proof term for the current goal is real_0.
Let eps be given.
Assume Heps.
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 use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Let n be given.
Assume HnO: n ∈ ω.
Assume H0n: 0 ⊆ n.
We will prove Rlt (apply_fun R_bounded_metric (apply_fun (graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x)) n,0)) eps.
We prove the intermediate claim Hseqeq: apply_fun (graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x)) n = apply_fun (apply_fun fn n) x.
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x) n HnO).
We prove the intermediate claim Hpair1: (apply_fun (graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x)) n,0) = (apply_fun (apply_fun fn n) x,0).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
An exact proof term for the current goal is (tuple_2_ext (apply_fun (graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x)) n) 0 (apply_fun (apply_fun fn n) x) 0 Hseqeq H00).
rewrite the current goal using Hpair1 (from left to right).
We prove the intermediate claim Hpair2: (apply_fun (apply_fun fn n) x,0) = (0,0).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
An exact proof term for the current goal is (tuple_2_ext (apply_fun (apply_fun fn n) x) 0 0 0 (HfnA0 n HnO) H00).
rewrite the current goal using Hpair2 (from left to right).
We prove the intermediate claim Hd00: apply_fun R_bounded_metric (0,0) = 0.
An exact proof term for the current goal is (metric_on_diag_zero R R_bounded_metric 0 R_bounded_metric_is_metric_on_early real_0).
rewrite the current goal using Hd00 (from left to right).
An exact proof term for the current goal is HepsPos.
We prove the intermediate claim Hgx0: apply_fun g x = 0.
An exact proof term for the current goal is (metric_limits_unique R R_bounded_metric (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x)) (apply_fun g x) 0 R_bounded_metric_is_metric_on_early (sequence_converges_metric_sequence_on R R_bounded_metric (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x)) (apply_fun g x) Hseqgx) Hseqgx Hseq0).
We prove the intermediate claim Hfx: apply_fun f x = apply_fun normalize01_fun (apply_fun g x).
An exact proof term for the current goal is (compose_fun_apply X g normalize01_fun x HxX).
rewrite the current goal using Hfx (from left to right).
rewrite the current goal using Hgx0 (from left to right).
An exact proof term for the current goal is normalize01_fun_0.
Let x be given.
Assume HxX: x ∈ X.
Assume HxnotA: x ∉ A.
We will prove Rlt 0 (apply_fun f x).
We prove the intermediate claim Hfx: apply_fun f x = apply_fun normalize01_fun (apply_fun g x).
An exact proof term for the current goal is (compose_fun_apply X g normalize01_fun x HxX).
rewrite the current goal using Hfx (from left to right).
We prove the intermediate claim Hleft: function_on g X R ∧ uniform_limit_metric X R R_bounded_metric fn g.
An exact proof term for the current goal is (andEL (function_on g X R ∧ uniform_limit_metric X R R_bounded_metric fn g) (continuous_map X Tx R R_standard_topology g) Hgpack).
We prove the intermediate claim Hgfun: function_on g X R.
An exact proof term for the current goal is (andEL (function_on g X R) (uniform_limit_metric X R R_bounded_metric fn g) Hleft).
We prove the intermediate claim Hgunif: uniform_limit_metric X R R_bounded_metric fn g.
An exact proof term for the current goal is (andER (function_on g X R) (uniform_limit_metric X R R_bounded_metric fn g) Hleft).
We prove the intermediate claim HgxR: apply_fun g x ∈ R.
An exact proof term for the current goal is (Hgfun x HxX).
We prove the intermediate claim Hgxne0: apply_fun g x ≠ 0.
Assume Hgx0: apply_fun g x = 0.
Apply FalseE to the current goal.
We prove the intermediate claim HxnotInt: x ∉ intersection_of_family X Fam.
rewrite the current goal using HAEq (from right to left).
An exact proof term for the current goal is HxnotA.
We prove the intermediate claim HnotAllU: ¬ (∀U : set, U ∈ Fam → x ∈ U).
Assume HallU: ∀U : set, U ∈ Fam → x ∈ U.
Apply HxnotInt to the current goal.
An exact proof term for the current goal is (intersection_of_familyI X Fam x HxX HallU).
Set P to be the term (λU : set ⇒ (U ∈ Fam → x ∈ U)).
We prove the intermediate claim HexU: ∃U : set, ¬ (P U).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λU : set ⇒ P U) HnotAllU).
Apply HexU to the current goal.
Let U be given.
Assume HnotImp: ¬ (U ∈ Fam → x ∈ U).
We prove the intermediate claim Hcore: U ∈ Fam ∧ x ∉ U.
An exact proof term for the current goal is (not_imp (U ∈ Fam) (x ∈ U) HnotImp).
We prove the intermediate claim HUinFam: U ∈ Fam.
An exact proof term for the current goal is (andEL (U ∈ Fam) (x ∉ U) Hcore).
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (andER (U ∈ Fam) (x ∉ U) Hcore).
Set n0 to be the term i U.
We prove the intermediate claim Hn0O: n0 ∈ ω.
An exact proof term for the current goal is (Hi_to_omega U HUinFam).
Set delta to be the term apply_fun (term_of n0) x.
We prove the intermediate claim HxB: x ∈ (B_of n0).
Set Pn to be the term (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n0).
We prove the intermediate claim HexPn: ∃U0 : set, Pn U0.
We prove the intermediate claim HiUn0: i U = n0.
Use reflexivity.
We use U to witness the existential quantifier.
An exact proof term for the current goal is (andI (U ∈ Fam) (i U = n0) HUinFam HiUn0).
We prove the intermediate claim HPn: Pn (Eps_i Pn).
Apply HexPn to the current goal.
Let U0 be given.
Assume HPU0: Pn U0.
An exact proof term for the current goal is (Eps_i_ax Pn U0 HPU0).
We prove the intermediate claim HEpsFam: (Eps_i Pn) ∈ Fam.
An exact proof term for the current goal is (andEL ((Eps_i Pn) ∈ Fam) (i (Eps_i Pn) = n0) HPn).
We prove the intermediate claim HiEq: i (Eps_i Pn) = n0.
An exact proof term for the current goal is (andER ((Eps_i Pn) ∈ Fam) (i (Eps_i Pn) = n0) HPn).
We prove the intermediate claim HEpsEqU: (Eps_i Pn) = U.
An exact proof term for the current goal is (Hi_inj (Eps_i Pn) HEpsFam U HUinFam HiEq).
We prove the intermediate claim HUofEq: U_of n0 = Eps_i Pn.
We prove the intermediate claim HUdef: U_of n0 = if (∃U1 : set, U1 ∈ Fam ∧ i U1 = n0) then (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n0)) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
rewrite the current goal using (If_i_1 (∃U1 : set, U1 ∈ Fam ∧ i U1 = n0) (Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ i U0 = n0)) X HexPn) (from left to right).
Use reflexivity.
We prove the intermediate claim HxnotUof: x ∉ (U_of n0).
rewrite the current goal using HUofEq (from left to right).
rewrite the current goal using HEpsEqU (from left to right).
An exact proof term for the current goal is HxnotU.
We prove the intermediate claim HBdef: B_of n0 = X ∖ (U_of n0).
Use reflexivity.
rewrite the current goal using HBdef (from left to right).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxnotUof.
We prove the intermediate claim HtermPos: Rlt 0 delta.
An exact proof term for the current goal is (Hterm_Bpos n0 x Hn0O HxB).
We prove the intermediate claim Hseqgx: sequence_converges_metric R R_bounded_metric (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x)) (apply_fun g x).
An exact proof term for the current goal is (uniform_limit_metric_imp_sequence_converges_metric_at_point X R R_bounded_metric fn g x R_bounded_metric_is_metric_on_early Hfn Hgfun HxX Hgunif).
We prove the intermediate claim HdeltaR: delta ∈ R.
We prove the intermediate claim HtermC: continuous_map X Tx R R_standard_topology (term_of n0).
An exact proof term for the current goal is (Hterm_cont n0 Hn0O).
We prove the intermediate claim HtermFun: function_on (term_of n0) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (term_of n0) HtermC).
An exact proof term for the current goal is (HtermFun x HxX).
We prove the intermediate claim Heps: delta ∈ R ∧ Rlt 0 delta.
An exact proof term for the current goal is (andI (delta ∈ R) (Rlt 0 delta) HdeltaR HtermPos).
We prove the intermediate claim Htail: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun (graph ω (λn1 : set ⇒ apply_fun (apply_fun fn n1) x)) n,apply_fun g x)) delta.
An exact proof term for the current goal is (sequence_converges_metric_eps R R_bounded_metric (graph ω (λn1 : set ⇒ apply_fun (apply_fun fn n1) x)) (apply_fun g x) Hseqgx delta Heps).
Apply Htail to the current goal.
Let N be given.
Assume HNpair: N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun (graph ω (λn1 : set ⇒ apply_fun (apply_fun fn n1) x)) n,apply_fun g x)) delta.
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun (graph ω (λn1 : set ⇒ apply_fun (apply_fun fn n1) x)) n,apply_fun g x)) delta) HNpair).
We prove the intermediate claim Hprop: ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun (graph ω (λn1 : set ⇒ apply_fun (apply_fun fn n1) x)) n,apply_fun g x)) delta.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun (graph ω (λn1 : set ⇒ apply_fun (apply_fun fn n1) x)) n,apply_fun g x)) delta) HNpair).
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 Hn0Nat: nat_p n0.
An exact proof term for the current goal is (omega_nat_p n0 Hn0O).
Set m0 to be the term add_nat N (ordsucc n0).
We prove the intermediate claim Hm0Nat: nat_p m0.
An exact proof term for the current goal is (add_nat_p N HNnat (ordsucc n0) (nat_ordsucc n0 Hn0Nat)).
We prove the intermediate claim Hm0O: m0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega m0 Hm0Nat).
We prove the intermediate claim HNsub: N ⊆ m0.
An exact proof term for the current goal is (add_nat_Subq_R' N HNnat (ordsucc n0) (nat_ordsucc n0 Hn0Nat)).
We prove the intermediate claim Hclose: Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m0) x,apply_fun g x)) delta.
We prove the intermediate claim Hseqeq: apply_fun (graph ω (λn1 : set ⇒ apply_fun (apply_fun fn n1) x)) m0 = apply_fun (apply_fun fn m0) x.
An exact proof term for the current goal is (apply_fun_graph ω (λn1 : set ⇒ apply_fun (apply_fun fn n1) x) m0 Hm0O).
rewrite the current goal using Hseqeq (from right to left).
An exact proof term for the current goal is (Hprop m0 Hm0O HNsub).
We prove the intermediate claim Hclose0: Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m0) x,0)) delta.
We prove the intermediate claim HpairEq: (apply_fun (apply_fun fn m0) x,0) = (apply_fun (apply_fun fn m0) x,apply_fun g x).
Apply tuple_2_ext to the current goal.
Use reflexivity.
rewrite the current goal using Hgx0 (from right to left) at position 1.
Use reflexivity.
rewrite the current goal using HpairEq (from left to right) at position 1.
An exact proof term for the current goal is Hclose.
We prove the intermediate claim HdistGe: Rle delta (apply_fun R_bounded_metric (apply_fun (apply_fun fn m0) x,0)).
Set a to be the term apply_fun (apply_fun fn m0) x.
We prove the intermediate claim HaR: a ∈ R.
We prove the intermediate claim Hfm0: apply_fun fn m0 ∈ function_space X R.
An exact proof term for the current goal is (Hfn m0 Hm0O).
We prove the intermediate claim Hfm0_on: function_on (apply_fun fn m0) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn m0) X R Hfm0).
An exact proof term for the current goal is (Hfm0_on x HxX).
We prove the intermediate claim HpairEq: (apply_fun (apply_fun fn m0) x,0) = (a,0).
We prove the intermediate claim HaEq: apply_fun (apply_fun fn m0) x = a.
Use reflexivity.
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
An exact proof term for the current goal is (tuple_2_ext (apply_fun (apply_fun fn m0) x) 0 a 0 HaEq H00).
rewrite the current goal using HpairEq (from left to right) at position 1.
We prove the intermediate claim HbdEq: apply_fun R_bounded_metric (a,0) = R_bounded_distance a 0.
An exact proof term for the current goal is (R_bounded_metric_apply_early a 0 HaR real_0).
rewrite the current goal using HbdEq (from left to right).
We prove the intermediate claim HabR: abs_SNo a ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R a HaR).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HdeltaLe1: Rle delta 1.
Set eps0 to be the term eps_ (ordsucc n0).
We prove the intermediate claim Heps0O: ordsucc n0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n0 Hn0O).
We prove the intermediate claim Heps0R: eps0 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eps0 (SNo_eps_SNoS_omega (ordsucc n0) Heps0O)).
We prove the intermediate claim Heps0S: SNo eps0.
An exact proof term for the current goal is (real_SNo eps0 Heps0R).
We prove the intermediate claim Heps0pos: Rlt 0 eps0.
An exact proof term for the current goal is (RltI 0 eps0 real_0 Heps0R (SNo_eps_pos (ordsucc n0) Heps0O)).
We prove the intermediate claim H0leEps0R: Rle 0 eps0.
An exact proof term for the current goal is (Rlt_implies_Rle 0 eps0 Heps0pos).
We prove the intermediate claim H0leEps0: 0 ≤ eps0.
An exact proof term for the current goal is (SNoLe_of_Rle 0 eps0 H0leEps0R).
Set v to be the term apply_fun (vI_of n0) x.
We prove the intermediate claim HvI: continuous_map X Tx unit_interval unit_interval_topology (vI_of n0).
An exact proof term for the current goal is (HvI_cont n0 Hn0O).
We prove the intermediate claim HvIfun: function_on (vI_of n0) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (vI_of n0) HvI).
We prove the intermediate claim HvUI: v ∈ unit_interval.
An exact proof term for the current goal is (HvIfun x HxX).
We prove the intermediate claim HvR: v ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) v HvUI).
We prove the intermediate claim Hvcond: ¬ (Rlt v 0) ∧ ¬ (Rlt 1 v).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) v HvUI).
We prove the intermediate claim Hvle1': ¬ (Rlt 1 v).
An exact proof term for the current goal is (andER (¬ (Rlt v 0)) (¬ (Rlt 1 v)) Hvcond).
We prove the intermediate claim HvLe1R: Rle v 1.
Apply (RleI v 1 HvR real_1) to the current goal.
An exact proof term for the current goal is Hvle1'.
We prove the intermediate claim HvS: SNo v.
An exact proof term for the current goal is (real_SNo v HvR).
We prove the intermediate claim HvLe1: v ≤ 1.
An exact proof term for the current goal is (SNoLe_of_Rle v 1 HvLe1R).
We prove the intermediate claim HtermEq: delta = mul_SNo v eps0.
We prove the intermediate claim Htapp: apply_fun (term_of n0) x = apply_fun (mul_const_fun eps0) (apply_fun (vI_of n0) x).
An exact proof term for the current goal is (compose_fun_apply X (vI_of n0) (mul_const_fun eps0) x HxX).
rewrite the current goal using Htapp (from left to right).
We prove the intermediate claim HmulApp: apply_fun (mul_const_fun eps0) v = mul_SNo v eps0.
An exact proof term for the current goal is (mul_const_fun_apply eps0 v Heps0R HvR).
rewrite the current goal using HmulApp (from left to right).
Use reflexivity.
rewrite the current goal using HtermEq (from left to right).
We prove the intermediate claim HmulLeS: mul_SNo v eps0 ≤ eps0.
An exact proof term for the current goal is (mul_SNo_Le1_nonneg_Le v eps0 HvS Heps0S HvLe1 H0leEps0).
We prove the intermediate claim HmulLeR: Rle (mul_SNo v eps0) eps0.
An exact proof term for the current goal is (Rle_of_SNoLe (mul_SNo v eps0) eps0 (real_mul_SNo v HvR eps0 Heps0R) Heps0R HmulLeS).
We prove the intermediate claim Heps0Le1S: eps0 ≤ 1.
An exact proof term for the current goal is (eps_bd_1 (ordsucc n0) Heps0O).
We prove the intermediate claim Heps0Le1R: Rle eps0 1.
An exact proof term for the current goal is (Rle_of_SNoLe eps0 1 Heps0R real_1 Heps0Le1S).
An exact proof term for the current goal is (Rle_tra (mul_SNo v eps0) eps0 1 HmulLeR Heps0Le1R).
We prove the intermediate claim HaLeAbs: Rle a (abs_SNo a).
An exact proof term for the current goal is (Rle_of_SNoLe a (abs_SNo a) HaR HabR (abs_SNo_upper_bound a HaS)).
We prove the intermediate claim HdeltaLeA: Rle delta a.
We prove the intermediate claim HaDef: a = apply_fun (apply_fun fn m0) x.
Use reflexivity.
rewrite the current goal using HaDef (from left to right) at position 1.
We prove the intermediate claim HaPS: apply_fun (apply_fun fn m0) x = partial_sum x m0.
We prove the intermediate claim Hfnt: apply_fun fn m0 = s_fun m0.
An exact proof term for the current goal is (apply_fun_graph ω (λn1 : set ⇒ s_fun n1) m0 Hm0O).
rewrite the current goal using Hfnt (from left to right).
We prove the intermediate claim Hsdef: s_fun m0 = graph X (λx0 : set ⇒ partial_sum x0 m0).
Use reflexivity.
rewrite the current goal using Hsdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 m0) x HxX).
rewrite the current goal using HaPS (from left to right) at position 1.
We prove the intermediate claim Hm0def: m0 = add_nat N (ordsucc n0).
Use reflexivity.
We prove the intermediate claim Hm0comm: add_nat N (ordsucc n0) = add_nat (ordsucc n0) N.
An exact proof term for the current goal is (add_nat_com N HNnat (ordsucc n0) (nat_ordsucc n0 Hn0Nat)).
We prove the intermediate claim Hm0Eq: m0 = add_nat (ordsucc n0) N.
rewrite the current goal using Hm0def (from left to right).
An exact proof term for the current goal is Hm0comm.
rewrite the current goal using Hm0Eq (from left to right) at position 1.
We prove the intermediate claim HtermNN: ∀t : set, t ∈ ω → Rle 0 (apply_fun (term_of t) x).
Let t be given.
Assume HtO: t ∈ ω.
Set vt to be the term apply_fun (vI_of t) x.
We prove the intermediate claim HvI: continuous_map X Tx unit_interval unit_interval_topology (vI_of t).
An exact proof term for the current goal is (HvI_cont t HtO).
We prove the intermediate claim HvOn: function_on (vI_of t) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (vI_of t) HvI).
We prove the intermediate claim HvtUI: vt ∈ unit_interval.
An exact proof term for the current goal is (HvOn x HxX).
We prove the intermediate claim HvtR: vt ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) vt HvtUI).
We prove the intermediate claim Hvtcond: ¬ (Rlt vt 0) ∧ ¬ (Rlt 1 vt).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) vt HvtUI).
We prove the intermediate claim H0le_vtR: Rle 0 vt.
An exact proof term for the current goal is (RleI 0 vt real_0 HvtR (andEL (¬ (Rlt vt 0)) (¬ (Rlt 1 vt)) Hvtcond)).
We prove the intermediate claim H0le_vt: 0 ≤ vt.
An exact proof term for the current goal is (SNoLe_of_Rle 0 vt H0le_vtR).
We prove the intermediate claim HsuccO: ordsucc t ∈ ω.
An exact proof term for the current goal is (omega_ordsucc t HtO).
We prove the intermediate claim HepsR: eps_ (ordsucc t) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc t)) (SNo_eps_SNoS_omega (ordsucc t) HsuccO)).
We prove the intermediate claim HepsS: SNo (eps_ (ordsucc t)).
An exact proof term for the current goal is (real_SNo (eps_ (ordsucc t)) HepsR).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ (ordsucc t)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc t)) real_0 HepsR (SNo_eps_pos (ordsucc t) HsuccO)).
We prove the intermediate claim H0le_epsR: Rle 0 (eps_ (ordsucc t)).
An exact proof term for the current goal is (Rlt_implies_Rle 0 (eps_ (ordsucc t)) Hepspos).
We prove the intermediate claim H0le_eps: 0 ≤ eps_ (ordsucc t).
An exact proof term for the current goal is (SNoLe_of_Rle 0 (eps_ (ordsucc t)) H0le_epsR).
We prove the intermediate claim HtermApp: apply_fun (term_of t) x = mul_SNo vt (eps_ (ordsucc t)).
We prove the intermediate claim Htapp: apply_fun (term_of t) x = apply_fun (mul_const_fun (eps_ (ordsucc t))) (apply_fun (vI_of t) x).
An exact proof term for the current goal is (compose_fun_apply X (vI_of t) (mul_const_fun (eps_ (ordsucc t))) x HxX).
rewrite the current goal using Htapp (from left to right).
We prove the intermediate claim HmulApp: apply_fun (mul_const_fun (eps_ (ordsucc t))) vt = mul_SNo vt (eps_ (ordsucc t)).
An exact proof term for the current goal is (mul_const_fun_apply (eps_ (ordsucc t)) vt HepsR HvtR).
rewrite the current goal using HmulApp (from left to right).
Use reflexivity.
We prove the intermediate claim HmulR: mul_SNo vt (eps_ (ordsucc t)) ∈ R.
An exact proof term for the current goal is (real_mul_SNo vt HvtR (eps_ (ordsucc t)) HepsR).
We prove the intermediate claim HmulS: SNo (mul_SNo vt (eps_ (ordsucc t))).
An exact proof term for the current goal is (real_SNo (mul_SNo vt (eps_ (ordsucc t))) HmulR).
We prove the intermediate claim H0le_mul: 0 ≤ mul_SNo vt (eps_ (ordsucc t)).
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg vt (eps_ (ordsucc t)) (real_SNo vt HvtR) HepsS H0le_vt H0le_eps).
We prove the intermediate claim H0le_mulR: Rle 0 (mul_SNo vt (eps_ (ordsucc t))).
An exact proof term for the current goal is (Rle_of_SNoLe 0 (mul_SNo vt (eps_ (ordsucc t))) real_0 HmulR H0le_mul).
rewrite the current goal using HtermApp (from left to right).
An exact proof term for the current goal is H0le_mulR.
We prove the intermediate claim HpsNN: ∀k : set, nat_p k → Rle 0 (partial_sum x k).
Let k be given.
Assume HkNat: nat_p k.
We prove the intermediate claim HP0: Rle 0 (partial_sum x 0).
We prove the intermediate claim Hdef0: partial_sum x 0 = nat_primrec 0 (sum_step x) 0.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (nat_primrec_0 0 (sum_step x)) (from left to right).
An exact proof term for the current goal is (Rle_refl 0 real_0).
We prove the intermediate claim HPS: ∀m : set, nat_p m → Rle 0 (partial_sum x m) → Rle 0 (partial_sum x (ordsucc m)).
Let m be given.
Assume HmNat: nat_p m.
Assume IH: Rle 0 (partial_sum x m).
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (nat_p_omega m HmNat).
We prove the intermediate claim Hterm0: Rle 0 (apply_fun (term_of m) x).
An exact proof term for the current goal is (HtermNN m HmO).
We prove the intermediate claim HpsSucc: partial_sum x (ordsucc m) = add_SNo (partial_sum x m) (apply_fun (term_of m) x).
We prove the intermediate claim HdefS: partial_sum x (ordsucc m) = nat_primrec 0 (sum_step x) (ordsucc m).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc m) = sum_step x m (nat_primrec 0 (sum_step x) m).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) m HmNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) m = partial_sum x m.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim Hstepdef: sum_step x m (partial_sum x m) = add_SNo (partial_sum x m) (apply_fun (term_of m) x).
Use reflexivity.
rewrite the current goal using Hstepdef (from left to right).
Use reflexivity.
rewrite the current goal using HpsSucc (from left to right).
We prove the intermediate claim HpsR: partial_sum x m ∈ R.
We prove the intermediate claim Hfm: apply_fun fn m ∈ function_space X R.
An exact proof term for the current goal is (Hfn m HmO).
We prove the intermediate claim Hfm_on: function_on (apply_fun fn m) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn m) X R Hfm).
We prove the intermediate claim HfmEq: apply_fun (apply_fun fn m) x = partial_sum x m.
We prove the intermediate claim Hfnt: apply_fun fn m = s_fun m.
An exact proof term for the current goal is (apply_fun_graph ω (λn1 : set ⇒ s_fun n1) m HmO).
rewrite the current goal using Hfnt (from left to right).
We prove the intermediate claim Hsdef: s_fun m = graph X (λx0 : set ⇒ partial_sum x0 m).
Use reflexivity.
rewrite the current goal using Hsdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 m) x HxX).
rewrite the current goal using HfmEq (from right to left).
An exact proof term for the current goal is (Hfm_on x HxX).
We prove the intermediate claim HtermR: apply_fun (term_of m) x ∈ R.
We prove the intermediate claim HtC: continuous_map X Tx R R_standard_topology (term_of m).
An exact proof term for the current goal is (Hterm_cont m HmO).
We prove the intermediate claim HtFun: function_on (term_of m) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (term_of m) HtC).
An exact proof term for the current goal is (HtFun x HxX).
We prove the intermediate claim HsumR: add_SNo (partial_sum x m) (apply_fun (term_of m) x) ∈ R.
An exact proof term for the current goal is (real_add_SNo (partial_sum x m) HpsR (apply_fun (term_of m) x) HtermR).
We prove the intermediate claim HpsS: SNo (partial_sum x m).
An exact proof term for the current goal is (real_SNo (partial_sum x m) HpsR).
We prove the intermediate claim HtermS: SNo (apply_fun (term_of m) x).
An exact proof term for the current goal is (real_SNo (apply_fun (term_of m) x) HtermR).
We prove the intermediate claim H0le_ps: 0 ≤ partial_sum x m.
An exact proof term for the current goal is (SNoLe_of_Rle 0 (partial_sum x m) IH).
We prove the intermediate claim H0le_term: 0 ≤ apply_fun (term_of m) x.
An exact proof term for the current goal is (SNoLe_of_Rle 0 (apply_fun (term_of m) x) Hterm0).
We prove the intermediate claim H0le_sumS: 0 ≤ add_SNo (partial_sum x m) (apply_fun (term_of m) x).
We prove the intermediate claim Hle: add_SNo 0 0 ≤ add_SNo (partial_sum x m) (apply_fun (term_of m) x).
An exact proof term for the current goal is (add_SNo_Le3 0 0 (partial_sum x m) (apply_fun (term_of m) x) SNo_0 SNo_0 HpsS HtermS H0le_ps H0le_term).
We will prove 0 ≤ add_SNo (partial_sum x m) (apply_fun (term_of m) x).
rewrite the current goal using (add_SNo_0R 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Hle.
An exact proof term for the current goal is (Rle_of_SNoLe 0 (add_SNo (partial_sum x m) (apply_fun (term_of m) x)) real_0 HsumR H0le_sumS).
An exact proof term for the current goal is (nat_ind (λm : set ⇒ Rle 0 (partial_sum x m)) HP0 HPS k HkNat).
We prove the intermediate claim Hbase: Rle delta (partial_sum x (ordsucc n0)).
We prove the intermediate claim Hn0psNN: Rle 0 (partial_sum x n0).
An exact proof term for the current goal is (HpsNN n0 Hn0Nat).
We prove the intermediate claim HpsSucc: partial_sum x (ordsucc n0) = add_SNo (partial_sum x n0) (apply_fun (term_of n0) x).
We prove the intermediate claim HdefS: partial_sum x (ordsucc n0) = nat_primrec 0 (sum_step x) (ordsucc n0).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc n0) = sum_step x n0 (nat_primrec 0 (sum_step x) n0).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) n0 Hn0Nat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) n0 = partial_sum x n0.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim Hstepdef: sum_step x n0 (partial_sum x n0) = add_SNo (partial_sum x n0) (apply_fun (term_of n0) x).
Use reflexivity.
rewrite the current goal using Hstepdef (from left to right).
Use reflexivity.
rewrite the current goal using HpsSucc (from left to right).
We prove the intermediate claim HpsR: partial_sum x n0 ∈ R.
We prove the intermediate claim Hfm: apply_fun fn n0 ∈ function_space X R.
An exact proof term for the current goal is (Hfn n0 Hn0O).
We prove the intermediate claim Hfm_on: function_on (apply_fun fn n0) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn n0) X R Hfm).
We prove the intermediate claim HfmEq: apply_fun (apply_fun fn n0) x = partial_sum x n0.
We prove the intermediate claim Hfnt: apply_fun fn n0 = s_fun n0.
An exact proof term for the current goal is (apply_fun_graph ω (λn1 : set ⇒ s_fun n1) n0 Hn0O).
rewrite the current goal using Hfnt (from left to right).
We prove the intermediate claim Hsdef: s_fun n0 = graph X (λx0 : set ⇒ partial_sum x0 n0).
Use reflexivity.
rewrite the current goal using Hsdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 n0) x HxX).
rewrite the current goal using HfmEq (from right to left).
An exact proof term for the current goal is (Hfm_on x HxX).
We prove the intermediate claim HdeltaEq: delta = apply_fun (term_of n0) x.
Use reflexivity.
rewrite the current goal using HdeltaEq (from left to right).
We prove the intermediate claim HdeltaR': apply_fun (term_of n0) x ∈ R.
An exact proof term for the current goal is HdeltaR.
We prove the intermediate claim Hle: Rle (add_SNo 0 (apply_fun (term_of n0) x)) (add_SNo (partial_sum x n0) (apply_fun (term_of n0) x)).
An exact proof term for the current goal is (Rle_add_SNo_1 0 (partial_sum x n0) (apply_fun (term_of n0) x) real_0 HpsR HdeltaR' Hn0psNN).
We prove the intermediate claim HdeltaS: SNo (apply_fun (term_of n0) x).
An exact proof term for the current goal is (real_SNo (apply_fun (term_of n0) x) HdeltaR').
We prove the intermediate claim H0deltaEq: add_SNo 0 (apply_fun (term_of n0) x) = apply_fun (term_of n0) x.
An exact proof term for the current goal is (add_SNo_0L (apply_fun (term_of n0) x) HdeltaS).
We prove the intermediate claim Hle2: Rle (apply_fun (term_of n0) x) (add_SNo (partial_sum x n0) (apply_fun (term_of n0) x)).
rewrite the current goal using H0deltaEq (from right to left) at position 1.
An exact proof term for the current goal is Hle.
An exact proof term for the current goal is Hle2.
We prove the intermediate claim HP0: Rle delta (partial_sum x (add_nat (ordsucc n0) 0)).
rewrite the current goal using (add_nat_0R (ordsucc n0)) (from left to right).
An exact proof term for the current goal is Hbase.
We prove the intermediate claim HPS: ∀k : set, nat_p k → Rle delta (partial_sum x (add_nat (ordsucc n0) k)) → Rle delta (partial_sum x (add_nat (ordsucc n0) (ordsucc k))).
Let k be given.
Assume HkNat: nat_p k.
Assume IH: Rle delta (partial_sum x (add_nat (ordsucc n0) k)).
Set n to be the term add_nat (ordsucc n0) k.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (add_nat_p (ordsucc n0) (nat_ordsucc n0 Hn0Nat) k HkNat).
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 HaddS: add_nat (ordsucc n0) (ordsucc k) = ordsucc n.
An exact proof term for the current goal is (add_nat_SR (ordsucc n0) k HkNat).
rewrite the current goal using HaddS (from left to right).
We prove the intermediate claim HpsSucc: partial_sum x (ordsucc n) = add_SNo (partial_sum x n) (apply_fun (term_of n) x).
We prove the intermediate claim HdefS: partial_sum x (ordsucc n) = nat_primrec 0 (sum_step x) (ordsucc n).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc n) = sum_step x n (nat_primrec 0 (sum_step x) n).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) n HnNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) n = partial_sum x n.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim Hstepdef: sum_step x n (partial_sum x n) = add_SNo (partial_sum x n) (apply_fun (term_of n) x).
Use reflexivity.
rewrite the current goal using Hstepdef (from left to right).
Use reflexivity.
We prove the intermediate claim HpsnR: partial_sum x n ∈ R.
We prove the intermediate claim Hfnn: apply_fun fn n ∈ function_space X R.
An exact proof term for the current goal is (Hfn n HnO).
We prove the intermediate claim Hfnn_on: function_on (apply_fun fn n) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun fn n) X R Hfnn).
We prove the intermediate claim HfnnEq: apply_fun (apply_fun fn n) x = partial_sum x n.
We prove the intermediate claim Hfnt: apply_fun fn n = s_fun n.
An exact proof term for the current goal is (apply_fun_graph ω (λn1 : set ⇒ s_fun n1) n HnO).
rewrite the current goal using Hfnt (from left to right).
We prove the intermediate claim Hsdef: s_fun n = graph X (λx0 : set ⇒ partial_sum x0 n).
Use reflexivity.
rewrite the current goal using Hsdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 n) x HxX).
rewrite the current goal using HfnnEq (from right to left).
An exact proof term for the current goal is (Hfnn_on x HxX).
We prove the intermediate claim HtermnR: apply_fun (term_of n) x ∈ R.
We prove the intermediate claim HtC: continuous_map X Tx R R_standard_topology (term_of n).
An exact proof term for the current goal is (Hterm_cont n HnO).
We prove the intermediate claim HtFun: function_on (term_of n) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (term_of n) HtC).
An exact proof term for the current goal is (HtFun x HxX).
We prove the intermediate claim Hterm0: Rle 0 (apply_fun (term_of n) x).
An exact proof term for the current goal is (HtermNN n HnO).
We prove the intermediate claim Hinc: Rle (partial_sum x n) (partial_sum x (ordsucc n)).
rewrite the current goal using HpsSucc (from left to right).
We prove the intermediate claim Hle: Rle (add_SNo (partial_sum x n) 0) (add_SNo (partial_sum x n) (apply_fun (term_of n) x)).
An exact proof term for the current goal is (Rle_add_SNo_2 (partial_sum x n) 0 (apply_fun (term_of n) x) HpsnR real_0 HtermnR Hterm0).
We prove the intermediate claim HpsnS: SNo (partial_sum x n).
An exact proof term for the current goal is (real_SNo (partial_sum x n) HpsnR).
We prove the intermediate claim H0eq: add_SNo (partial_sum x n) 0 = partial_sum x n.
An exact proof term for the current goal is (add_SNo_0R (partial_sum x n) HpsnS).
We prove the intermediate claim Hle2: Rle (partial_sum x n) (add_SNo (partial_sum x n) (apply_fun (term_of n) x)).
rewrite the current goal using H0eq (from right to left) at position 1.
An exact proof term for the current goal is Hle.
An exact proof term for the current goal is Hle2.
An exact proof term for the current goal is (Rle_tra delta (partial_sum x n) (partial_sum x (ordsucc n)) IH Hinc).
An exact proof term for the current goal is (nat_ind (λk : set ⇒ Rle delta (partial_sum x (add_nat (ordsucc n0) k))) HP0 HPS N HNnat).
We prove the intermediate claim HdeltaLeAbs: Rle delta (abs_SNo a).
An exact proof term for the current goal is (Rle_tra delta a (abs_SNo a) HdeltaLeA HaLeAbs).
We prove the intermediate claim Hbddef: R_bounded_distance a 0 = (if Rlt (abs_SNo (add_SNo a (minus_SNo 0))) 1 then (abs_SNo (add_SNo a (minus_SNo 0))) else 1).
Use reflexivity.
rewrite the current goal using Hbddef (from left to right).
Apply (xm (Rlt (abs_SNo (add_SNo a (minus_SNo 0))) 1)) to the current goal.
Assume Hc: Rlt (abs_SNo (add_SNo a (minus_SNo 0))) 1.
We prove the intermediate claim HifEq: (if Rlt (abs_SNo (add_SNo a (minus_SNo 0))) 1 then (abs_SNo (add_SNo a (minus_SNo 0))) else 1) = (abs_SNo (add_SNo a (minus_SNo 0))).
An exact proof term for the current goal is (If_i_1 (Rlt (abs_SNo (add_SNo a (minus_SNo 0))) 1) (abs_SNo (add_SNo a (minus_SNo 0))) 1 Hc).
rewrite the current goal using HifEq (from left to right).
We prove the intermediate claim HargEq: add_SNo a (minus_SNo 0) = a.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is (add_SNo_0R a HaS).
rewrite the current goal using HargEq (from left to right).
An exact proof term for the current goal is HdeltaLeAbs.
Assume Hnc: ¬ (Rlt (abs_SNo (add_SNo a (minus_SNo 0))) 1).
We prove the intermediate claim HifEq0: (if Rlt (abs_SNo (add_SNo a (minus_SNo 0))) 1 then (abs_SNo (add_SNo a (minus_SNo 0))) else 1) = 1.
An exact proof term for the current goal is (If_i_0 (Rlt (abs_SNo (add_SNo a (minus_SNo 0))) 1) (abs_SNo (add_SNo a (minus_SNo 0))) 1 Hnc).
rewrite the current goal using HifEq0 (from left to right).
An exact proof term for the current goal is HdeltaLe1.
We prove the intermediate claim Hnlt: ¬ (Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m0) x,0)) delta).
An exact proof term for the current goal is (RleE_nlt delta (apply_fun R_bounded_metric (apply_fun (apply_fun fn m0) x,0)) HdistGe).
An exact proof term for the current goal is (Hnlt Hclose0).
An exact proof term for the current goal is (normalize01_fun_pos_of_neq0 (apply_fun g x) HgxR Hgxne0).
∎