Let X, Tx and A be given.
Assume Hnorm: normal_space X Tx.
Assume HAcl: closed_in X Tx A.
We will prove (Gdelta_in X Tx A ↔ ∃f : set, continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → x ∉ A → ¬ (apply_fun f x = 0))).
Apply iffI to the current goal.
Assume HGd: Gdelta_in X Tx A.
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 HGdpack.
We prove the intermediate claim Hcore: countable_set Fam ∧ ∀U ∈ Fam, open_in X Tx U.
An exact proof term for the current goal is (andEL (countable_set Fam ∧ ∀U ∈ Fam, open_in X Tx U) (intersection_over_family X Fam = A) HGdpack).
We prove the intermediate claim HIntEq: intersection_over_family X Fam = A.
An exact proof term for the current goal is (andER (countable_set Fam ∧ ∀U ∈ Fam, open_in X Tx U) (intersection_over_family X Fam = A) HGdpack).
We prove the intermediate claim HcountFam: countable_set Fam.
An exact proof term for the current goal is (andEL (countable_set Fam) (∀U ∈ Fam, open_in X Tx U) Hcore).
We prove the intermediate claim HopFam: ∀U ∈ Fam, open_in X Tx U.
An exact proof term for the current goal is (andER (countable_set Fam) (∀U ∈ Fam, open_in X Tx U) Hcore).
Apply HcountFam to the current goal.
Let i 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_open: ∀n : set, n ∈ ω → open_in X Tx (U_of n).
Let n be given.
Assume HnO: n ∈ ω.
Set P to be the term (λU : set ⇒ U ∈ Fam ∧ i U = n).
Apply (xm (∃U : set, P U)) to the current goal.
Assume HexU: ∃U : set, P U.
We prove the intermediate claim HP: P (Eps_i P).
Apply HexU to the current goal.
Let U be given.
Assume HPU: P U.
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 HUopen: open_in X Tx (Eps_i P).
An exact proof term for the current goal is (HopFam (Eps_i P) HUinFam).
We prove the intermediate claim HUeq: U_of n = Eps_i P.
We prove the intermediate claim HUdef: U_of n = if (∃U : set, P U) then (Eps_i P) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
We prove the intermediate claim L2: (if (∃U : set, P U) then (Eps_i P) else X) = Eps_i P.
An exact proof term for the current goal is (If_i_1 (∃U : set, P U) (Eps_i P) X HexU).
rewrite the current goal using L2 (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 HUopen.
Assume HnexU: ¬ (∃U : set, P U).
We prove the intermediate claim HUeq: U_of n = X.
We prove the intermediate claim HUdef: U_of n = if (∃U : set, P U) then (Eps_i P) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
We prove the intermediate claim L2: (if (∃U : set, P U) then (Eps_i P) else X) = X.
An exact proof term for the current goal is (If_i_0 (∃U : set, P U) (Eps_i P) X HnexU).
rewrite the current goal using L2 (from left to right).
Use reflexivity.
rewrite the current goal using HUeq (from left to right).
We will prove topology_on X Tx ∧ X ∈ Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
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 HUnopen: open_in X Tx (U_of n).
An exact proof term for the current goal is (HU_of_open n HnO).
We prove the intermediate claim HUninTx: U_of n ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (U_of n ∈ Tx) HUnopen).
An exact proof term for the current goal is (closed_of_open_complement X Tx (U_of n) HTx HUninTx).
We prove the intermediate claim HA_sub_Un: ∀n : set, n ∈ ω → A ⊆ U_of n.
Let n be given.
Assume HnO: n ∈ ω.
Set P to be the term (λU : set ⇒ U ∈ Fam ∧ i U = n).
Apply (xm (∃U : set, P U)) to the current goal.
Assume HexU: ∃U : set, P U.
We prove the intermediate claim HP: P (Eps_i P).
Apply HexU to the current goal.
Let U be given.
Assume HPU: P U.
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, P U) then (Eps_i P) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
We prove the intermediate claim L2: (if (∃U : set, P U) then (Eps_i P) else X) = Eps_i P.
An exact proof term for the current goal is (If_i_1 (∃U : set, P U) (Eps_i P) X HexU).
rewrite the current goal using L2 (from left to right).
Use reflexivity.
rewrite the current goal using HUeq (from left to right).
Let x be given.
Assume HxA: x ∈ A.
We will prove x ∈ (Eps_i P).
We prove the intermediate claim HxInt: x ∈ intersection_over_family X Fam.
rewrite the current goal using HIntEq (from left to right).
An exact proof term for the current goal is HxA.
We prove the intermediate claim HIntDef: intersection_over_family X Fam = {x0 ∈ X|∀U0 : set, U0 ∈ Fam → x0 ∈ U0}.
Use reflexivity.
We prove the intermediate claim HxInt2: x ∈ {x0 ∈ X|∀U0 : set, U0 ∈ Fam → x0 ∈ U0}.
rewrite the current goal using HIntDef (from right to left).
An exact proof term for the current goal is HxInt.
We prove the intermediate claim Hall: ∀U0 : set, U0 ∈ Fam → x ∈ U0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam → x0 ∈ U0) x HxInt2).
An exact proof term for the current goal is (Hall (Eps_i P) HUinFam).
Assume HnexU: ¬ (∃U : set, P U).
We prove the intermediate claim HUeq: U_of n = X.
We prove the intermediate claim HUdef: U_of n = if (∃U : set, P U) then (Eps_i P) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
We prove the intermediate claim L2: (if (∃U : set, P U) then (Eps_i P) else X) = X.
An exact proof term for the current goal is (If_i_0 (∃U : set, P U) (Eps_i P) X HnexU).
rewrite the current goal using L2 (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 (closed_in_subset X Tx A HAcl).
We prove the intermediate claim HdisjAB: ∀n : set, n ∈ ω → A ∩ (B_of n) = Empty.
Let n be given.
Assume HnO: n ∈ ω.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume Hx: x ∈ A ∩ (B_of n).
We will prove x ∈ Empty.
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 Hx).
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 Hx).
We prove the intermediate claim HxU: x ∈ U_of n.
An exact proof term for the current goal is (HA_sub_Un n HnO x HxA).
We prove the intermediate claim HxNotU: 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 (HxNotU HxU).
Set u_of to be the term (λn : set ⇒ Eps_i (λu : set ⇒ continuous_map X Tx (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) u ∧ (∀x : set, x ∈ A → apply_fun u x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun u x = eps_ (ordsucc n)))).
We prove the intermediate claim Hu_of_prop: ∀n : set, n ∈ ω → continuous_map X Tx (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) (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)).
Let n be given.
Assume HnO: n ∈ ω.
Set I to be the term closed_interval 0 (eps_ (ordsucc n)).
Set Ti to be the term closed_interval_topology 0 (eps_ (ordsucc n)).
Set P to be the term (λu : set ⇒ continuous_map X Tx I Ti u ∧ (∀x : set, x ∈ A → apply_fun u x = 0) ∧ (∀x : set, x ∈ (B_of n) → apply_fun u x = eps_ (ordsucc n))).
We prove the intermediate claim Hexu: ∃u : set, P u.
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) (omega_ordsucc n HnO))).
We prove the intermediate claim HepsPosS: 0 < eps_ (ordsucc n).
An exact proof term for the current goal is (SNo_eps_pos (ordsucc n) (omega_ordsucc n HnO)).
We prove the intermediate claim HepsPos: Rlt 0 (eps_ (ordsucc n)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc n)) real_0 HepsR HepsPosS).
We prove the intermediate claim H0le: Rle 0 (eps_ (ordsucc n)).
An exact proof term for the current goal is (Rlt_implies_Rle 0 (eps_ (ordsucc n)) 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 (HdisjAB n HnO).
An exact proof term for the current goal is (Urysohn_lemma X Tx A (B_of n) 0 (eps_ (ordsucc n)) H0le Hnorm HAcl HBcl Hdisj).
Apply Hexu to the current goal.
Let u be given.
Assume Hu: P u.
An exact proof term for the current goal is (Eps_i_ax P u Hu).
We prove the intermediate claim Hu_contR: ∀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 Hu12: continuous_map X Tx (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) (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 (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) (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)) (Hu_of_prop n HnO)).
We prove the intermediate claim HuI: continuous_map X Tx (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) (u_of n).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) (u_of n)) (∀x : set, x ∈ A → apply_fun (u_of n) x = 0) Hu12).
We prove the intermediate claim HI_sub_R: closed_interval 0 (eps_ (ordsucc n)) ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R 0 (eps_ (ordsucc n))).
We prove the intermediate claim HTiEq: closed_interval_topology 0 (eps_ (ordsucc n)) = subspace_topology R R_standard_topology (closed_interval 0 (eps_ (ordsucc n))).
Use reflexivity.
An exact proof term for the current goal is (continuous_map_range_expand X Tx (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) R R_standard_topology (u_of n) HuI HI_sub_R R_standard_topology_is_topology_local HTiEq).
Set Base to be the term const_fun X 0.
Set Step to be the term (λk st : set ⇒ compose_fun X (pair_map X st (u_of k)) add_fun_R).
Set State to be the term (λn : set ⇒ nat_primrec Base Step n).
Set fn to be the term graph ω (λn : set ⇒ State n).
We prove the intermediate claim HfnFS: function_on fn ω (function_space X R).
We prove the intermediate claim HStateFS_nat: ∀n : set, nat_p n → State n ∈ function_space X R.
Apply nat_ind to the current goal.
We will prove State 0 ∈ function_space X R.
We prove the intermediate claim H0: State 0 = Base.
An exact proof term for the current goal is (nat_primrec_0 Base Step).
rewrite the current goal using H0 (from left to right).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
Set f0 to be the term const_fun X 0.
We prove the intermediate claim Hsub: f0 ⊆ setprod X R.
Let q be given.
Assume Hq: q ∈ f0.
We will prove q ∈ setprod X R.
Apply (ReplE_impred X (λa0 : set ⇒ (a0,0)) q Hq (q ∈ setprod X R)) to the current goal.
Let a be given.
Assume HaX: a ∈ X.
Assume Heq: q = (a,0).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X R a 0 HaX H0R).
We prove the intermediate claim Hpow: f0 ∈ 𝒫 (setprod X R).
An exact proof term for the current goal is (PowerI (setprod X R) f0 Hsub).
We prove the intermediate claim Hfun: function_on f0 X R.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun f0 x ∈ R.
rewrite the current goal using (const_fun_apply X 0 x HxX) (from left to right).
An exact proof term for the current goal is H0R.
An exact proof term for the current goal is (SepI (𝒫 (setprod X R)) (λf : set ⇒ function_on f X R) f0 Hpow Hfun).
Let n be given.
Assume HnNat: nat_p n.
Assume IH: State n ∈ function_space X R.
We will prove State (ordsucc n) ∈ function_space X R.
We prove the intermediate claim HS: State (ordsucc n) = Step n (State n).
An exact proof term for the current goal is (nat_primrec_S Base Step n HnNat).
rewrite the current goal using HS (from left to right).
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 HstFun: function_on (State n) X R.
An exact proof term for the current goal is (function_on_of_function_space (State n) X R IH).
We prove the intermediate claim HukFun: function_on (u_of n) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (u_of n) (Hu_contR n HnO)).
We prove the intermediate claim HpairFS: pair_map X (State n) (u_of n) ∈ function_space X (setprod R R).
An exact proof term for the current goal is (pair_map_in_function_space X R R (State n) (u_of n) HstFun HukFun).
We prove the intermediate claim HpairFun: function_on (pair_map X (State n) (u_of n)) X (setprod R R).
An exact proof term for the current goal is (function_on_of_function_space (pair_map X (State n) (u_of n)) X (setprod R R) HpairFS).
We prove the intermediate claim HaddFS: add_fun_R ∈ function_space (setprod R R) R.
An exact proof term for the current goal is add_fun_R_in_function_space.
We prove the intermediate claim HaddFun: function_on add_fun_R (setprod R R) R.
An exact proof term for the current goal is (function_on_of_function_space add_fun_R (setprod R R) R HaddFS).
An exact proof term for the current goal is (compose_fun_in_function_space X (setprod R R) R (pair_map X (State n) (u_of n)) add_fun_R HpairFun HaddFun).
We prove the intermediate claim HfnMem: fn ∈ function_space ω (function_space X R).
We prove the intermediate claim Hdef: fn = graph ω (λn0 : set ⇒ State n0).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (graph_in_function_space ω (function_space X R) (λn0 : set ⇒ State n0)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
An exact proof term for the current goal is (HStateFS_nat n (omega_nat_p n HnO)).
An exact proof term for the current goal is (function_on_of_function_space fn ω (function_space X R) HfnMem).
We prove the intermediate claim HfnCont: ∀n : set, n ∈ ω → continuous_map X Tx R R_standard_topology (apply_fun fn n).
We prove the intermediate claim HTyR: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HStateCont_nat: ∀n : set, nat_p n → continuous_map X Tx R R_standard_topology (State n).
Apply nat_ind to the current goal.
We will prove continuous_map X Tx R R_standard_topology (State 0).
We prove the intermediate claim H0: State 0 = Base.
An exact proof term for the current goal is (nat_primrec_0 Base Step).
rewrite the current goal using H0 (from left to right).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is (const_fun_continuous X Tx R R_standard_topology 0 HTx HTyR H0R).
Let n be given.
Assume HnNat: nat_p n.
Assume IH: continuous_map X Tx R R_standard_topology (State n).
We will prove continuous_map X Tx R R_standard_topology (State (ordsucc n)).
We prove the intermediate claim HS: State (ordsucc n) = Step n (State n).
An exact proof term for the current goal is (nat_primrec_S Base Step n HnNat).
rewrite the current goal using HS (from left to right).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (nat_p_omega n HnNat).
Set h to be the term pair_map X (State n) (u_of n).
We prove the intermediate claim Hhcont: continuous_map X Tx (setprod R R) (product_topology R R_standard_topology R R_standard_topology) h.
An exact proof term for the current goal is (maps_into_products_axiom X Tx R R_standard_topology R R_standard_topology (State n) (u_of n) IH (Hu_contR n HnO)).
We prove the intermediate claim Haddcont: continuous_map (setprod R R) (product_topology R R_standard_topology R R_standard_topology) R R_standard_topology add_fun_R.
An exact proof term for the current goal is add_fun_R_continuous.
An exact proof term for the current goal is (composition_continuous X Tx (setprod R R) (product_topology R R_standard_topology R R_standard_topology) R R_standard_topology h add_fun_R Hhcont Haddcont).
Let n be given.
Assume HnO: n ∈ ω.
rewrite the current goal using (apply_fun_graph ω (λn0 : set ⇒ State n0) n HnO) (from left to right).
An exact proof term for the current goal is (HStateCont_nat n (omega_nat_p n HnO)).
We prove the intermediate claim HfnUC: 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 (HfnFS 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 (HfnFS 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 (HfnFS (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 (HfnFS (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 (u_of t) x.
We prove the intermediate claim Hu1: continuous_map X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t).
We prove the intermediate claim Hu12: continuous_map X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of t) x0 = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of t) x0 = 0)) (∀x0 : set, x0 ∈ (B_of t) → apply_fun (u_of t) x0 = eps_ (ordsucc t)) (Hu_of_prop t HtO)).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t)) (∀x0 : set, x0 ∈ A → apply_fun (u_of t) x0 = 0) Hu12).
We prove the intermediate claim HuOn: function_on (u_of t) X (closed_interval 0 (eps_ (ordsucc t))).
An exact proof term for the current goal is (continuous_map_function_on X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t) Hu1).
We prove the intermediate claim HuIn0: apply_fun (u_of t) x ∈ closed_interval 0 (eps_ (ordsucc t)).
An exact proof term for the current goal is (HuOn x HxX).
We prove the intermediate claim HuIn: u ∈ closed_interval 0 (eps_ (ordsucc t)).
An exact proof term for the current goal is HuIn0.
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 Hubounds: Rle 0 u ∧ Rle u (eps_ (ordsucc t)).
An exact proof term for the current goal is (closed_interval_bounds 0 (eps_ (ordsucc t)) u real_0 HepsSuccR HuIn).
We prove the intermediate claim H0leuR: Rle 0 u.
An exact proof term for the current goal is (andEL (Rle 0 u) (Rle u (eps_ (ordsucc t))) Hubounds).
We prove the intermediate claim HuLeR: Rle u (eps_ (ordsucc t)).
An exact proof term for the current goal is (andER (Rle 0 u) (Rle u (eps_ (ordsucc t))) Hubounds).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R 0 (eps_ (ordsucc t)) u HuIn).
We prove the intermediate claim HuxR: apply_fun (u_of t) x ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R 0 (eps_ (ordsucc t)) (apply_fun (u_of t) x) HuIn0).
We prove the intermediate claim HuS: SNo u.
An exact proof term for the current goal is (real_SNo u HuR).
We prove the intermediate claim H0leu: 0 ≤ u.
An exact proof term for the current goal is (SNoLe_of_Rle 0 u H0leuR).
We prove the intermediate claim HuLe: u ≤ eps_ (ordsucc t).
An exact proof term for the current goal is (SNoLe_of_Rle u (eps_ (ordsucc t)) HuLeR).
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 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 HuLt1: u < 1.
An exact proof term for the current goal is (SNoLeLt_tra u (eps_ (ordsucc t)) 1 HuS 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 HuR real_1 HuLt1).
We prove the intermediate claim HaEq: apply_fun fn t = State t.
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ State n0) t HtO).
We prove the intermediate claim HbEq0: apply_fun fn (ordsucc t) = State (ordsucc t).
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ State n0) (ordsucc t) HtSuccO).
We prove the intermediate claim HbState: State (ordsucc t) = Step t (State t).
An exact proof term for the current goal is (nat_primrec_S Base Step t HtNat).
We prove the intermediate claim HstepDef: Step t (State t) = compose_fun X (pair_map X (State t) (u_of t)) add_fun_R.
Use reflexivity.
We prove the intermediate claim HbEq: b = add_SNo a u.
rewrite the current goal using HbEq0 (from left to right) at position 1.
rewrite the current goal using HbState (from left to right) at position 1.
rewrite the current goal using HstepDef (from left to right) at position 1.
We prove the intermediate claim HstRx: apply_fun (State t) x ∈ R.
rewrite the current goal using HaEq (from right to left).
An exact proof term for the current goal is HaR.
We prove the intermediate claim HbEq1: apply_fun (compose_fun X (pair_map X (State t) (u_of t)) add_fun_R) x = add_SNo (apply_fun (State t) x) (apply_fun (u_of t) x).
An exact proof term for the current goal is (add_of_pair_map_apply X (State t) (u_of t) x HxX HstRx HuxR).
rewrite the current goal using HbEq1 (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 HuS).
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 HuS).
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 HuS).
rewrite the current goal using Habsm (from left to right).
An exact proof term for the current goal is (nonneg_abs_SNo u H0leu).
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.
rewrite the current goal using (R_bounded_metric_apply_early a b HaR HbR) (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).
rewrite the current goal using (If_i_1 (Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1) (abs_SNo (add_SNo a (minus_SNo b))) 1 HabsLt1) (from left to right).
rewrite the current goal using HabsEq (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 (HfnFS 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 (HfnFS 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: ∃f : set, function_on f X R ∧ uniform_limit_metric X R R_bounded_metric fn f ∧ continuous_map X Tx R R_standard_topology f.
An exact proof term for the current goal is (uniform_cauchy_continuous_to_R_has_continuous_limit X Tx fn HTx HfnFS HfnCont HfnUC).
Apply Hexlim to the current goal.
Let f be given.
Assume Hfpack: function_on f X R ∧ uniform_limit_metric X R R_bounded_metric fn f ∧ continuous_map X Tx R R_standard_topology f.
We use f to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (andER (function_on f X R ∧ uniform_limit_metric X R R_bounded_metric fn f) (continuous_map X Tx R R_standard_topology f) Hfpack).
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun f x = 0.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate claim Hf12: function_on f X R ∧ uniform_limit_metric X R R_bounded_metric fn f.
An exact proof term for the current goal is (andEL (function_on f X R ∧ uniform_limit_metric X R R_bounded_metric fn f) (continuous_map X Tx R R_standard_topology f) Hfpack).
We prove the intermediate claim Hf_fun: function_on f X R.
An exact proof term for the current goal is (andEL (function_on f X R) (uniform_limit_metric X R R_bounded_metric fn f) Hf12).
We prove the intermediate claim Hf_unif: uniform_limit_metric X R R_bounded_metric fn f.
An exact proof term for the current goal is (andER (function_on f X R) (uniform_limit_metric X R R_bounded_metric fn f) Hf12).
Set seqx to be the term graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x).
We prove the intermediate claim Hu_zero: ∀n : set, n ∈ ω → apply_fun (u_of n) x = 0.
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim H12: continuous_map X Tx (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) (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 (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) (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)) (Hu_of_prop n HnO)).
We prove the intermediate claim Hz: ∀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 (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) (u_of n)) (∀x0 : set, x0 ∈ A → apply_fun (u_of n) x0 = 0) H12).
An exact proof term for the current goal is (Hz x HxA).
We prove the intermediate claim HState0A_nat: ∀n : set, nat_p n → apply_fun (State n) x = 0.
Apply nat_ind to the current goal.
We will prove apply_fun (State 0) x = 0.
We prove the intermediate claim H0: State 0 = Base.
An exact proof term for the current goal is (nat_primrec_0 Base Step).
rewrite the current goal using H0 (from left to right).
rewrite the current goal using (const_fun_apply X 0 x HxX) (from left to right).
Use reflexivity.
Let n be given.
Assume HnNat: nat_p n.
Assume IH: apply_fun (State n) x = 0.
We will prove apply_fun (State (ordsucc n)) x = 0.
We prove the intermediate claim HS: State (ordsucc n) = Step n (State n).
An exact proof term for the current goal is (nat_primrec_S Base Step n HnNat).
rewrite the current goal using HS (from left to right).
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 HstepDef: Step n (State n) = compose_fun X (pair_map X (State n) (u_of n)) add_fun_R.
Use reflexivity.
rewrite the current goal using HstepDef (from left to right).
We prove the intermediate claim L2: apply_fun (compose_fun X (pair_map X (State n) (u_of n)) add_fun_R) x = apply_fun add_fun_R (apply_fun (pair_map X (State n) (u_of n)) x).
An exact proof term for the current goal is (compose_fun_apply X (pair_map X (State n) (u_of n)) add_fun_R x HxX).
rewrite the current goal using L2 (from left to right).
We prove the intermediate claim L3: apply_fun (pair_map X (State n) (u_of n)) x = (apply_fun (State n) x,apply_fun (u_of n) x).
An exact proof term for the current goal is (pair_map_apply X R R (State n) (u_of n) x HxX).
rewrite the current goal using L3 (from left to right) at position 1.
We prove the intermediate claim HstRx: apply_fun (State n) x ∈ R.
rewrite the current goal using IH (from left to right).
An exact proof term for the current goal is real_0.
We prove the intermediate claim HukFun: function_on (u_of n) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (u_of n) (Hu_contR n HnO)).
We prove the intermediate claim HukRx: apply_fun (u_of n) x ∈ R.
An exact proof term for the current goal is (HukFun x HxX).
We prove the intermediate claim HpRR: (apply_fun (State n) x,apply_fun (u_of n) x) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (apply_fun (State n) x) (apply_fun (u_of n) x) HstRx HukRx).
We prove the intermediate claim L4: apply_fun add_fun_R (apply_fun (State n) x,apply_fun (u_of n) x) = add_SNo ((apply_fun (State n) x,apply_fun (u_of n) x) 0) ((apply_fun (State n) x,apply_fun (u_of n) x) 1).
An exact proof term for the current goal is (add_fun_R_apply (apply_fun (State n) x,apply_fun (u_of n) x) HpRR).
rewrite the current goal using L4 (from left to right).
rewrite the current goal using (tuple_2_0_eq (apply_fun (State n) x) (apply_fun (u_of n) x)) (from left to right).
rewrite the current goal using (tuple_2_1_eq (apply_fun (State n) x) (apply_fun (u_of n) x)) (from left to right).
rewrite the current goal using IH (from left to right).
We prove the intermediate claim L5: apply_fun (u_of n) x = 0.
An exact proof term for the current goal is (Hu_zero n HnO).
rewrite the current goal using L5 (from left to right).
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hseq0: ∀n : set, n ∈ ω → apply_fun seqx n = 0.
Let n be given.
Assume HnO: n ∈ ω.
rewrite the current goal using (apply_fun_graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x) n HnO) (from left to right).
rewrite the current goal using (apply_fun_graph ω (λn0 : set ⇒ State n0) n HnO) (from left to right).
An exact proof term for the current goal is (HState0A_nat n (omega_nat_p n HnO)).
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 HTopR: topology_on R (metric_topology R R_bounded_metric).
An exact proof term for the current goal is (metric_topology_is_topology R R_bounded_metric HmR).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hconv0: converges_to R (metric_topology R R_bounded_metric) seqx 0.
We will prove topology_on R (metric_topology R R_bounded_metric) ∧ sequence_on seqx R ∧ 0 ∈ R ∧ ∀U : set, U ∈ (metric_topology R R_bounded_metric) → 0 ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqx n ∈ U.
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 HTopR.
We will prove sequence_on seqx R.
Let n be given.
Assume HnO: n ∈ ω.
We will prove apply_fun seqx n ∈ R.
rewrite the current goal using (Hseq0 n HnO) (from left to right).
An exact proof term for the current goal is H0R.
An exact proof term for the current goal is H0R.
Let U be given.
Assume HU: U ∈ metric_topology R R_bounded_metric.
Assume H0U: 0 ∈ U.
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 H0sub: 0 ⊆ n.
rewrite the current goal using (Hseq0 n HnO) (from left to right).
An exact proof term for the current goal is H0U.
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (Hf_fun x HxX).
We prove the intermediate claim Hconvfx: converges_to R (metric_topology R R_bounded_metric) seqx (apply_fun f x).
An exact proof term for the current goal is (uniform_limit_metric_imp_converges_to_metric_topology_at_point X R R_bounded_metric fn f x HmR HfnFS Hf_fun HxX Hf_unif).
Apply (xm (apply_fun f x = 0)) to the current goal.
Assume Heq: apply_fun f x = 0.
An exact proof term for the current goal is Heq.
Assume Hneq: ¬ (apply_fun f x = 0).
We will prove apply_fun f x = 0.
Apply FalseE to the current goal.
We prove the intermediate claim Hneq0: 0 ≠ apply_fun f x.
Assume H0eq: 0 = apply_fun f x.
We prove the intermediate claim Heq: apply_fun f x = 0.
rewrite the current goal using H0eq (from right to left).
Use reflexivity.
An exact proof term for the current goal is (Hneq Heq).
We prove the intermediate claim HHaus: Hausdorff_space R (metric_topology R R_bounded_metric).
An exact proof term for the current goal is (metric_topology_Hausdorff R R_bounded_metric HmR).
We prove the intermediate claim Hseq_on: function_on seqx ω R.
An exact proof term for the current goal is (converges_to_sequence_on R (metric_topology R R_bounded_metric) seqx 0 Hconv0).
We prove the intermediate claim Hpack0: ((topology_on R (metric_topology R R_bounded_metric) ∧ sequence_on seqx R) ∧ 0 ∈ R) ∧ (∀U : set, U ∈ metric_topology R R_bounded_metric → 0 ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqx n ∈ U).
An exact proof term for the current goal is Hconv0.
We prove the intermediate claim Htail0: ∀U : set, U ∈ metric_topology R R_bounded_metric → 0 ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqx n ∈ U.
An exact proof term for the current goal is (andER ((topology_on R (metric_topology R R_bounded_metric) ∧ sequence_on seqx R) ∧ 0 ∈ R) (∀U : set, U ∈ metric_topology R R_bounded_metric → 0 ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqx n ∈ U) Hpack0).
We prove the intermediate claim Hpackf: ((topology_on R (metric_topology R R_bounded_metric) ∧ sequence_on seqx R) ∧ apply_fun f x ∈ R) ∧ (∀U : set, U ∈ metric_topology R R_bounded_metric → apply_fun f x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqx n ∈ U).
An exact proof term for the current goal is Hconvfx.
We prove the intermediate claim Htailf: ∀U : set, U ∈ metric_topology R R_bounded_metric → apply_fun f x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqx n ∈ U.
An exact proof term for the current goal is (andER ((topology_on R (metric_topology R R_bounded_metric) ∧ sequence_on seqx R) ∧ apply_fun f x ∈ R) (∀U : set, U ∈ metric_topology R R_bounded_metric → apply_fun f x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqx n ∈ U) Hpackf).
An exact proof term for the current goal is (Hausdorff_unique_limits R (metric_topology R R_bounded_metric) seqx 0 (apply_fun f x) HHaus H0R HfxR Hneq0 Hseq_on Htail0 Htailf).
Let x be given.
Assume HxX: x ∈ X.
Assume HxNA: x ∉ A.
We will prove ¬ (apply_fun f x = 0).
Assume Hfx0: apply_fun f x = 0.
We will prove False.
We prove the intermediate claim Hf12: function_on f X R ∧ uniform_limit_metric X R R_bounded_metric fn f.
An exact proof term for the current goal is (andEL (function_on f X R ∧ uniform_limit_metric X R R_bounded_metric fn f) (continuous_map X Tx R R_standard_topology f) Hfpack).
We prove the intermediate claim Hf_fun: function_on f X R.
An exact proof term for the current goal is (andEL (function_on f X R) (uniform_limit_metric X R R_bounded_metric fn f) Hf12).
We prove the intermediate claim Hf_unif: uniform_limit_metric X R R_bounded_metric fn f.
An exact proof term for the current goal is (andER (function_on f X R) (uniform_limit_metric X R R_bounded_metric fn f) Hf12).
We prove the intermediate claim HxNotInt: ¬ (x ∈ intersection_over_family X Fam).
Assume HxInt: x ∈ intersection_over_family X Fam.
We prove the intermediate claim HxA: x ∈ A.
rewrite the current goal using HIntEq (from right to left).
An exact proof term for the current goal is HxInt.
An exact proof term for the current goal is (HxNA HxA).
We prove the intermediate claim HexU: ∃U : set, U ∈ Fam ∧ x ∉ U.
Apply (xm (∃U : set, U ∈ Fam ∧ x ∉ U)) to the current goal.
Assume Hex: ∃U : set, U ∈ Fam ∧ x ∉ U.
An exact proof term for the current goal is Hex.
Assume Hnex: ¬ (∃U : set, U ∈ Fam ∧ x ∉ U).
Apply FalseE to the current goal.
We prove the intermediate claim Hall: ∀U0 : set, U0 ∈ Fam → x ∈ U0.
Let U0 be given.
Assume HU0: U0 ∈ Fam.
Apply (xm (x ∈ U0)) to the current goal.
Assume HxU0: x ∈ U0.
An exact proof term for the current goal is HxU0.
Assume HxNotU0: ¬ (x ∈ U0).
We will prove x ∈ U0.
Apply FalseE to the current goal.
We prove the intermediate claim Hexbad: ∃U : set, U ∈ Fam ∧ x ∉ U.
We use U0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU0.
An exact proof term for the current goal is HxNotU0.
An exact proof term for the current goal is (Hnex Hexbad).
We prove the intermediate claim HxIntSep: x ∈ {x0 ∈ X|∀U0 : set, U0 ∈ Fam → x0 ∈ U0}.
Apply (SepI X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam → x0 ∈ U0) x HxX) to the current goal.
An exact proof term for the current goal is Hall.
We prove the intermediate claim HxInt2: x ∈ intersection_over_family X Fam.
We prove the intermediate claim HIntDef: intersection_over_family X Fam = {x0 ∈ X|∀U0 : set, U0 ∈ Fam → x0 ∈ U0}.
Use reflexivity.
rewrite the current goal using HIntDef (from left to right).
An exact proof term for the current goal is HxIntSep.
An exact proof term for the current goal is (HxNotInt HxInt2).
Apply HexU to the current goal.
Let U be given.
Assume HUpair: U ∈ Fam ∧ x ∉ U.
We prove the intermediate claim HUinFam: U ∈ Fam.
An exact proof term for the current goal is (andEL (U ∈ Fam) (x ∉ U) HUpair).
We prove the intermediate claim HxNotU: x ∉ U.
An exact proof term for the current goal is (andER (U ∈ Fam) (x ∉ U) HUpair).
Set n to be the term i U.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (Hi_to_omega U HUinFam).
Set Pn to be the term (λV : set ⇒ V ∈ Fam ∧ i V = n).
We prove the intermediate claim HexPn: ∃V : set, Pn V.
We use U to witness the existential quantifier.
We will prove U ∈ Fam ∧ i U = n.
Apply andI to the current goal.
An exact proof term for the current goal is HUinFam.
Use reflexivity.
We prove the intermediate claim HPn: Pn (Eps_i Pn).
Apply HexPn to the current goal.
Let V be given.
Assume HPV: Pn V.
An exact proof term for the current goal is (Eps_i_ax Pn V HPV).
We prove the intermediate claim HUofEq: U_of n = U.
We prove the intermediate claim HUdef: U_of n = if (∃V : set, Pn V) then (Eps_i Pn) else X.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
We prove the intermediate claim HUif: (if (∃V : set, Pn V) then (Eps_i Pn) else X) = Eps_i Pn.
An exact proof term for the current goal is (If_i_1 (∃V : set, Pn V) (Eps_i Pn) X HexPn).
rewrite the current goal using HUif (from left to right).
We prove the intermediate claim HEpsIn: (Eps_i Pn) ∈ Fam.
An exact proof term for the current goal is (andEL ((Eps_i Pn) ∈ Fam) (i (Eps_i Pn) = n) HPn).
We prove the intermediate claim HEpsCode: i (Eps_i Pn) = n.
An exact proof term for the current goal is (andER ((Eps_i Pn) ∈ Fam) (i (Eps_i Pn) = n) HPn).
We prove the intermediate claim HnDef: n = i U.
Use reflexivity.
We prove the intermediate claim HEpsCode2: i (Eps_i Pn) = i U.
rewrite the current goal using HnDef (from left to right) at position 2.
An exact proof term for the current goal is HEpsCode.
An exact proof term for the current goal is (Hi_inj (Eps_i Pn) HEpsIn U HUinFam HEpsCode2).
We prove the intermediate claim HxNotUof: x ∉ U_of n.
rewrite the current goal using HUofEq (from left to right).
An exact proof term for the current goal is HxNotU.
We prove the intermediate claim HxBn: x ∈ (B_of n).
We prove the intermediate claim HBdef: B_of n = X ∖ (U_of n).
Use reflexivity.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is (setminusI X (U_of n) x HxX HxNotUof).
We prove the intermediate claim Hunprop: ∀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 (closed_interval 0 (eps_ (ordsucc n))) (closed_interval_topology 0 (eps_ (ordsucc n))) (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)) (Hu_of_prop n HnO)).
We prove the intermediate claim HuxEq: apply_fun (u_of n) x = eps_ (ordsucc n).
An exact proof term for the current goal is (Hunprop x HxBn).
We prove the intermediate claim HepsnR: 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) (omega_ordsucc n HnO))).
We prove the intermediate claim Hepsnpos: Rlt 0 (eps_ (ordsucc n)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc n)) real_0 HepsnR (SNo_eps_pos (ordsucc n) (omega_ordsucc n HnO))).
Set eps2 to be the term eps_ (ordsucc (ordsucc n)).
We prove the intermediate claim Heps2O: ordsucc (ordsucc n) ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (ordsucc n) (omega_ordsucc n HnO)).
We prove the intermediate claim Heps2R: eps2 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eps2 (SNo_eps_SNoS_omega (ordsucc (ordsucc n)) Heps2O)).
We prove the intermediate claim Heps2pos: Rlt 0 eps2.
An exact proof term for the current goal is (RltI 0 eps2 real_0 Heps2R (SNo_eps_pos (ordsucc (ordsucc n)) Heps2O)).
We prove the intermediate claim Heps2ltS: eps2 < eps_ (ordsucc n).
We prove the intermediate claim Hnin: ordsucc n ∈ ordsucc (ordsucc n).
An exact proof term for the current goal is (ordsuccI2 (ordsucc n)).
An exact proof term for the current goal is (SNo_eps_decr (ordsucc (ordsucc n)) Heps2O (ordsucc n) Hnin).
We prove the intermediate claim Heps2lt: Rlt eps2 (eps_ (ordsucc n)).
An exact proof term for the current goal is (RltI eps2 (eps_ (ordsucc n)) Heps2R HepsnR Heps2ltS).
Apply (Hf_unif eps2 Heps2R Heps2pos) to the current goal.
Let N0 be given.
Assume HN0pair: N0 ∈ ω ∧ ∀m0 : set, m0 ∈ ω → N0 ⊆ m0 → ∀x0 : set, x0 ∈ X → Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m0) x0,apply_fun f x0)) eps2.
Set m0 to be the term add_nat N0 (ordsucc n).
We prove the intermediate claim HN0O: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (∀m1 : set, m1 ∈ ω → N0 ⊆ m1 → ∀x0 : set, x0 ∈ X → Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m1) x0,apply_fun f x0)) eps2) HN0pair).
We prove the intermediate claim HN0Nat: nat_p N0.
An exact proof term for the current goal is (omega_nat_p N0 HN0O).
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 Hm0Nat: nat_p m0.
An exact proof term for the current goal is (add_nat_p N0 HN0Nat (ordsucc n) (nat_ordsucc n HnNat)).
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 HN0sub: N0 ⊆ m0.
An exact proof term for the current goal is (add_nat_Subq_R' N0 HN0Nat (ordsucc n) (nat_ordsucc n HnNat)).
We prove the intermediate claim Hclose: Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m0) x,apply_fun f x)) eps2.
An exact proof term for the current goal is (andER (N0 ∈ ω) (∀m1 : set, m1 ∈ ω → N0 ⊆ m1 → ∀x0 : set, x0 ∈ X → Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m1) x0,apply_fun f x0)) eps2) HN0pair m0 Hm0O HN0sub x HxX).
We prove the intermediate claim Hclose0: Rlt (apply_fun R_bounded_metric (apply_fun (apply_fun fn m0) x,0)) eps2.
We prove the intermediate claim HpairEq: (apply_fun (apply_fun fn m0) x,0) = (apply_fun (apply_fun fn m0) x,apply_fun f x).
Apply tuple_2_ext to the current goal.
Use reflexivity.
rewrite the current goal using Hfx0 (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.
Set sx to be the term apply_fun (apply_fun fn m0) x.
We prove the intermediate claim HsxR: sx ∈ R.
We prove the intermediate claim Hfm0: apply_fun fn m0 ∈ function_space X R.
An exact proof term for the current goal is (HfnFS 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 Hm0sub: ordsucc n ⊆ m0.
We prove the intermediate claim Hcom: add_nat N0 (ordsucc n) = add_nat (ordsucc n) N0.
An exact proof term for the current goal is (add_nat_com N0 HN0Nat (ordsucc n) (nat_ordsucc n HnNat)).
rewrite the current goal using Hcom (from left to right).
An exact proof term for the current goal is (add_nat_Subq_R' (ordsucc n) (nat_ordsucc n HnNat) N0 HN0Nat).
We prove the intermediate claim Hsx_ge: Rle (eps_ (ordsucc n)) sx.
We prove the intermediate claim HState_step_at_x: ∀t : set, nat_p t → apply_fun (State (ordsucc t)) x = add_SNo (apply_fun (State t) x) (apply_fun (u_of t) x).
Let t be given.
Assume HtNat: nat_p t.
We prove the intermediate claim HtO: t ∈ ω.
An exact proof term for the current goal is (nat_p_omega t HtNat).
We prove the intermediate claim HtSuccO: ordsucc t ∈ ω.
An exact proof term for the current goal is (omega_ordsucc t HtO).
We prove the intermediate claim HbState: State (ordsucc t) = Step t (State t).
An exact proof term for the current goal is (nat_primrec_S Base Step t HtNat).
rewrite the current goal using HbState (from left to right).
We prove the intermediate claim HstepDef: Step t (State t) = compose_fun X (pair_map X (State t) (u_of t)) add_fun_R.
Use reflexivity.
rewrite the current goal using HstepDef (from left to right).
We prove the intermediate claim HftFS: apply_fun fn t ∈ function_space X R.
An exact proof term for the current goal is (HfnFS 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 HftFS).
We prove the intermediate claim HaEq: apply_fun fn t = State t.
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ State n0) t HtO).
We prove the intermediate claim HStxR: apply_fun (State t) x ∈ R.
rewrite the current goal using HaEq (from right to left) at position 1.
An exact proof term for the current goal is (Hft_on x HxX).
We prove the intermediate claim HucR: continuous_map X Tx R R_standard_topology (u_of t).
An exact proof term for the current goal is (Hu_contR t HtO).
We prove the intermediate claim Hut_on: function_on (u_of t) X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (u_of t) HucR).
We prove the intermediate claim HuxR: apply_fun (u_of t) x ∈ R.
An exact proof term for the current goal is (Hut_on x HxX).
An exact proof term for the current goal is (add_of_pair_map_apply X (State t) (u_of t) x HxX HStxR HuxR).
We prove the intermediate claim Hu_nonneg_at_x: ∀t : set, nat_p t → Rle 0 (apply_fun (u_of t) x).
Let t be given.
Assume HtNat: nat_p t.
We prove the intermediate claim HtO: t ∈ ω.
An exact proof term for the current goal is (nat_p_omega t HtNat).
We prove the intermediate claim HtSuccO: ordsucc t ∈ ω.
An exact proof term for the current goal is (omega_ordsucc t HtO).
We prove the intermediate claim Hu12: (continuous_map X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of t) x0 = 0)).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t) ∧ (∀x0 : set, x0 ∈ A → apply_fun (u_of t) x0 = 0)) (∀x0 : set, x0 ∈ (B_of t) → apply_fun (u_of t) x0 = eps_ (ordsucc t)) (Hu_of_prop t HtO)).
We prove the intermediate claim HuI: continuous_map X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t)) (∀x0 : set, x0 ∈ A → apply_fun (u_of t) x0 = 0) Hu12).
We prove the intermediate claim HuOn: function_on (u_of t) X (closed_interval 0 (eps_ (ordsucc t))).
An exact proof term for the current goal is (continuous_map_function_on X Tx (closed_interval 0 (eps_ (ordsucc t))) (closed_interval_topology 0 (eps_ (ordsucc t))) (u_of t) HuI).
We prove the intermediate claim HuxI: apply_fun (u_of t) x ∈ closed_interval 0 (eps_ (ordsucc t)).
An exact proof term for the current goal is (HuOn x HxX).
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) HtSuccO)).
We prove the intermediate claim Hbds: Rle 0 (apply_fun (u_of t) x) ∧ Rle (apply_fun (u_of t) x) (eps_ (ordsucc t)).
An exact proof term for the current goal is (closed_interval_bounds 0 (eps_ (ordsucc t)) (apply_fun (u_of t) x) real_0 HepsR HuxI).
An exact proof term for the current goal is (andEL (Rle 0 (apply_fun (u_of t) x)) (Rle (apply_fun (u_of t) x) (eps_ (ordsucc t))) Hbds).
We prove the intermediate claim HState_step_mono: ∀t : set, nat_p t → Rle (apply_fun (State t) x) (apply_fun (State (ordsucc t)) x).
Let t be given.
Assume HtNat: nat_p t.
We prove the intermediate claim HtO: t ∈ ω.
An exact proof term for the current goal is (nat_p_omega t HtNat).
We prove the intermediate claim HStEq: apply_fun (State (ordsucc t)) x = add_SNo (apply_fun (State t) x) (apply_fun (u_of t) x).
An exact proof term for the current goal is (HState_step_at_x t HtNat).
rewrite the current goal using HStEq (from left to right).
We prove the intermediate claim H0leu: Rle 0 (apply_fun (u_of t) x).
An exact proof term for the current goal is (Hu_nonneg_at_x t HtNat).
We prove the intermediate claim HuR: apply_fun (u_of t) x ∈ R.
An exact proof term for the current goal is (RleE_right 0 (apply_fun (u_of t) x) H0leu).
We prove the intermediate claim HftFS: apply_fun fn t ∈ function_space X R.
An exact proof term for the current goal is (HfnFS 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 HftFS).
We prove the intermediate claim HaEq: apply_fun fn t = State t.
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ State n0) t HtO).
We prove the intermediate claim HStR: apply_fun (State t) x ∈ R.
rewrite the current goal using HaEq (from right to left) at position 1.
An exact proof term for the current goal is (Hft_on x HxX).
We prove the intermediate claim Hle': Rle (add_SNo (apply_fun (State t) x) 0) (add_SNo (apply_fun (State t) x) (apply_fun (u_of t) x)).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun (State t) x) 0 (apply_fun (u_of t) x) HStR real_0 HuR H0leu).
rewrite the current goal using (add_SNo_0R (apply_fun (State t) x) (real_SNo (apply_fun (State t) x) HStR)) (from right to left) at position 1.
An exact proof term for the current goal is Hle'.
We prove the intermediate claim HState_nonneg_at_x: ∀t : set, nat_p t → Rle 0 (apply_fun (State t) x).
Let t be given.
Assume HtNat: nat_p t.
We prove the intermediate claim Hbase0: Rle 0 (apply_fun (State 0) x).
We prove the intermediate claim HSt0: State 0 = Base.
An exact proof term for the current goal is (nat_primrec_0 Base Step).
rewrite the current goal using HSt0 (from left to right).
rewrite the current goal using (const_fun_apply X 0 x HxX) (from left to right).
An exact proof term for the current goal is (Rle_refl 0 real_0).
We prove the intermediate claim Hstep0: ∀k : set, nat_p k → Rle 0 (apply_fun (State k) x) → Rle 0 (apply_fun (State (ordsucc k)) x).
Let k be given.
Assume HkNat: nat_p k.
Assume IH: Rle 0 (apply_fun (State k) x).
We prove the intermediate claim Hmono: Rle (apply_fun (State k) x) (apply_fun (State (ordsucc k)) x).
An exact proof term for the current goal is (HState_step_mono k HkNat).
An exact proof term for the current goal is (Rle_tra 0 (apply_fun (State k) x) (apply_fun (State (ordsucc k)) x) IH Hmono).
An exact proof term for the current goal is (nat_ind (λk : set ⇒ Rle 0 (apply_fun (State k) x)) Hbase0 Hstep0 t HtNat).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is HnNat.
We prove the intermediate claim H0leStn: Rle 0 (apply_fun (State n) x).
An exact proof term for the current goal is (HState_nonneg_at_x n HnNat).
We prove the intermediate claim HStnR: apply_fun (State n) x ∈ R.
We prove the intermediate claim HftFS: apply_fun fn n ∈ function_space X R.
An exact proof term for the current goal is (HfnFS n HnO).
We prove the intermediate claim Hft_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 HftFS).
We prove the intermediate claim HaEq: apply_fun fn n = State n.
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ State n0) n HnO).
rewrite the current goal using HaEq (from right to left) at position 1.
An exact proof term for the current goal is (Hft_on x HxX).
We prove the intermediate claim HStSuccEq: apply_fun (State (ordsucc n)) x = add_SNo (apply_fun (State n) x) (apply_fun (u_of n) x).
An exact proof term for the current goal is (HState_step_at_x n HnNat).
We prove the intermediate claim Hbase_lb: Rle (eps_ (ordsucc n)) (apply_fun (State (ordsucc n)) x).
rewrite the current goal using HStSuccEq (from left to right).
rewrite the current goal using HuxEq (from left to right).
We prove the intermediate claim Hle': Rle (add_SNo (eps_ (ordsucc n)) 0) (add_SNo (eps_ (ordsucc n)) (apply_fun (State n) x)).
An exact proof term for the current goal is (Rle_add_SNo_2 (eps_ (ordsucc n)) 0 (apply_fun (State n) x) HepsnR real_0 HStnR H0leStn).
rewrite the current goal using (add_SNo_0R (eps_ (ordsucc n)) (real_SNo (eps_ (ordsucc n)) HepsnR)) (from right to left) at position 1.
We prove the intermediate claim Hcomm: add_SNo (eps_ (ordsucc n)) (apply_fun (State n) x) = add_SNo (apply_fun (State n) x) (eps_ (ordsucc n)).
An exact proof term for the current goal is (add_SNo_com (eps_ (ordsucc n)) (apply_fun (State n) x) (real_SNo (eps_ (ordsucc n)) HepsnR) (real_SNo (apply_fun (State n) x) HStnR)).
rewrite the current goal using Hcomm (from right to left).
An exact proof term for the current goal is Hle'.
We prove the intermediate claim HbaseNat: nat_p (ordsucc n).
An exact proof term for the current goal is (nat_ordsucc n HnNat).
We prove the intermediate claim HN0Nat: nat_p N0.
An exact proof term for the current goal is HN0Nat.
We prove the intermediate claim Hmono_to_m0: Rle (apply_fun (State (ordsucc n)) x) (apply_fun (State m0) x).
We prove the intermediate claim Hmono_aux: ∀k : set, nat_p k → Rle (apply_fun (State (ordsucc n)) x) (apply_fun (State (add_nat k (ordsucc n))) x).
Let k be given.
Assume HkNat: nat_p k.
We prove the intermediate claim HStbaseR: apply_fun (State (ordsucc n)) x ∈ R.
rewrite the current goal using HStSuccEq (from left to right).
rewrite the current goal using HuxEq (from left to right).
An exact proof term for the current goal is (real_add_SNo (apply_fun (State n) x) HStnR (eps_ (ordsucc n)) HepsnR).
We prove the intermediate claim Hbase0mono: Rle (apply_fun (State (ordsucc n)) x) (apply_fun (State (add_nat 0 (ordsucc n))) x).
rewrite the current goal using (add_nat_0L (ordsucc n) HbaseNat) (from left to right).
An exact proof term for the current goal is (Rle_refl (apply_fun (State (ordsucc n)) x) HStbaseR).
We prove the intermediate claim Hstepmono: ∀kk : set, nat_p kk → Rle (apply_fun (State (ordsucc n)) x) (apply_fun (State (add_nat kk (ordsucc n))) x) → Rle (apply_fun (State (ordsucc n)) x) (apply_fun (State (add_nat (ordsucc kk) (ordsucc n))) x).
Let kk be given.
Assume HkkNat: nat_p kk.
Assume IH: Rle (apply_fun (State (ordsucc n)) x) (apply_fun (State (add_nat kk (ordsucc n))) x).
We prove the intermediate claim HsuccEq: add_nat (ordsucc kk) (ordsucc n) = ordsucc (add_nat kk (ordsucc n)).
An exact proof term for the current goal is (add_nat_SL kk HkkNat (ordsucc n) HbaseNat).
rewrite the current goal using HsuccEq (from left to right).
We prove the intermediate claim HkbaseNat: nat_p (add_nat kk (ordsucc n)).
An exact proof term for the current goal is (add_nat_p kk HkkNat (ordsucc n) HbaseNat).
We prove the intermediate claim Hstep: Rle (apply_fun (State (add_nat kk (ordsucc n))) x) (apply_fun (State (ordsucc (add_nat kk (ordsucc n)))) x).
An exact proof term for the current goal is (HState_step_mono (add_nat kk (ordsucc n)) HkbaseNat).
An exact proof term for the current goal is (Rle_tra (apply_fun (State (ordsucc n)) x) (apply_fun (State (add_nat kk (ordsucc n))) x) (apply_fun (State (ordsucc (add_nat kk (ordsucc n)))) x) IH Hstep).
An exact proof term for the current goal is (nat_ind (λkk : set ⇒ Rle (apply_fun (State (ordsucc n)) x) (apply_fun (State (add_nat kk (ordsucc n))) x)) Hbase0mono Hstepmono k HkNat).
We prove the intermediate claim Hm0Def: m0 = add_nat N0 (ordsucc n).
Use reflexivity.
rewrite the current goal using Hm0Def (from left to right).
An exact proof term for the current goal is (Hmono_aux N0 HN0Nat).
We prove the intermediate claim Hlb_m0: Rle (eps_ (ordsucc n)) (apply_fun (State m0) x).
An exact proof term for the current goal is (Rle_tra (eps_ (ordsucc n)) (apply_fun (State (ordsucc n)) x) (apply_fun (State m0) x) Hbase_lb Hmono_to_m0).
We prove the intermediate claim HaEq0: apply_fun fn m0 = State m0.
An exact proof term for the current goal is (apply_fun_graph ω (λn0 : set ⇒ State n0) m0 Hm0O).
We prove the intermediate claim HsxEq: sx = apply_fun (State m0) x.
rewrite the current goal using HaEq0 (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HsxEq (from left to right).
An exact proof term for the current goal is Hlb_m0.
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 Heps2lt1S: eps2 < 1.
We prove the intermediate claim H0in: 0 ∈ ordsucc (ordsucc n).
An exact proof term for the current goal is (nat_0_in_ordsucc (ordsucc n) (nat_ordsucc n HnNat)).
We prove the intermediate claim Heps2ltE0: eps_ (ordsucc (ordsucc n)) < eps_ 0.
An exact proof term for the current goal is (SNo_eps_decr (ordsucc (ordsucc n)) Heps2O 0 H0in).
rewrite the current goal using (eps_0_1) (from right to left).
An exact proof term for the current goal is Heps2ltE0.
We prove the intermediate claim Habslt: abs_SNo (add_SNo sx (minus_SNo 0)) < eps2.
We prove the intermediate claim Hclose0d: Rlt (R_bounded_distance sx 0) eps2.
rewrite the current goal using (R_bounded_metric_apply_early sx 0 HsxR real_0) (from right to left).
An exact proof term for the current goal is Hclose0.
An exact proof term for the current goal is (R_bounded_distance_lt_lt1_imp_abs_lt sx 0 eps2 HsxR real_0 Heps2R (RltI eps2 1 Heps2R real_1 Heps2lt1S) Hclose0d).
We prove the intermediate claim HabsEq0: add_SNo sx (minus_SNo 0) = sx.
rewrite the current goal using (minus_SNo_0) (from left to right) at position 1.
rewrite the current goal using (add_SNo_0R sx (real_SNo sx HsxR)) (from left to right).
Use reflexivity.
We prove the intermediate claim Habslt2: abs_SNo sx < eps2.
rewrite the current goal using HabsEq0 (from right to left) at position 1.
An exact proof term for the current goal is Habslt.
We prove the intermediate claim Hcontra: ¬ (Rlt (eps_ (ordsucc n)) eps2).
An exact proof term for the current goal is (not_Rlt_sym eps2 (eps_ (ordsucc n)) Heps2lt).
We prove the intermediate claim HabsR: abs_SNo sx ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R sx HsxR).
We prove the intermediate claim HsxS: SNo sx.
An exact proof term for the current goal is (real_SNo sx HsxR).
We prove the intermediate claim HsxleabsS: sx ≤ abs_SNo sx.
An exact proof term for the current goal is (abs_SNo_upper_bound sx HsxS).
We prove the intermediate claim Hsxleabs: Rle sx (abs_SNo sx).
An exact proof term for the current goal is (Rle_of_SNoLe sx (abs_SNo sx) HsxR HabsR HsxleabsS).
We prove the intermediate claim Hepsleabs: Rle (eps_ (ordsucc n)) (abs_SNo sx).
An exact proof term for the current goal is (Rle_tra (eps_ (ordsucc n)) sx (abs_SNo sx) Hsx_ge Hsxleabs).
We prove the intermediate claim HabsltR: Rlt (abs_SNo sx) eps2.
An exact proof term for the current goal is (RltI (abs_SNo sx) eps2 HabsR Heps2R Habslt2).
We prove the intermediate claim Hepslt: Rlt (eps_ (ordsucc n)) eps2.
An exact proof term for the current goal is (Rle_Rlt_tra (eps_ (ordsucc n)) (abs_SNo sx) eps2 Hepsleabs HabsltR).
An exact proof term for the current goal is (Hcontra Hepslt).
Assume Hexf: ∃f : set, continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → x ∉ A → ¬ (apply_fun f x = 0)).
Apply Hexf to the current goal.
Let f be given.
Assume Hfpack.
Apply Hfpack to the current goal.
Assume Hcore: continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0).
Assume HvanOut: ∀x : set, x ∈ X → x ∉ A → ¬ (apply_fun f x = 0).
Apply Hcore to the current goal.
Assume Hcont: continuous_map X Tx R R_standard_topology f.
Assume HvanA: ∀x : set, x ∈ A → apply_fun f x = 0.
We will prove Gdelta_in X Tx A.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (continuous_map_topology_dom X Tx R R_standard_topology f Hcont).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).
We will prove ∃Fam : set, countable_set Fam ∧ (∀U ∈ Fam, open_in X Tx U) ∧ intersection_over_family X Fam = A.
Set Fam to be the term {preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n))|n ∈ ω}.
We use Fam to witness the existential quantifier.
We will prove countable_set Fam ∧ (∀U ∈ Fam, open_in X Tx U) ∧ intersection_over_family X Fam = A.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim Homega_countable: countable ω.
An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).
An exact proof term for the current goal is (countable_image ω Homega_countable (λn : set ⇒ preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n)))).
Let U be given.
Assume HU: U ∈ Fam.
We will prove open_in X Tx U.
We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ U = preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n)).
An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n0))) U HU).
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 ∈ ω) (U = preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n))) Hnpair).
We prove the intermediate claim HUeq: U = preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n)).
An exact proof term for the current goal is (andER (n ∈ ω) (U = preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n))) Hnpair).
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HepsInS: eps_ n ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega n Hnomega).
We prove the intermediate claim HepsR: eps_ n ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ n) HepsInS).
We prove the intermediate claim HepsposS: 0 < (eps_ n).
An exact proof term for the current goal is (SNo_eps_pos n Hnomega).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ n).
An exact proof term for the current goal is (RltI 0 (eps_ n) real_0 HepsR HepsposS).
We prove the intermediate claim HballOpenR: open_ball R R_bounded_metric 0 (eps_ n) ∈ R_standard_topology.
An exact proof term for the current goal is (open_ball_R_bounded_metric_in_R_standard_topology 0 (eps_ n) real_0 HepsR Hepspos).
We will prove open_in X Tx (preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n))).
We will prove topology_on X Tx ∧ preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n)) ∈ Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is (andER ((topology_on X Tx ∧ topology_on R R_standard_topology) ∧ function_on f X R) (∀V : set, V ∈ R_standard_topology → preimage_of X f V ∈ Tx) Hcont (open_ball R R_bounded_metric 0 (eps_ n)) HballOpenR).
We prove the intermediate claim HIntDef: intersection_over_family X Fam = {x0 ∈ X|∀U0 : set, U0 ∈ Fam → x0 ∈ U0}.
Use reflexivity.
rewrite the current goal using HIntDef (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume HxInt: x ∈ {x0 ∈ X|∀U0 : set, U0 ∈ Fam → x0 ∈ U0}.
We will prove x ∈ A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam → x0 ∈ U0) x HxInt).
We prove the intermediate claim HallU: ∀U0 : set, U0 ∈ Fam → x ∈ U0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam → x0 ∈ U0) x HxInt).
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
An exact proof term for the current goal is HxA.
Assume HxNotA: ¬ (x ∈ A).
Apply FalseE to the current goal.
We prove the intermediate claim HfXY: function_on f X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology f Hcont).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (HfXY x HxX).
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.
Set d0 to be the term apply_fun R_bounded_metric (apply_fun f x,0).
We prove the intermediate claim Hd0pos: Rlt 0 d0.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hneq0: ¬ (apply_fun f x = 0).
An exact proof term for the current goal is (HvanOut x HxX HxNotA).
An exact proof term for the current goal is (metric_on_pos_of_neq R R_bounded_metric (apply_fun f x) 0 HmR HfxR H0R Hneq0).
We prove the intermediate claim Hd0R: d0 ∈ R.
We prove the intermediate claim HdFun: function_on R_bounded_metric (setprod R R) R.
An exact proof term for the current goal is (metric_on_function_on R R_bounded_metric HmR).
We prove the intermediate claim Hpair: (apply_fun f x,0) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (apply_fun f x) 0 HfxR real_0).
An exact proof term for the current goal is (HdFun (apply_fun f x,0) Hpair).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < d0.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid d0 Hd0R Hd0pos).
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 < d0) HNpair).
We prove the intermediate claim HepsLt: eps_ N < d0.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < d0) HNpair).
Set UN to be the term preimage_of X f (open_ball R R_bounded_metric 0 (eps_ N)).
We prove the intermediate claim HUNinFam: UN ∈ Fam.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n0))) N HNomega).
We prove the intermediate claim HxUN: x ∈ UN.
An exact proof term for the current goal is (HallU UN HUNinFam).
We prove the intermediate claim HpreUNDef: UN = {x0 ∈ X|apply_fun f x0 ∈ open_ball R R_bounded_metric 0 (eps_ N)}.
Use reflexivity.
We prove the intermediate claim HxUN': x ∈ {x0 ∈ X|apply_fun f x0 ∈ open_ball R R_bounded_metric 0 (eps_ N)}.
rewrite the current goal using HpreUNDef (from right to left).
An exact proof term for the current goal is HxUN.
We prove the intermediate claim HfxInBall: apply_fun f x ∈ open_ball R R_bounded_metric 0 (eps_ N).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ open_ball R R_bounded_metric 0 (eps_ N)) x HxUN').
We prove the intermediate claim Hlt0: Rlt (apply_fun R_bounded_metric (0,apply_fun f x)) (eps_ N).
An exact proof term for the current goal is (open_ballE2 R R_bounded_metric 0 (eps_ N) (apply_fun f x) HfxInBall).
We prove the intermediate claim Hsym: apply_fun R_bounded_metric (0,apply_fun f x) = apply_fun R_bounded_metric (apply_fun f x,0).
An exact proof term for the current goal is (metric_on_symmetric R R_bounded_metric 0 (apply_fun f x) HmR real_0 HfxR).
We prove the intermediate claim Hlt: Rlt d0 (eps_ N).
rewrite the current goal using Hsym (from right to left).
An exact proof term for the current goal is Hlt0.
We prove the intermediate claim HepsR: 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 HepsLtRlt: Rlt (eps_ N) d0.
An exact proof term for the current goal is (RltI (eps_ N) d0 HepsR Hd0R HepsLt).
We prove the intermediate claim Hbad: Rlt (eps_ N) (eps_ N).
An exact proof term for the current goal is (Rlt_tra (eps_ N) d0 (eps_ N) HepsLtRlt Hlt).
An exact proof term for the current goal is ((not_Rlt_refl (eps_ N) HepsR) Hbad).
Let x be given.
Assume HxA: x ∈ A.
We will prove x ∈ {x0 ∈ X|∀U0 : set, U0 ∈ Fam → x0 ∈ U0}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
Apply (SepI X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam → x0 ∈ U0) x HxX) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Fam.
We will prove x ∈ U0.
We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ U0 = preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n)).
An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n0))) U0 HU0).
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 ∈ ω) (U0 = preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n))) Hnpair).
We prove the intermediate claim HU0eq: U0 = preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n)).
An exact proof term for the current goal is (andER (n ∈ ω) (U0 = preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n))) Hnpair).
rewrite the current goal using HU0eq (from left to right).
We prove the intermediate claim HfXY: function_on f X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology f Hcont).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (HfXY x HxX).
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.
We prove the intermediate claim HepsR: 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 HepsposS: 0 < (eps_ n).
An exact proof term for the current goal is (SNo_eps_pos n Hnomega).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ n).
An exact proof term for the current goal is (RltI 0 (eps_ n) real_0 HepsR HepsposS).
We prove the intermediate claim H0InBall: 0 ∈ open_ball R R_bounded_metric 0 (eps_ n).
An exact proof term for the current goal is (center_in_open_ball R R_bounded_metric 0 (eps_ n) HmR real_0 Hepspos).
We prove the intermediate claim Hfx0: apply_fun f x = 0.
An exact proof term for the current goal is (HvanA x HxA).
We prove the intermediate claim HfxInBall: apply_fun f x ∈ open_ball R R_bounded_metric 0 (eps_ n).
rewrite the current goal using Hfx0 (from left to right).
An exact proof term for the current goal is H0InBall.
We prove the intermediate claim HpreDef: preimage_of X f (open_ball R R_bounded_metric 0 (eps_ n)) = {x0 ∈ X|apply_fun f x0 ∈ open_ball R R_bounded_metric 0 (eps_ n)}.
Use reflexivity.
rewrite the current goal using HpreDef (from left to right).
Apply (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ open_ball R R_bounded_metric 0 (eps_ n)) x HxX) to the current goal.
An exact proof term for the current goal is HfxInBall.
∎