Let X and Tx be given.
Assume Hreg: regular_space X Tx.
Assume Hbasis: sigma_locally_finite_basis X Tx.
We will prove metrizable X Tx.
We prove the intermediate claim H40: normal_space X Tx ∧ (∀C : set, closed_in X Tx C → Gdelta_simple X Tx C).
An exact proof term for the current goal is (lemma40_1_regular_sigma_basis_implies_normal_and_closed_Gdelta X Tx Hreg Hbasis).
We prove the intermediate claim Hnorm: normal_space X Tx.
An exact proof term for the current goal is (andEL (normal_space X Tx) (∀C : set, closed_in X Tx C → Gdelta_simple X Tx C) H40).
We prove the intermediate claim HclosedG: ∀C : set, closed_in X Tx C → Gdelta_simple X Tx C.
An exact proof term for the current goal is (andER (normal_space X Tx) (∀C : set, closed_in X Tx C → Gdelta_simple X Tx C) H40).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (regular_space_topology_on X Tx Hreg).
We prove the intermediate claim HT1: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
We prove the intermediate claim HexFams: ∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀F0 : set, F0 ∈ Fams → locally_finite_family X Tx F0) ∧ basis_generates X (⋃ Fams) Tx ∧ ∀b : set, b ∈ ⋃ Fams → b ∈ Tx.
An exact proof term for the current goal is (sigma_locally_finite_basis_data X Tx Hbasis).
Apply HexFams to the current goal.
Let Fams be given.
Assume HFamsPack: countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀F0 : set, F0 ∈ Fams → locally_finite_family X Tx F0) ∧ basis_generates X (⋃ Fams) Tx ∧ ∀b : set, b ∈ ⋃ Fams → b ∈ Tx.
Apply (and5E (countable_set Fams) (Fams ⊆ 𝒫 (𝒫 X)) (∀F0 : set, F0 ∈ Fams → locally_finite_family X Tx F0) (basis_generates X (⋃ Fams) Tx) (∀b : set, b ∈ ⋃ Fams → b ∈ Tx) HFamsPack) to the current goal.
Assume _HFamsCount.
Assume _HFamsSubPow.
Assume _HLFams.
Assume HBgen: basis_generates X (⋃ Fams) Tx.
Assume HBopen: ∀b : set, b ∈ ⋃ Fams → b ∈ Tx.
Set B to be the term ⋃ Fams.
We prove the intermediate claim Href: basis_refines X B Tx.
An exact proof term for the current goal is (basis_generates_imp_basis_refines X Tx B HBgen).
Apply _HFamsCount to the current goal.
Let idx of type set → set be given.
Assume Hidxinj: inj Fams ω idx.
We prove the intermediate claim Hidx_to_omega: ∀F0 ∈ Fams, idx F0 ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ Fams, idx u ∈ ω) (∀u v ∈ Fams, idx u = idx v → u = v) Hidxinj).
We prove the intermediate claim Hidx_inj: ∀F0 F1 ∈ Fams, idx F0 = idx F1 → F0 = F1.
An exact proof term for the current goal is (andER (∀u ∈ Fams, idx u ∈ ω) (∀u v ∈ Fams, idx u = idx v → u = v) Hidxinj).
Set J to be the term {p ∈ setprod ω B|∃F0 : set, F0 ∈ Fams ∧ idx F0 = (p 0) ∧ (p 1) ∈ F0}.
Set bump0 to be the term (λb : set ⇒ Eps_i (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x)))).
Set bump to be the term (λb : set ⇒ graph X (λx : set ⇒ apply_fun (bump0 b) x)).
Set bump_scaled to be the term (λn b : set ⇒ compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n)))).
Set F to be the term graph J (λp : set ⇒ bump_scaled (p 0) (p 1)).
We prove the intermediate claim Hsep: separating_family_of_functions X Tx F J.
We will prove separating_family_of_functions X Tx F J.
We prove the intermediate claim HdefSep: separating_family_of_functions X Tx F J = (topology_on X Tx ∧ total_function_on F J (function_space X R) ∧ (∀j : set, j ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j)) ∧ (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x0) ∧ ∀x : set, x ∈ X ∖ U0 → apply_fun (apply_fun F j) x = 0)).
Use reflexivity.
rewrite the current goal using HdefSep (from left to right).
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 HTx.
We prove the intermediate claim HFdef: F = graph J (λp : set ⇒ bump_scaled (p 0) (p 1)).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
Apply (total_function_on_graph J (function_space X R) (λp : set ⇒ bump_scaled (p 0) (p 1))) to the current goal.
Let p be given.
Assume HpJ: p ∈ J.
We will prove bump_scaled (p 0) (p 1) ∈ function_space X R.
Set n to be the term p 0.
Set b to be the term p 1.
We prove the intermediate claim HidxInfo: ∃F0 : set, F0 ∈ Fams ∧ idx F0 = n ∧ b ∈ F0.
An exact proof term for the current goal is (SepE2 (setprod ω B) (λq : set ⇒ ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (q 0) ∧ (q 1) ∈ F0) p HpJ).
We prove the intermediate claim HbB: b ∈ B.
We prove the intermediate claim Hp0: n ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ B) p (SepE1 (setprod ω B) (λq : set ⇒ ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (q 0) ∧ (q 1) ∈ F0) p HpJ)).
An exact proof term for the current goal is (ap1_Sigma ω (λ_ : set ⇒ B) p (SepE1 (setprod ω B) (λq : set ⇒ ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (q 0) ∧ (q 1) ∈ F0) p HpJ)).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBopen b HbB).
We prove the intermediate claim Hexb0: ∃f0 : set, continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x)).
An exact proof term for the current goal is (open_set_has_positive_support_function_unit_interval X Tx b Hnorm HclosedG HbTx).
Set P to be the term (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x))).
We prove the intermediate claim HPb: P (bump0 b).
An exact proof term for the current goal is (Eps_i_ex P Hexb0).
We prove the intermediate claim Hbump_FS: bump b ∈ function_space X R.
We prove the intermediate claim HbumpDef: bump b = graph X (λx : set ⇒ apply_fun (bump0 b) x).
Use reflexivity.
rewrite the current goal using HbumpDef (from left to right).
Apply (graph_in_function_space X R (λx : set ⇒ apply_fun (bump0 b) x)) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun (bump0 b) x ∈ R.
We prove the intermediate claim Hb0c0: continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HPb).
We prove the intermediate claim Hb0cont: continuous_map X Tx unit_interval unit_interval_topology (bump0 b).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0c0).
We prove the intermediate claim Hb0fun: function_on (bump0 b) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (bump0 b) Hb0cont).
We prove the intermediate claim HxI: apply_fun (bump0 b) x ∈ unit_interval.
An exact proof term for the current goal is (Hb0fun x HxX).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (bump0 b) x) HxI).
We prove the intermediate claim Hbump_on: function_on (bump b) X R.
An exact proof term for the current goal is (function_on_of_function_space (bump b) X R Hbump_FS).
We prove the intermediate claim Hmul_on: function_on (mul_const_fun (inv_nat (ordsucc n))) R R.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ B) p (SepE1 (setprod ω B) (λq : set ⇒ ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (q 0) ∧ (q 1) ∈ F0) p HpJ)).
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 HinvR: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) HsuccO).
We prove the intermediate claim HmulFS: mul_const_fun (inv_nat (ordsucc n)) ∈ function_space R R.
An exact proof term for the current goal is (mul_const_fun_in_function_space (inv_nat (ordsucc n)) HinvR).
An exact proof term for the current goal is (SepE2 (𝒫 (setprod R R)) (λh0 : set ⇒ function_on h0 R R) (mul_const_fun (inv_nat (ordsucc n))) HmulFS).
An exact proof term for the current goal is (compose_fun_in_function_space X R R (bump b) (mul_const_fun (inv_nat (ordsucc n))) Hbump_on Hmul_on).
Let j be given.
Assume HjJ: j ∈ J.
We will prove continuous_map X Tx R R_standard_topology (apply_fun F j).
We prove the intermediate claim HFdef: F = graph J (λp : set ⇒ bump_scaled (p 0) (p 1)).
Use reflexivity.
We prove the intermediate claim HappF: apply_fun F j = bump_scaled (j 0) (j 1).
rewrite the current goal using HFdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph J (λp : set ⇒ bump_scaled (p 0) (p 1)) j HjJ).
rewrite the current goal using HappF (from left to right).
Set n to be the term j 0.
Set b to be the term j 1.
We prove the intermediate claim Hjpack: ∃F0 : set, F0 ∈ Fams ∧ idx F0 = n ∧ b ∈ F0.
An exact proof term for the current goal is (SepE2 (setprod ω B) (λq : set ⇒ ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (q 0) ∧ (q 1) ∈ F0) j HjJ).
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (ap1_Sigma ω (λ_ : set ⇒ B) j (SepE1 (setprod ω B) (λq : set ⇒ ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (q 0) ∧ (q 1) ∈ F0) j HjJ)).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBopen b HbB).
We prove the intermediate claim Hexb0: ∃f0 : set, continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x)).
An exact proof term for the current goal is (open_set_has_positive_support_function_unit_interval X Tx b Hnorm HclosedG HbTx).
Set P to be the term (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x))).
We prove the intermediate claim HPb: P (bump0 b).
An exact proof term for the current goal is (Eps_i_ex P Hexb0).
We prove the intermediate claim Hb0AB: continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HPb).
We prove the intermediate claim Hb0cont: continuous_map X Tx unit_interval unit_interval_topology (bump0 b).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0AB).
We prove the intermediate claim Hb0zero: ∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0AB).
We prove the intermediate claim Hb0pos: ∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x).
An exact proof term for the current goal is (andER (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HPb).
We prove the intermediate claim Hbumpcont: continuous_map X Tx R R_standard_topology (bump b).
We prove the intermediate claim HTi: unit_interval_topology = subspace_topology R R_standard_topology unit_interval.
Use reflexivity.
We prove the intermediate claim Hb0contR: continuous_map X Tx R R_standard_topology (bump0 b).
An exact proof term for the current goal is (continuous_map_range_expand X Tx unit_interval unit_interval_topology R R_standard_topology (bump0 b) Hb0cont unit_interval_sub_R R_standard_topology_is_topology HTi).
We prove the intermediate claim Hb0fun: function_on (bump0 b) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (bump0 b) Hb0cont).
We prove the intermediate claim Hbdef: bump b = graph X (λx : set ⇒ apply_fun (bump0 b) x).
Use reflexivity.
We prove the intermediate claim Happb: ∀x : set, x ∈ X → apply_fun (bump b) x = apply_fun (bump0 b) x.
Let x be given.
Assume HxX: x ∈ X.
rewrite the current goal using Hbdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ apply_fun (bump0 b) x0) x HxX).
We will prove continuous_map X Tx R R_standard_topology (bump b).
We prove the intermediate claim Hcmdef: continuous_map X Tx R R_standard_topology (bump b) = (topology_on X Tx ∧ topology_on R R_standard_topology ∧ function_on (bump b) X R ∧ ∀V : set, V ∈ R_standard_topology → preimage_of X (bump b) V ∈ Tx).
Use reflexivity.
rewrite the current goal using Hcmdef (from left to right).
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 HTx.
An exact proof term for the current goal is R_standard_topology_is_topology.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun (bump b) x ∈ R.
rewrite the current goal using Hbdef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun (bump0 b) x0) x HxX) (from left to right).
We prove the intermediate claim HxI: apply_fun (bump0 b) x ∈ unit_interval.
An exact proof term for the current goal is (Hb0fun x HxX).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (bump0 b) x) HxI).
Let V be given.
Assume HV: V ∈ R_standard_topology.
We will prove preimage_of X (bump b) V ∈ Tx.
We prove the intermediate claim Hpre_eq: preimage_of X (bump b) V = preimage_of X (bump0 b) V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X (bump b) V.
We will prove x ∈ preimage_of X (bump0 b) V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun (bump b) x0 ∈ V) x Hx).
We prove the intermediate claim HxV: apply_fun (bump b) x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (bump b) x0 ∈ V) x Hx).
We prove the intermediate claim HxV0: apply_fun (bump0 b) x ∈ V.
We prove the intermediate claim Hbeta: (λx0 : set ⇒ apply_fun (bump0 b) x0) x = apply_fun (bump0 b) x.
Use reflexivity.
rewrite the current goal using Hbeta (from right to left).
We prove the intermediate claim Happg: apply_fun (bump b) x = (λx0 : set ⇒ apply_fun (bump0 b) x0) x.
rewrite the current goal using Hbdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ apply_fun (bump0 b) x0) x HxX).
rewrite the current goal using Happg (from right to left).
An exact proof term for the current goal is HxV.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun (bump0 b) x0 ∈ V) x HxX HxV0).
Let x be given.
Assume Hx: x ∈ preimage_of X (bump0 b) V.
We will prove x ∈ preimage_of X (bump b) V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun (bump0 b) x0 ∈ V) x Hx).
We prove the intermediate claim HxV: apply_fun (bump0 b) x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (bump0 b) x0 ∈ V) x Hx).
We prove the intermediate claim HxVb: apply_fun (bump b) x ∈ V.
We prove the intermediate claim Happg: apply_fun (bump b) x = (λx0 : set ⇒ apply_fun (bump0 b) x0) x.
rewrite the current goal using Hbdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ apply_fun (bump0 b) x0) x HxX).
rewrite the current goal using Happg (from left to right).
We prove the intermediate claim Hbeta: (λx0 : set ⇒ apply_fun (bump0 b) x0) x = apply_fun (bump0 b) x.
Use reflexivity.
rewrite the current goal using Hbeta (from left to right).
An exact proof term for the current goal is HxV.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun (bump b) x0 ∈ V) x HxX HxVb).
rewrite the current goal using Hpre_eq (from left to right).
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology (bump0 b) Hb0contR V HV).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ B) j (SepE1 (setprod ω B) (λq : set ⇒ ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (q 0) ∧ (q 1) ∈ F0) j HjJ)).
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 HinvR: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) HsuccO).
We prove the intermediate claim HinvPos: Rlt 0 (inv_nat (ordsucc n)).
We prove the intermediate claim HsuccNot0: ordsucc n ∉ {0}.
Assume H0: ordsucc n ∈ {0}.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) H0).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
We prove the intermediate claim HsuccIn: ordsucc n ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HsuccO.
An exact proof term for the current goal is HsuccNot0.
An exact proof term for the current goal is (inv_nat_pos (ordsucc n) HsuccIn).
We prove the intermediate claim Hinvlt: 0 < inv_nat (ordsucc n).
An exact proof term for the current goal is (RltE_lt 0 (inv_nat (ordsucc n)) HinvPos).
An exact proof term for the current goal is (scale_continuous_mul_const_pos X Tx (bump b) (inv_nat (ordsucc n)) HTx Hbumpcont HinvR Hinvlt).
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Let U0 be given.
Assume HU0: U0 ∈ Tx.
Assume Hx0U0: x0 ∈ U0.
We prove the intermediate claim HrefProp: ∀U1 ∈ Tx, ∀x1 ∈ U1, ∃b ∈ B, x1 ∈ b ∧ b ⊆ U1.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U1 ∈ Tx, ∀x1 ∈ U1, ∃b ∈ B, x1 ∈ b ∧ b ⊆ U1) Href).
We prove the intermediate claim Hexb: ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0.
An exact proof term for the current goal is (HrefProp U0 HU0 x0 Hx0U0).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack: b ∈ B ∧ (x0 ∈ b ∧ b ⊆ U0).
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x0 ∈ b ∧ b ⊆ U0) Hbpack).
We prove the intermediate claim Hbrest: x0 ∈ b ∧ b ⊆ U0.
An exact proof term for the current goal is (andER (b ∈ B) (x0 ∈ b ∧ b ⊆ U0) Hbpack).
We prove the intermediate claim Hx0b: x0 ∈ b.
An exact proof term for the current goal is (andEL (x0 ∈ b) (b ⊆ U0) Hbrest).
We prove the intermediate claim HbsubU0: b ⊆ U0.
An exact proof term for the current goal is (andER (x0 ∈ b) (b ⊆ U0) Hbrest).
We prove the intermediate claim HbU: b ∈ ⋃ Fams.
An exact proof term for the current goal is HbB.
We prove the intermediate claim HexF0: ∃F0 : set, F0 ∈ Fams ∧ b ∈ F0.
Apply (UnionE_impred Fams b HbU (∃F0 : set, F0 ∈ Fams ∧ b ∈ F0)) to the current goal.
Let F0 be given.
Assume HbF0: b ∈ F0.
Assume HF0: F0 ∈ Fams.
We use F0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HF0.
An exact proof term for the current goal is HbF0.
Apply HexF0 to the current goal.
Let F0 be given.
Assume HF0pair: F0 ∈ Fams ∧ b ∈ F0.
We prove the intermediate claim HF0F: F0 ∈ Fams.
An exact proof term for the current goal is (andEL (F0 ∈ Fams) (b ∈ F0) HF0pair).
We prove the intermediate claim HbF0: b ∈ F0.
An exact proof term for the current goal is (andER (F0 ∈ Fams) (b ∈ F0) HF0pair).
Set n to be the term idx F0.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (Hidx_to_omega F0 HF0F).
Set j to be the term (n,b).
We prove the intermediate claim HjSigma: j ∈ setprod ω B.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω B n b HnO HbB).
We prove the intermediate claim HjJ: j ∈ J.
Apply (SepI (setprod ω B) (λp : set ⇒ ∃G0 : set, G0 ∈ Fams ∧ idx G0 = (p 0) ∧ (p 1) ∈ G0) j HjSigma) to the current goal.
We use F0 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 HF0F.
rewrite the current goal using (tuple_2_0_eq n b) (from left to right).
Use reflexivity.
rewrite the current goal using (tuple_2_1_eq n b) (from left to right).
An exact proof term for the current goal is HbF0.
We use j 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 HjJ.
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBopen b HbU).
We prove the intermediate claim Hexb0: ∃f0 : set, continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x)).
An exact proof term for the current goal is (open_set_has_positive_support_function_unit_interval X Tx b Hnorm HclosedG HbTx).
Set P to be the term (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x))).
We prove the intermediate claim HPb: P (bump0 b).
An exact proof term for the current goal is (Eps_i_ex P Hexb0).
We prove the intermediate claim Hb0AB: continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HPb).
We prove the intermediate claim Hb0cont: continuous_map X Tx unit_interval unit_interval_topology (bump0 b).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0AB).
We prove the intermediate claim Hb0fun: function_on (bump0 b) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (bump0 b) Hb0cont).
We prove the intermediate claim Hb0pos_fun: ∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x).
An exact proof term for the current goal is (andER (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HPb).
We prove the intermediate claim Hb0pos: Rlt 0 (apply_fun (bump0 b) x0).
An exact proof term for the current goal is (Hb0pos_fun x0 Hx0b).
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 HinvR: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) HsuccO).
We prove the intermediate claim HinvPos: Rlt 0 (inv_nat (ordsucc n)).
We prove the intermediate claim HsuccNot0: ordsucc n ∉ {0}.
Assume H0: ordsucc n ∈ {0}.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) H0).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
We prove the intermediate claim HsuccIn: ordsucc n ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HsuccO.
An exact proof term for the current goal is HsuccNot0.
An exact proof term for the current goal is (inv_nat_pos (ordsucc n) HsuccIn).
We prove the intermediate claim HappF: apply_fun (apply_fun F j) x0 = mul_SNo (apply_fun (bump b) x0) (inv_nat (ordsucc n)).
We prove the intermediate claim HFdef: F = graph J (λp : set ⇒ bump_scaled (p 0) (p 1)).
Use reflexivity.
We prove the intermediate claim HappF0: apply_fun F j = bump_scaled (j 0) (j 1).
rewrite the current goal using HFdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph J (λp : set ⇒ bump_scaled (p 0) (p 1)) j HjJ).
rewrite the current goal using HappF0 (from left to right).
We prove the intermediate claim Hjdef: j = (n,b).
Use reflexivity.
rewrite the current goal using Hjdef (from left to right) at position 1.
rewrite the current goal using (tuple_2_0_eq n b) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq n b) (from left to right) at position 1.
We prove the intermediate claim Hbscdef: bump_scaled n b = compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n))).
Use reflexivity.
rewrite the current goal using Hbscdef (from left to right).
We prove the intermediate claim Hcomp: apply_fun (compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n)))) x0 = apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) x0).
An exact proof term for the current goal is (compose_fun_apply X (bump b) (mul_const_fun (inv_nat (ordsucc n))) x0 Hx0X).
We prove the intermediate claim Hb0AB: continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HPb).
We prove the intermediate claim Hb0cont: continuous_map X Tx unit_interval unit_interval_topology (bump0 b).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0AB).
We prove the intermediate claim Hb0fun: function_on (bump0 b) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (bump0 b) Hb0cont).
We prove the intermediate claim HbumpEq0: apply_fun (bump b) x0 = apply_fun (bump0 b) x0.
We prove the intermediate claim HbumpDef: bump b = graph X (λx : set ⇒ apply_fun (bump0 b) x).
Use reflexivity.
rewrite the current goal using HbumpDef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx : set ⇒ apply_fun (bump0 b) x) x0 Hx0X) (from left to right).
Use reflexivity.
We prove the intermediate claim HbumpR: apply_fun (bump b) x0 ∈ R.
rewrite the current goal using HbumpEq0 (from left to right).
We prove the intermediate claim Hx0I: apply_fun (bump0 b) x0 ∈ unit_interval.
An exact proof term for the current goal is (Hb0fun x0 Hx0X).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (bump0 b) x0) Hx0I).
We prove the intermediate claim Hmul: apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) x0) = mul_SNo (apply_fun (bump b) x0) (inv_nat (ordsucc n)).
An exact proof term for the current goal is (mul_const_fun_apply (inv_nat (ordsucc n)) (apply_fun (bump b) x0) HinvR HbumpR).
An exact proof term for the current goal is (eq_i_tra (apply_fun (compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n)))) x0) (apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) x0)) (mul_SNo (apply_fun (bump b) x0) (inv_nat (ordsucc n))) Hcomp Hmul).
rewrite the current goal using HappF (from left to right).
We prove the intermediate claim HbumpEq: apply_fun (bump b) x0 = apply_fun (bump0 b) x0.
We prove the intermediate claim HbumpDef: bump b = graph X (λx : set ⇒ apply_fun (bump0 b) x).
Use reflexivity.
rewrite the current goal using HbumpDef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx : set ⇒ apply_fun (bump0 b) x) x0 Hx0X) (from left to right).
Use reflexivity.
rewrite the current goal using HbumpEq (from left to right) at position 1.
We prove the intermediate claim Hx0S: SNo (apply_fun (bump0 b) x0).
An exact proof term for the current goal is (real_SNo (apply_fun (bump0 b) x0) (unit_interval_sub_R (apply_fun (bump0 b) x0) (Hb0fun x0 Hx0X))).
We prove the intermediate claim HinvS: SNo (inv_nat (ordsucc n)).
An exact proof term for the current goal is (real_SNo (inv_nat (ordsucc n)) HinvR).
An exact proof term for the current goal is (RltI 0 (mul_SNo (apply_fun (bump0 b) x0) (inv_nat (ordsucc n))) real_0 (real_mul_SNo_pos (apply_fun (bump0 b) x0) (unit_interval_sub_R (apply_fun (bump0 b) x0) (Hb0fun x0 Hx0X)) (inv_nat (ordsucc n)) HinvR (RltE_lt 0 (apply_fun (bump0 b) x0) Hb0pos) (RltE_lt 0 (inv_nat (ordsucc n)) HinvPos)) (mul_SNo_pos_pos (apply_fun (bump0 b) x0) (inv_nat (ordsucc n)) Hx0S HinvS (RltE_lt 0 (apply_fun (bump0 b) x0) Hb0pos) (RltE_lt 0 (inv_nat (ordsucc n)) HinvPos))).
Let x be given.
Assume HxOut: x ∈ X ∖ U0.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X U0 x HxOut).
We prove the intermediate claim HxnotU0: x ∉ U0.
An exact proof term for the current goal is (setminusE2 X U0 x HxOut).
We prove the intermediate claim Hxnotb: x ∉ b.
Assume Hxb: x ∈ b.
We prove the intermediate claim HxU0': x ∈ U0.
An exact proof term for the current goal is (HbsubU0 x Hxb).
An exact proof term for the current goal is (HxnotU0 HxU0').
We prove the intermediate claim HxOutb: x ∈ X ∖ b.
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 Hxnotb.
We prove the intermediate claim Hexb0': ∃f0 : set, continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x)).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBopen b HbU).
An exact proof term for the current goal is (open_set_has_positive_support_function_unit_interval X Tx b Hnorm HclosedG HbTx).
Set P0 to be the term (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x))).
We prove the intermediate claim HP0b: P0 (bump0 b).
An exact proof term for the current goal is (Eps_i_ex P0 Hexb0').
We prove the intermediate claim Hz0: apply_fun (bump0 b) x = 0.
We prove the intermediate claim Hb0AB0: continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HP0b).
We prove the intermediate claim Hb0zero: ∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0AB0).
An exact proof term for the current goal is (Hb0zero x HxOutb).
We prove the intermediate claim Happ: apply_fun (apply_fun F j) x = mul_SNo (apply_fun (bump b) x) (inv_nat (ordsucc n)).
We prove the intermediate claim HFdef: F = graph J (λp : set ⇒ bump_scaled (p 0) (p 1)).
Use reflexivity.
We prove the intermediate claim HappFj: apply_fun F j = bump_scaled (j 0) (j 1).
rewrite the current goal using HFdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph J (λp : set ⇒ bump_scaled (p 0) (p 1)) j HjJ).
rewrite the current goal using HappFj (from left to right).
We prove the intermediate claim Hjdef: j = (n,b).
Use reflexivity.
rewrite the current goal using Hjdef (from left to right) at position 1.
rewrite the current goal using (tuple_2_0_eq n b) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq n b) (from left to right) at position 1.
We prove the intermediate claim Hbscdef: bump_scaled n b = compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n))).
Use reflexivity.
rewrite the current goal using Hbscdef (from left to right).
We prove the intermediate claim Hcomp: apply_fun (compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n)))) x = apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) x).
An exact proof term for the current goal is (compose_fun_apply X (bump b) (mul_const_fun (inv_nat (ordsucc n))) x HxX).
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 HinvR0: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) HsuccO).
We prove the intermediate claim HbumpEqx0: apply_fun (bump b) x = apply_fun (bump0 b) x.
We prove the intermediate claim HbumpDef: bump b = graph X (λx : set ⇒ apply_fun (bump0 b) x).
Use reflexivity.
rewrite the current goal using HbumpDef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun (bump0 b) x0) x HxX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hb0AB1: continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HP0b).
We prove the intermediate claim Hb0cont1: continuous_map X Tx unit_interval unit_interval_topology (bump0 b).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0AB1).
We prove the intermediate claim Hb0fun1: function_on (bump0 b) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (bump0 b) Hb0cont1).
We prove the intermediate claim HbumpR: apply_fun (bump b) x ∈ R.
rewrite the current goal using HbumpEqx0 (from left to right).
We prove the intermediate claim HxI: apply_fun (bump0 b) x ∈ unit_interval.
An exact proof term for the current goal is (Hb0fun1 x HxX).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (bump0 b) x) HxI).
We prove the intermediate claim Hmul: apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) x) = mul_SNo (apply_fun (bump b) x) (inv_nat (ordsucc n)).
An exact proof term for the current goal is (mul_const_fun_apply (inv_nat (ordsucc n)) (apply_fun (bump b) x) HinvR0 HbumpR).
An exact proof term for the current goal is (eq_i_tra (apply_fun (compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n)))) x) (apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) x)) (mul_SNo (apply_fun (bump b) x) (inv_nat (ordsucc n))) Hcomp Hmul).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim HbumpEqx: apply_fun (bump b) x = apply_fun (bump0 b) x.
We prove the intermediate claim HbumpDef: bump b = graph X (λx : set ⇒ apply_fun (bump0 b) x).
Use reflexivity.
rewrite the current goal using HbumpDef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx : set ⇒ apply_fun (bump0 b) x) x HxX) (from left to right).
Use reflexivity.
rewrite the current goal using HbumpEqx (from left to right) at position 1.
rewrite the current goal using Hz0 (from left to right).
We prove the intermediate claim HinvR: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) (omega_ordsucc n HnO)).
We prove the intermediate claim HinvS: SNo (inv_nat (ordsucc n)).
An exact proof term for the current goal is (real_SNo (inv_nat (ordsucc n)) HinvR).
rewrite the current goal using (mul_SNo_zeroL (inv_nat (ordsucc n)) HinvS) (from left to right).
Use reflexivity.
Set Fmap to be the term diagonal_map X F J.
Set dY to be the term uniform_metric_power_real J.
We prove the intermediate claim HmY: metric_on (power_real J) dY.
An exact proof term for the current goal is (uniform_metric_power_real_is_metric_on J).
We prove the intermediate claim HsepABC: (topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j : set, j ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j)).
An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j : set, j ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x0) ∧ ∀x : set, x ∈ X ∖ U0 → apply_fun (apply_fun F j) x = 0) Hsep).
We prove the intermediate claim HsepNeigh: ∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x0) ∧ ∀x : set, x ∈ X ∖ U0 → apply_fun (apply_fun F j) x = 0.
An exact proof term for the current goal is (andER ((topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j : set, j ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x0) ∧ ∀x : set, x ∈ X ∖ U0 → apply_fun (apply_fun F j) x = 0) Hsep).
We prove the intermediate claim HtopTot: topology_on X Tx ∧ total_function_on F J (function_space X R).
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ total_function_on F J (function_space X R)) (∀j : set, j ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j)) HsepABC).
We prove the intermediate claim HtotF: total_function_on F J (function_space X R).
An exact proof term for the current goal is (andER (topology_on X Tx) (total_function_on F J (function_space X R)) HtopTot).
We prove the intermediate claim HFmapfun: function_on Fmap X (power_real J).
An exact proof term for the current goal is (diagonal_map_function_on_power_real X F J HtotF).
We prove the intermediate claim Hf_inj: ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → apply_fun Fmap x1 = apply_fun Fmap x2 → x1 = x2.
Let x1 and x2 be given.
Assume Hx1X: x1 ∈ X.
Assume Hx2X: x2 ∈ X.
Assume HeqF: apply_fun Fmap x1 = apply_fun Fmap x2.
Apply (xm (x1 = x2)) to the current goal.
An exact proof term for the current goal is (λH ⇒ H).
Assume Hne: x1 ≠ x2.
We will prove False.
We prove the intermediate claim Hexj: ∃j : set, j ∈ J ∧ apply_fun (apply_fun F j) x1 ≠ apply_fun (apply_fun F j) x2.
An exact proof term for the current goal is (separating_family_of_functions_separates_points X Tx F J x1 x2 HTx HT1 Hsep Hx1X Hx2X Hne).
Apply Hexj to the current goal.
Let j be given.
Assume Hjpair: j ∈ J ∧ apply_fun (apply_fun F j) x1 ≠ apply_fun (apply_fun F j) x2.
We prove the intermediate claim HjJ: j ∈ J.
An exact proof term for the current goal is (andEL (j ∈ J) (apply_fun (apply_fun F j) x1 ≠ apply_fun (apply_fun F j) x2) Hjpair).
We prove the intermediate claim Hneq: apply_fun (apply_fun F j) x1 ≠ apply_fun (apply_fun F j) x2.
An exact proof term for the current goal is (andER (j ∈ J) (apply_fun (apply_fun F j) x1 ≠ apply_fun (apply_fun F j) x2) Hjpair).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun Fmap x1) j = apply_fun (apply_fun Fmap x2) j.
rewrite the current goal using HeqF (from left to right).
Use reflexivity.
We prove the intermediate claim Hcoord1: apply_fun (apply_fun Fmap x1) j = apply_fun (apply_fun F j) x1.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J x1 j Hx1X HjJ).
We prove the intermediate claim Hcoord2: apply_fun (apply_fun Fmap x2) j = apply_fun (apply_fun F j) x2.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J x2 j Hx2X HjJ).
We prove the intermediate claim HeqFj: apply_fun (apply_fun F j) x1 = apply_fun (apply_fun F j) x2.
rewrite the current goal using Hcoord1 (from right to left).
rewrite the current goal using Hcoord2 (from right to left).
An exact proof term for the current goal is HcoordEq.
An exact proof term for the current goal is (Hneq HeqFj).
Set dX to be the term graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
We prove the intermediate claim HdefMet: metrizable X Tx = ∃d : set, metric_on X d ∧ metric_topology X d = Tx.
Use reflexivity.
rewrite the current goal using HdefMet (from left to right).
We use dX to witness the existential quantifier.
Apply andI to the current goal.
We will prove metric_on X dX.
We prove the intermediate claim Hmdef: metric_on X dX = (function_on dX (setprod X X) R ∧ (∀x y : set, x ∈ X → y ∈ X → apply_fun dX (x,y) = apply_fun dX (y,x)) ∧ (∀x : set, x ∈ X → apply_fun dX (x,x) = 0) ∧ (∀x y : set, x ∈ X → y ∈ X → ¬ (Rlt (apply_fun dX (x,y)) 0) ∧ (apply_fun dX (x,y) = 0 → x = y)) ∧ (∀x y z : set, x ∈ X → y ∈ X → z ∈ X → ¬ (Rlt (add_SNo (apply_fun dX (x,y)) (apply_fun dX (y,z))) (apply_fun dX (x,z))))).
Use reflexivity.
rewrite the current goal using Hmdef (from left to right).
Apply and5I to the current goal.
We prove the intermediate claim HtotdX: total_function_on dX (setprod X X) R.
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
rewrite the current goal using HdXdef (from left to right).
Apply (total_function_on_graph (setprod X X) R (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1)))) to the current goal.
Let pq be given.
Assume Hpq: pq ∈ setprod X X.
We will prove apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1)) ∈ R.
We prove the intermediate claim HxX: (pq 0) ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ X) pq Hpq).
We prove the intermediate claim HyX: (pq 1) ∈ X.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ X) pq Hpq).
We prove the intermediate claim HfxY: apply_fun Fmap (pq 0) ∈ power_real J.
An exact proof term for the current goal is (HFmapfun (pq 0) HxX).
We prove the intermediate claim HfyY: apply_fun Fmap (pq 1) ∈ power_real J.
An exact proof term for the current goal is (HFmapfun (pq 1) HyX).
We prove the intermediate claim HpairY: (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1)) ∈ setprod (power_real J) (power_real J).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (power_real J) (power_real J) (apply_fun Fmap (pq 0)) (apply_fun Fmap (pq 1)) HfxY HfyY).
An exact proof term for the current goal is ((metric_on_function_on (power_real J) dY HmY) (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1)) HpairY).
An exact proof term for the current goal is (total_function_on_function_on dX (setprod X X) R HtotdX).
Let x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
We will prove apply_fun dX (x,y) = apply_fun dX (y,x).
We prove the intermediate claim HfxY: apply_fun Fmap x ∈ power_real J.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ power_real J.
An exact proof term for the current goal is (HFmapfun y HyX).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HyxIn: (y,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y x HyX HxX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
We prove the intermediate claim HxyEq0: apply_fun dX (x,y) = apply_fun dY (apply_fun Fmap ((x,y) 0),apply_fun Fmap ((x,y) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,y) HxyIn).
We prove the intermediate claim HyxEq0: apply_fun dX (y,x) = apply_fun dY (apply_fun Fmap ((y,x) 0),apply_fun Fmap ((y,x) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (y,x) HyxIn).
rewrite the current goal using HxyEq0 (from left to right).
rewrite the current goal using HyxEq0 (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (tuple_2_0_eq y x) (from left to right).
rewrite the current goal using (tuple_2_1_eq y x) (from left to right).
An exact proof term for the current goal is (metric_on_symmetric (power_real J) dY (apply_fun Fmap x) (apply_fun Fmap y) HmY HfxY HfyY).
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun dX (x,x) = 0.
We prove the intermediate claim HfxY: apply_fun Fmap x ∈ power_real J.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HxxIn: (x,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x x HxX HxX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
We prove the intermediate claim HxxEq0: apply_fun dX (x,x) = apply_fun dY (apply_fun Fmap ((x,x) 0),apply_fun Fmap ((x,x) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,x) HxxIn).
rewrite the current goal using HxxEq0 (from left to right).
rewrite the current goal using (tuple_2_0_eq x x) (from left to right).
rewrite the current goal using (tuple_2_1_eq x x) (from left to right).
An exact proof term for the current goal is (metric_on_diag_zero (power_real J) dY (apply_fun Fmap x) HmY HfxY).
Let x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
We will prove ¬ (Rlt (apply_fun dX (x,y)) 0) ∧ (apply_fun dX (x,y) = 0 → x = y).
Apply andI to the current goal.
We prove the intermediate claim HfxY: apply_fun Fmap x ∈ power_real J.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ power_real J.
An exact proof term for the current goal is (HFmapfun y HyX).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
We prove the intermediate claim HxyEq0: apply_fun dX (x,y) = apply_fun dY (apply_fun Fmap ((x,y) 0),apply_fun Fmap ((x,y) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,y) HxyIn).
rewrite the current goal using HxyEq0 (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
An exact proof term for the current goal is (metric_on_nonneg (power_real J) dY (apply_fun Fmap x) (apply_fun Fmap y) HmY HfxY HfyY).
Assume H0: apply_fun dX (x,y) = 0.
We will prove x = y.
We prove the intermediate claim HfxY: apply_fun Fmap x ∈ power_real J.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ power_real J.
An exact proof term for the current goal is (HFmapfun y HyX).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
We prove the intermediate claim HxyEq0: apply_fun dX (x,y) = apply_fun dY (apply_fun Fmap ((x,y) 0),apply_fun Fmap ((x,y) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,y) HxyIn).
We prove the intermediate claim HyEq0: apply_fun dY (apply_fun Fmap x,apply_fun Fmap y) = 0.
We prove the intermediate claim HxyEqRev: apply_fun dY (apply_fun Fmap ((x,y) 0),apply_fun Fmap ((x,y) 1)) = apply_fun dX (x,y).
Use symmetry.
An exact proof term for the current goal is HxyEq0.
We prove the intermediate claim Htmp: apply_fun dY (apply_fun Fmap ((x,y) 0),apply_fun Fmap ((x,y) 1)) = 0.
An exact proof term for the current goal is (eq_i_tra (apply_fun dY (apply_fun Fmap ((x,y) 0),apply_fun Fmap ((x,y) 1))) (apply_fun dX (x,y)) 0 HxyEqRev H0).
rewrite the current goal using (tuple_2_0_eq x y) (from right to left) at position 1.
rewrite the current goal using (tuple_2_1_eq x y) (from right to left) at position 2.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HfyEq: apply_fun Fmap x = apply_fun Fmap y.
An exact proof term for the current goal is (metric_on_zero_eq (power_real J) dY (apply_fun Fmap x) (apply_fun Fmap y) HmY HfxY HfyY HyEq0).
An exact proof term for the current goal is (Hf_inj x y HxX HyX HfyEq).
Let x, y and z be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume HzX: z ∈ X.
We will prove ¬ (Rlt (add_SNo (apply_fun dX (x,y)) (apply_fun dX (y,z))) (apply_fun dX (x,z))).
We prove the intermediate claim HfxY: apply_fun Fmap x ∈ power_real J.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ power_real J.
An exact proof term for the current goal is (HFmapfun y HyX).
We prove the intermediate claim HfzY: apply_fun Fmap z ∈ power_real J.
An exact proof term for the current goal is (HFmapfun z HzX).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HyzIn: (y,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y z HyX HzX).
We prove the intermediate claim HxzIn: (x,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x z HxX HzX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
We prove the intermediate claim HxyEq0: apply_fun dX (x,y) = apply_fun dY (apply_fun Fmap ((x,y) 0),apply_fun Fmap ((x,y) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,y) HxyIn).
We prove the intermediate claim HyzEq0: apply_fun dX (y,z) = apply_fun dY (apply_fun Fmap ((y,z) 0),apply_fun Fmap ((y,z) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (y,z) HyzIn).
We prove the intermediate claim HxzEq0: apply_fun dX (x,z) = apply_fun dY (apply_fun Fmap ((x,z) 0),apply_fun Fmap ((x,z) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,z) HxzIn).
rewrite the current goal using HxyEq0 (from left to right).
rewrite the current goal using HyzEq0 (from left to right).
rewrite the current goal using HxzEq0 (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (tuple_2_0_eq y z) (from left to right).
rewrite the current goal using (tuple_2_1_eq y z) (from left to right).
rewrite the current goal using (tuple_2_0_eq x z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x z) (from left to right).
An exact proof term for the current goal is (metric_on_triangle (power_real J) dY (apply_fun Fmap x) (apply_fun Fmap y) (apply_fun Fmap z) HmY HfxY HfyY HfzY).
We will prove metric_topology X dX = Tx.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ metric_topology X dX.
We will prove U ∈ Tx.
Set Bx to be the term famunion X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim Hmtdef: metric_topology X dX = generated_topology X Bx.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology X Bx.
rewrite the current goal using Hmtdef (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim HBxSub: ∀b ∈ Bx, b ∈ Tx.
Let b be given.
Assume HbBx: b ∈ Bx.
We will prove b ∈ Tx.
Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}) b HbBx (b ∈ Tx)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume HbIn: b ∈ {open_ball X dX c r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X dX c r0) b HbIn (b ∈ Tx)) to the current goal.
Let r be given.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume Hbeq: b = open_ball X dX c r.
rewrite the current goal using Hbeq (from left to right).
Set Ball to be the term open_ball X dX c r.
We prove the intermediate claim HBallSubX: Ball ⊆ X.
An exact proof term for the current goal is (open_ball_subset_X X dX c r).
Set Fam to be the term {V ∈ Tx|V ⊆ Ball}.
We prove the intermediate claim HFamSubTx: Fam ⊆ Tx.
Let V be given.
Assume HVFam: V ∈ Fam.
An exact proof term for the current goal is (SepE1 Tx (λV0 : set ⇒ V0 ⊆ Ball) V HVFam).
We prove the intermediate claim HFamPowTx: Fam ∈ 𝒫 Tx.
Apply PowerI to the current goal.
An exact proof term for the current goal is HFamSubTx.
We prove the intermediate claim HUnionInTx: ⋃ Fam ∈ Tx.
An exact proof term for the current goal is (topology_union_axiom X Tx HTx Fam HFamPowTx).
We prove the intermediate claim HUnionEq: ⋃ Fam = Ball.
Apply set_ext to the current goal.
Let y be given.
Assume HyU: y ∈ ⋃ Fam.
Apply (UnionE_impred Fam y HyU) to the current goal.
Let V be given.
Assume HyV: y ∈ V.
Assume HVFam: V ∈ Fam.
We prove the intermediate claim HVsub: V ⊆ Ball.
An exact proof term for the current goal is (SepE2 Tx (λV0 : set ⇒ V0 ⊆ Ball) V HVFam).
An exact proof term for the current goal is (HVsub y HyV).
Let y be given.
Assume HyBall: y ∈ Ball.
We prove the intermediate claim HexV: ∃V : set, V ∈ Tx ∧ y ∈ V ∧ V ⊆ Ball.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X dX c r y HyBall).
Apply (xm (J = Empty)) to the current goal.
Assume HJ0: J = Empty.
We use X to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
An exact proof term for the current goal is HyX.
Let z be given.
Assume HzX: z ∈ X.
We will prove z ∈ Ball.
We prove the intermediate claim HBallDef: Ball = {y0 ∈ X|Rlt (apply_fun dX (c,y0)) r}.
Use reflexivity.
rewrite the current goal using HBallDef (from left to right).
We prove the intermediate claim Hlt: Rlt (apply_fun dX (c,z)) r.
We prove the intermediate claim Hpair: (c,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c z HcX HzX).
We prove the intermediate claim HfcY: apply_fun Fmap c ∈ power_real J.
An exact proof term for the current goal is (HFmapfun c HcX).
We prove the intermediate claim HfzY: apply_fun Fmap z ∈ power_real J.
An exact proof term for the current goal is (HFmapfun z HzX).
We prove the intermediate claim HdYapp: apply_fun dY (apply_fun Fmap c,apply_fun Fmap z) = power_real_uniform_metric_value J (apply_fun Fmap c) (apply_fun Fmap z).
We prove the intermediate claim HdYdef: dY = uniform_metric_power_real J.
Use reflexivity.
rewrite the current goal using HdYdef (from left to right).
An exact proof term for the current goal is (uniform_metric_power_real_apply J (apply_fun Fmap c) (apply_fun Fmap z) HfcY HfzY).
We prove the intermediate claim H0val: power_real_uniform_metric_value J (apply_fun Fmap c) (apply_fun Fmap z) = 0.
We prove the intermediate claim HdefV: power_real_uniform_metric_value J (apply_fun Fmap c) (apply_fun Fmap z) = If_i (J = Empty) 0 (Eps_i (λr0 : set ⇒ R_lub (power_real_clipped_diffs J (apply_fun Fmap c) (apply_fun Fmap z)) r0)).
Use reflexivity.
rewrite the current goal using HdefV (from left to right).
rewrite the current goal using (If_i_1 (J = Empty) 0 (Eps_i (λr0 : set ⇒ R_lub (power_real_clipped_diffs J (apply_fun Fmap c) (apply_fun Fmap z)) r0)) HJ0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hcz0: apply_fun dX (c,z) = 0.
We prove the intermediate claim HdXdef2: dX = graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))).
Use reflexivity.
We prove the intermediate claim HczEq: apply_fun dX (c,z) = apply_fun dY (apply_fun Fmap c,apply_fun Fmap z).
rewrite the current goal using HdXdef2 (from left to right).
We prove the intermediate claim Htmp: apply_fun (graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1)))) (c,z) = apply_fun dY (apply_fun Fmap ((c,z) 0),apply_fun Fmap ((c,z) 1)).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (c,z) Hpair).
rewrite the current goal using Htmp (from left to right).
rewrite the current goal using (tuple_2_0_eq c z) (from left to right).
rewrite the current goal using (tuple_2_1_eq c z) (from left to right).
Use reflexivity.
We prove the intermediate claim HdY0: apply_fun dY (apply_fun Fmap c,apply_fun Fmap z) = 0.
rewrite the current goal using HdYapp (from left to right).
rewrite the current goal using H0val (from left to right).
Use reflexivity.
An exact proof term for the current goal is (eq_i_tra (apply_fun dX (c,z)) (apply_fun dY (apply_fun Fmap c,apply_fun Fmap z)) 0 HczEq HdY0).
rewrite the current goal using Hcz0 (from left to right).
An exact proof term for the current goal is Hrpos.
An exact proof term for the current goal is (SepI X (λy0 : set ⇒ Rlt (apply_fun dX (c,y0)) r) z HzX Hlt).
Assume HJne: J ≠ Empty.
We prove the intermediate claim HexVJne: ∃V : set, V ∈ Tx ∧ y ∈ V ∧ V ⊆ Ball.
Set dist to be the term apply_fun dX (c,y).
We prove the intermediate claim Hdistlt: Rlt dist r.
An exact proof term for the current goal is (open_ballE2 X dX c r y HyBall).
We prove the intermediate claim Hcypair: (c,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c y HcX HyX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ power_real J.
An exact proof term for the current goal is (HFmapfun y HyX).
We prove the intermediate claim HfcY: apply_fun Fmap c ∈ power_real J.
An exact proof term for the current goal is (HFmapfun c HcX).
We prove the intermediate claim HdXdef2: dX = graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))).
Use reflexivity.
We prove the intermediate claim HdistEq: dist = apply_fun dY (apply_fun Fmap c,apply_fun Fmap y).
rewrite the current goal using HdXdef2 (from left to right).
We prove the intermediate claim Htmp: apply_fun (graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1)))) (c,y) = apply_fun dY (apply_fun Fmap ((c,y) 0),apply_fun Fmap ((c,y) 1)).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (c,y) Hcypair).
rewrite the current goal using Htmp (from left to right).
rewrite the current goal using (tuple_2_0_eq c y) (from left to right).
rewrite the current goal using (tuple_2_1_eq c y) (from left to right).
Use reflexivity.
We prove the intermediate claim HdYfun: function_on dY (setprod (power_real J) (power_real J)) R.
An exact proof term for the current goal is (metric_on_function_on (power_real J) dY HmY).
We prove the intermediate claim HpairCY: (apply_fun Fmap c,apply_fun Fmap y) ∈ setprod (power_real J) (power_real J).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (power_real J) (power_real J) (apply_fun Fmap c) (apply_fun Fmap y) HfcY HfyY).
We prove the intermediate claim HdistR: dist ∈ R.
rewrite the current goal using HdistEq (from left to right).
An exact proof term for the current goal is (HdYfun (apply_fun Fmap c,apply_fun Fmap y) HpairCY).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HdistS: SNo dist.
An exact proof term for the current goal is (real_SNo dist HdistR).
Set gap to be the term add_SNo r (minus_SNo dist).
We prove the intermediate claim HgapPos: Rlt 0 gap.
An exact proof term for the current goal is (Rlt_0_diff_of_lt dist r Hdistlt).
We prove the intermediate claim HgapR: gap ∈ R.
An exact proof term for the current goal is (real_add_SNo r HrR (minus_SNo dist) (real_minus_SNo dist HdistR)).
We prove the intermediate claim Hexd: ∃Nd ∈ ω, eps_ Nd < gap.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid gap HgapR HgapPos).
Apply Hexd to the current goal.
Let Nd be given.
Assume HNdPair.
We prove the intermediate claim HNdO: Nd ∈ ω.
An exact proof term for the current goal is (andEL (Nd ∈ ω) (eps_ Nd < gap) HNdPair).
We prove the intermediate claim HdltGapS: eps_ Nd < gap.
An exact proof term for the current goal is (andER (Nd ∈ ω) (eps_ Nd < gap) HNdPair).
Set d to be the term eps_ Nd.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (SNoS_omega_real d (SNo_eps_SNoS_omega Nd HNdO)).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim HdposS: 0 < d.
An exact proof term for the current goal is (SNo_eps_pos Nd HNdO).
We prove the intermediate claim Hdpos: Rlt 0 d.
An exact proof term for the current goal is (RltI 0 d real_0 HdR HdposS).
We prove the intermediate claim HsumLtS: add_SNo d dist < r.
An exact proof term for the current goal is (add_SNo_minus_Lt2 r dist d HrS HdistS HdS HdltGapS).
We prove the intermediate claim HsumLtR: Rlt (add_SNo d dist) r.
An exact proof term for the current goal is (RltI (add_SNo d dist) r (real_add_SNo d HdR dist HdistR) HrR HsumLtS).
We prove the intermediate claim HexV0: ∃V : set, V ∈ Tx ∧ y ∈ V ∧ ∀z : set, z ∈ V → Rlt (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) d.
We prove the intermediate claim HexN0: ∃N0 : set, N0 ∈ ω ∧ Rlt (inv_nat (ordsucc N0)) d.
An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt_local d HdR Hdpos).
Apply HexN0 to the current goal.
Let N0 be given.
Assume HN0pair.
We prove the intermediate claim HN0O: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (Rlt (inv_nat (ordsucc N0)) d) HN0pair).
We prove the intermediate claim HinvN0Lt: Rlt (inv_nat (ordsucc N0)) d.
An exact proof term for the current goal is (andER (N0 ∈ ω) (Rlt (inv_nat (ordsucc N0)) d) HN0pair).
Set FamsSmall to be the term {F0 ∈ Fams|idx F0 ∈ ordsucc N0}.
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 HFamsSmallFin: finite FamsSmall.
An exact proof term for the current goal is (inj_omega_preimage_ordsucc_finite Fams N0 idx HN0nat Hidxinj).
Set invN0 to be the term inv_nat (ordsucc N0).
We prove the intermediate claim HinvN0R: invN0 ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc N0) (omega_ordsucc N0 HN0O)).
We prove the intermediate claim HinvN0S: SNo invN0.
An exact proof term for the current goal is (real_SNo invN0 HinvN0R).
Set gap0 to be the term add_SNo d (minus_SNo invN0).
We prove the intermediate claim Hgap0R: gap0 ∈ R.
An exact proof term for the current goal is (real_add_SNo d HdR (minus_SNo invN0) (real_minus_SNo invN0 HinvN0R)).
We prove the intermediate claim Hgap0Pos: Rlt 0 gap0.
An exact proof term for the current goal is (Rlt_0_diff_of_lt invN0 d HinvN0Lt).
We prove the intermediate claim HexN1: ∃N1 ∈ ω, eps_ N1 < gap0.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid gap0 Hgap0R Hgap0Pos).
Apply HexN1 to the current goal.
Let N1 be given.
Assume HN1pair.
We prove the intermediate claim HN1O: N1 ∈ ω.
An exact proof term for the current goal is (andEL (N1 ∈ ω) (eps_ N1 < gap0) HN1pair).
We prove the intermediate claim Heps1LtGap0S: eps_ N1 < gap0.
An exact proof term for the current goal is (andER (N1 ∈ ω) (eps_ N1 < gap0) HN1pair).
Set eps1 to be the term eps_ N1.
We prove the intermediate claim Heps1R: eps1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eps1 (SNo_eps_SNoS_omega N1 HN1O)).
We prove the intermediate claim Heps1S: SNo eps1.
An exact proof term for the current goal is (real_SNo eps1 Heps1R).
Set eps2 to be the term eps_ (ordsucc N1).
We prove the intermediate claim Heps2O: ordsucc N1 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N1 HN1O).
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 N1) Heps2O)).
We prove the intermediate claim Heps2S: SNo eps2.
An exact proof term for the current goal is (real_SNo eps2 Heps2R).
Set eps3 to be the term eps_ (ordsucc (ordsucc N1)).
We prove the intermediate claim Heps3O: ordsucc (ordsucc N1) ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (ordsucc N1) Heps2O).
We prove the intermediate claim Heps3R: eps3 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eps3 (SNo_eps_SNoS_omega (ordsucc (ordsucc N1)) Heps3O)).
We prove the intermediate claim Heps3S: SNo eps3.
An exact proof term for the current goal is (real_SNo eps3 Heps3R).
Set u0 to be the term add_SNo invN0 eps1.
We prove the intermediate claim Hu0R: u0 ∈ R.
An exact proof term for the current goal is (real_add_SNo invN0 HinvN0R eps1 Heps1R).
We prove the intermediate claim Hu0S: SNo u0.
An exact proof term for the current goal is (real_SNo u0 Hu0R).
We prove the intermediate claim HdLt0S: add_SNo eps1 invN0 < d.
An exact proof term for the current goal is (add_SNo_minus_Lt2 d invN0 eps1 HdS HinvN0S Heps1S Heps1LtGap0S).
We prove the intermediate claim Hu0LtdS: u0 < d.
rewrite the current goal using (add_SNo_com invN0 eps1 HinvN0S Heps1S) (from left to right).
An exact proof term for the current goal is HdLt0S.
We prove the intermediate claim Hu0Ltd: Rlt u0 d.
An exact proof term for the current goal is (RltI u0 d Hu0R HdR Hu0LtdS).
We prove the intermediate claim HexVsmall: ∃Vsmall : set, Vsmall ∈ Tx ∧ y ∈ Vsmall ∧ ∀F0 : set, F0 ∈ FamsSmall → ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ S.
Set Nsel to be the term λF0 : set ⇒ Eps_i (λN : set ⇒ N ∈ Tx ∧ y ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ N ≠ Empty → b ∈ S).
Set Ssel to be the term λF0 : set ⇒ Eps_i (λS : set ⇒ finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ S).
We prove the intermediate claim HNselSpec: ∀F0 : set, F0 ∈ FamsSmall → (Nsel F0) ∈ Tx ∧ y ∈ (Nsel F0) ∧ ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ S.
Let F0 be given.
Assume HF0small: F0 ∈ FamsSmall.
We prove the intermediate claim HF0Fams: F0 ∈ Fams.
An exact proof term for the current goal is (SepE1 Fams (λF1 : set ⇒ idx F1 ∈ ordsucc N0) F0 HF0small).
We prove the intermediate claim HLF0: locally_finite_family X Tx F0.
An exact proof term for the current goal is (_HLFams F0 HF0Fams).
We prove the intermediate claim HLF0prop: ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ N ≠ Empty → b ∈ S.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ N ≠ Empty → b ∈ S) HLF0).
We prove the intermediate claim HexNS: ∃N : set, N ∈ Tx ∧ y ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ N ≠ Empty → b ∈ S.
An exact proof term for the current goal is (HLF0prop y HyX).
An exact proof term for the current goal is (Eps_i_ex (λN : set ⇒ N ∈ Tx ∧ y ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ N ≠ Empty → b ∈ S) HexNS).
We prove the intermediate claim HSselSpec: ∀F0 : set, F0 ∈ FamsSmall → finite (Ssel F0) ∧ (Ssel F0) ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ (Ssel F0).
Let F0 be given.
Assume HF0small: F0 ∈ FamsSmall.
We prove the intermediate claim HNpack: (Nsel F0) ∈ Tx ∧ y ∈ (Nsel F0) ∧ ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ S.
An exact proof term for the current goal is (HNselSpec F0 HF0small).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ S.
An exact proof term for the current goal is (andER ((Nsel F0) ∈ Tx ∧ y ∈ (Nsel F0)) (∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ S) HNpack).
An exact proof term for the current goal is (Eps_i_ex (λS : set ⇒ finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ S) HexS).
Set Nfam to be the term {Nsel F0|F0 ∈ FamsSmall}.
Set Vsmall to be the term intersection_of_family X Nfam.
We use Vsmall to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HNfamFin: finite Nfam.
An exact proof term for the current goal is (finite_Repl FamsSmall HFamsSmallFin Nsel).
We prove the intermediate claim HNfamSubTx: Nfam ⊆ Tx.
Let U be given.
Assume HU: U ∈ Nfam.
We will prove U ∈ Tx.
Apply (ReplE_impred FamsSmall Nsel U HU (U ∈ Tx)) to the current goal.
Let F0 be given.
Assume HF0small: F0 ∈ FamsSmall.
Assume HUeq: U = Nsel F0.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim Hpair: (Nsel F0) ∈ Tx ∧ y ∈ (Nsel F0).
An exact proof term for the current goal is (andEL ((Nsel F0) ∈ Tx ∧ y ∈ (Nsel F0)) (∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ S) (HNselSpec F0 HF0small)).
An exact proof term for the current goal is (andEL ((Nsel F0) ∈ Tx) (y ∈ (Nsel F0)) Hpair).
We prove the intermediate claim HNfamPow: Nfam ∈ 𝒫 Tx.
An exact proof term for the current goal is (PowerI Tx Nfam HNfamSubTx).
An exact proof term for the current goal is (finite_intersection_in_topology X Tx Nfam HTx HNfamPow HNfamFin).
We prove the intermediate claim HVsmallDef: Vsmall = intersection_of_family X Nfam.
Use reflexivity.
rewrite the current goal using HVsmallDef (from left to right).
We prove the intermediate claim HallU: ∀U : set, U ∈ Nfam → y ∈ U.
Let U be given.
Assume HU: U ∈ Nfam.
Apply (ReplE_impred FamsSmall Nsel U HU (y ∈ U)) to the current goal.
Let F0 be given.
Assume HF0small: F0 ∈ FamsSmall.
Assume HUeq: U = Nsel F0.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim Hpair: (Nsel F0) ∈ Tx ∧ y ∈ (Nsel F0).
An exact proof term for the current goal is (andEL ((Nsel F0) ∈ Tx ∧ y ∈ (Nsel F0)) (∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ S) (HNselSpec F0 HF0small)).
An exact proof term for the current goal is (andER ((Nsel F0) ∈ Tx) (y ∈ (Nsel F0)) Hpair).
An exact proof term for the current goal is (intersection_of_familyI X Nfam y HyX HallU).
Let F0 be given.
Assume HF0small: F0 ∈ FamsSmall.
We use (Ssel F0) to witness the existential quantifier.
We prove the intermediate claim HSspec: finite (Ssel F0) ∧ (Ssel F0) ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ (Ssel F0).
An exact proof term for the current goal is (HSselSpec F0 HF0small).
Apply andI to the current goal.
We prove the intermediate claim HSleft: finite (Ssel F0) ∧ (Ssel F0) ⊆ F0.
An exact proof term for the current goal is (andEL (finite (Ssel F0) ∧ (Ssel F0) ⊆ F0) (∀b : set, b ∈ F0 → b ∩ (Nsel F0) ≠ Empty → b ∈ (Ssel F0)) HSspec).
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (finite (Ssel F0)) ((Ssel F0) ⊆ F0) HSleft).
An exact proof term for the current goal is (andER (finite (Ssel F0)) ((Ssel F0) ⊆ F0) HSleft).
Let b be given.
Assume HbF0: b ∈ F0.
Assume HbcapV: b ∩ Vsmall ≠ Empty.
We prove the intermediate claim HbcapN: b ∩ (Nsel F0) ≠ Empty.
Apply (nonempty_has_element (b ∩ Vsmall) HbcapV) to the current goal.
Let x be given.
Assume Hx: x ∈ b ∩ Vsmall.
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (binintersectE1 b Vsmall x Hx).
We prove the intermediate claim HxV: x ∈ Vsmall.
An exact proof term for the current goal is (binintersectE2 b Vsmall x Hx).
We prove the intermediate claim HNselIn: (Nsel F0) ∈ Nfam.
An exact proof term for the current goal is (ReplI FamsSmall Nsel F0 HF0small).
We prove the intermediate claim HxN: x ∈ (Nsel F0).
An exact proof term for the current goal is (intersection_of_familyE2 X Nfam x HxV (Nsel F0) HNselIn).
An exact proof term for the current goal is (elem_implies_nonempty (b ∩ (Nsel F0)) x (binintersectI b (Nsel F0) x Hxb HxN)).
An exact proof term for the current goal is ((andER (finite (Ssel F0) ∧ (Ssel F0) ⊆ F0) (∀b0 : set, b0 ∈ F0 → b0 ∩ (Nsel F0) ≠ Empty → b0 ∈ (Ssel F0)) HSspec) b HbF0 HbcapN).
Apply HexVsmall to the current goal.
Let Vsmall be given.
Assume HVsmallPack.
We prove the intermediate claim HVsmallPair: Vsmall ∈ Tx ∧ y ∈ Vsmall.
An exact proof term for the current goal is (andEL (Vsmall ∈ Tx ∧ y ∈ Vsmall) (∀F0 : set, F0 ∈ FamsSmall → ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ S) HVsmallPack).
We prove the intermediate claim HVsmallTx: Vsmall ∈ Tx.
An exact proof term for the current goal is (andEL (Vsmall ∈ Tx) (y ∈ Vsmall) HVsmallPair).
We prove the intermediate claim HyVsmall: y ∈ Vsmall.
An exact proof term for the current goal is (andER (Vsmall ∈ Tx) (y ∈ Vsmall) HVsmallPair).
We prove the intermediate claim HVsmallLF: ∀F0 : set, F0 ∈ FamsSmall → ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ S.
An exact proof term for the current goal is (andER (Vsmall ∈ Tx ∧ y ∈ Vsmall) (∀F0 : set, F0 ∈ FamsSmall → ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ S) HVsmallPack).
Set Sfun to be the term λF0 : set ⇒ Eps_i (λS : set ⇒ finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ S).
We prove the intermediate claim HSfunSpec: ∀F0 : set, F0 ∈ FamsSmall → finite (Sfun F0) ∧ (Sfun F0) ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ (Sfun F0).
Let F0 be given.
Assume HF0small: F0 ∈ FamsSmall.
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ S.
An exact proof term for the current goal is (HVsmallLF F0 HF0small).
An exact proof term for the current goal is (Eps_i_ex (λS : set ⇒ finite S ∧ S ⊆ F0 ∧ ∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ S) HexS).
Set Jsel to be the term λF0 : set ⇒ Repl (Sfun F0) (λb0 : set ⇒ (idx F0,b0)).
Set Jfam to be the term {Jsel F0|F0 ∈ FamsSmall}.
Set Jneed to be the term ⋃ Jfam.
We prove the intermediate claim HJfamFin: finite Jfam.
An exact proof term for the current goal is (finite_Repl FamsSmall HFamsSmallFin Jsel).
We prove the intermediate claim HJfamAllFin: ∀A : set, A ∈ Jfam → finite A.
Let A be given.
Assume HA: A ∈ Jfam.
Apply (ReplE_impred FamsSmall Jsel A HA (finite A)) to the current goal.
Let F0 be given.
Assume HF0small: F0 ∈ FamsSmall.
Assume HAeq: A = Jsel F0.
rewrite the current goal using HAeq (from left to right).
We prove the intermediate claim HSfin: finite (Sfun F0).
An exact proof term for the current goal is (andEL (finite (Sfun F0)) ((Sfun F0) ⊆ F0) (andEL (finite (Sfun F0) ∧ (Sfun F0) ⊆ F0) (∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ (Sfun F0)) (HSfunSpec F0 HF0small))).
An exact proof term for the current goal is (finite_Repl (Sfun F0) HSfin (λb0 : set ⇒ (idx F0,b0))).
We prove the intermediate claim HJneedFin: finite Jneed.
We prove the intermediate claim HJneedDef: Jneed = ⋃ Jfam.
Use reflexivity.
rewrite the current goal using HJneedDef (from left to right).
An exact proof term for the current goal is (finite_Union_of_finite_family Jfam HJfamFin HJfamAllFin).
We prove the intermediate claim HJneedSubJ: Jneed ⊆ J.
Let j0 be given.
Assume Hj0: j0 ∈ Jneed.
We prove the intermediate claim Hj0U: j0 ∈ ⋃ Jfam.
We prove the intermediate claim HJneedDef0: Jneed = ⋃ Jfam.
Use reflexivity.
rewrite the current goal using HJneedDef0 (from right to left).
An exact proof term for the current goal is Hj0.
Apply (UnionE_impred Jfam j0 Hj0U) to the current goal.
Let A be given.
Assume Hj0A: j0 ∈ A.
Assume HA: A ∈ Jfam.
Apply (ReplE_impred FamsSmall Jsel A HA (j0 ∈ J)) to the current goal.
Let F0 be given.
Assume HF0small: F0 ∈ FamsSmall.
Assume HAeq: A = Jsel F0.
We prove the intermediate claim Hj0A0: j0 ∈ Jsel F0.
rewrite the current goal using HAeq (from right to left).
An exact proof term for the current goal is Hj0A.
Apply (ReplE_impred (Sfun F0) (λb0 : set ⇒ (idx F0,b0)) j0 Hj0A0 (j0 ∈ J)) to the current goal.
Let b0 be given.
Assume Hb0S: b0 ∈ Sfun F0.
Assume Hj0eq: j0 = (idx F0,b0).
rewrite the current goal using Hj0eq (from left to right).
We prove the intermediate claim HF0Fams: F0 ∈ Fams.
An exact proof term for the current goal is (SepE1 Fams (λF1 : set ⇒ idx F1 ∈ ordsucc N0) F0 HF0small).
We prove the intermediate claim HidxF0O: idx F0 ∈ ω.
An exact proof term for the current goal is (Hidx_to_omega F0 HF0Fams).
We prove the intermediate claim Hb0F0: b0 ∈ F0.
We prove the intermediate claim HSleft0: finite (Sfun F0) ∧ (Sfun F0) ⊆ F0.
An exact proof term for the current goal is (andEL (finite (Sfun F0) ∧ (Sfun F0) ⊆ F0) (∀b : set, b ∈ F0 → b ∩ Vsmall ≠ Empty → b ∈ (Sfun F0)) (HSfunSpec F0 HF0small)).
We prove the intermediate claim HSsub: (Sfun F0) ⊆ F0.
An exact proof term for the current goal is (andER (finite (Sfun F0)) ((Sfun F0) ⊆ F0) HSleft0).
An exact proof term for the current goal is (HSsub b0 Hb0S).
We prove the intermediate claim Hb0B: b0 ∈ B.
We prove the intermediate claim HBdef: B = ⋃ Fams.
Use reflexivity.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is (UnionI Fams b0 F0 Hb0F0 HF0Fams).
We prove the intermediate claim Hj0prod: (idx F0,b0) ∈ setprod ω B.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω B (idx F0) b0 HidxF0O Hb0B).
We prove the intermediate claim HJdef0: J = {p ∈ setprod ω B|∃F1 : set, (F1 ∈ Fams ∧ idx F1 = (p 0) ∧ (p 1) ∈ F1)}.
Use reflexivity.
rewrite the current goal using HJdef0 (from left to right).
Apply (SepI (setprod ω B) (λp : set ⇒ ∃F1 : set, (F1 ∈ Fams ∧ idx F1 = (p 0) ∧ (p 1) ∈ F1)) (idx F0,b0)) to the current goal.
An exact proof term for the current goal is Hj0prod.
We use F0 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 HF0Fams.
We prove the intermediate claim Hp0: (idx F0,b0) 0 = idx F0.
An exact proof term for the current goal is (tuple_2_0_eq (idx F0) b0).
rewrite the current goal using Hp0 (from left to right).
Use reflexivity.
We prove the intermediate claim Hp1: (idx F0,b0) 1 = b0.
An exact proof term for the current goal is (tuple_2_1_eq (idx F0) b0).
rewrite the current goal using Hp1 (from left to right).
An exact proof term for the current goal is Hb0F0.
We prove the intermediate claim HcontF: ∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0).
An exact proof term for the current goal is (andER (topology_on X Tx ∧ total_function_on F J (function_space X R)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepABC).
Set Ij to be the term λj0 : set ⇒ ({t ∈ R|Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) t} ∩ {t ∈ R|Rlt t (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3)}).
We prove the intermediate claim HIjOpen: ∀j0 : set, j0 ∈ Jneed → (Ij j0) ∈ R_standard_topology.
Let j0 be given.
Assume Hj0N: j0 ∈ Jneed.
We prove the intermediate claim Hj0J: j0 ∈ J.
An exact proof term for the current goal is (HJneedSubJ j0 Hj0N).
We prove the intermediate claim HcR: apply_fun (apply_fun Fmap y) j0 ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J (apply_fun Fmap y) j0 Hj0J HfyY).
We prove the intermediate claim HlowR: add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun (apply_fun Fmap y) j0) HcR (minus_SNo eps3) (real_minus_SNo eps3 Heps3R)).
We prove the intermediate claim HupR: add_SNo (apply_fun (apply_fun Fmap y) j0) eps3 ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun (apply_fun Fmap y) j0) HcR eps3 Heps3R).
We prove the intermediate claim HUlow: {t ∈ R|Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) t} ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_in_R_standard_topology (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) HlowR).
We prove the intermediate claim HUup: {t ∈ R|Rlt t (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3)} ∈ R_standard_topology.
An exact proof term for the current goal is (open_left_ray_in_R_standard_topology (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3) HupR).
We prove the intermediate claim HIeq: Ij j0 = ({t ∈ R|Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) t} ∩ {t ∈ R|Rlt t (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3)}).
Use reflexivity.
rewrite the current goal using HIeq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed R R_standard_topology {t ∈ R|Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) t} {t ∈ R|Rlt t (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3)} R_standard_topology_is_topology HUlow HUup).
Set Nj to be the term λj0 : set ⇒ preimage_of X (apply_fun F j0) (Ij j0).
Set Cfam to be the term {Nj j0|j0 ∈ Jneed}.
Set Vcont to be the term intersection_of_family X Cfam.
Set V to be the term Vsmall ∩ Vcont.
We prove the intermediate claim HCfamFin: finite Cfam.
An exact proof term for the current goal is (finite_Repl Jneed HJneedFin Nj).
We prove the intermediate claim HCfamSubTx: Cfam ⊆ Tx.
Let U be given.
Assume HU: U ∈ Cfam.
Apply (ReplE_impred Jneed Nj U HU (U ∈ Tx)) to the current goal.
Let j0 be given.
Assume Hj0N: j0 ∈ Jneed.
Assume HUeq: U = Nj j0.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim Hj0J: j0 ∈ J.
An exact proof term for the current goal is (HJneedSubJ j0 Hj0N).
We prove the intermediate claim Hfjcont: continuous_map X Tx R R_standard_topology (apply_fun F j0).
An exact proof term for the current goal is (HcontF j0 Hj0J).
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology (apply_fun F j0) Hfjcont (Ij j0) (HIjOpen j0 Hj0N)).
We prove the intermediate claim HCfamPow: Cfam ∈ 𝒫 Tx.
An exact proof term for the current goal is (PowerI Tx Cfam HCfamSubTx).
We prove the intermediate claim HVcontTx: Vcont ∈ Tx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx Cfam HTx HCfamPow HCfamFin).
We prove the intermediate claim HyVcont: y ∈ Vcont.
We prove the intermediate claim HVcontDef0: Vcont = intersection_of_family X Cfam.
Use reflexivity.
rewrite the current goal using HVcontDef0 (from left to right).
We prove the intermediate claim HinterDef0: intersection_of_family X Cfam = {x ∈ X|∀U : set, U ∈ Cfam → x ∈ U}.
Use reflexivity.
rewrite the current goal using HinterDef0 (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HyX.
Let U be given.
Assume HU: U ∈ Cfam.
Apply (ReplE_impred Jneed Nj U HU (y ∈ U)) to the current goal.
Let j0 be given.
Assume Hj0N: j0 ∈ Jneed.
Assume HUeq: U = Nj j0.
rewrite the current goal using HUeq (from left to right).
We will prove y ∈ preimage_of X (apply_fun F j0) (Ij j0).
We prove the intermediate claim HpreDef0: preimage_of X (apply_fun F j0) (Ij j0) = {x ∈ X|apply_fun (apply_fun F j0) x ∈ (Ij j0)}.
Use reflexivity.
rewrite the current goal using HpreDef0 (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HyX.
We prove the intermediate claim Hj0J: j0 ∈ J.
An exact proof term for the current goal is (HJneedSubJ j0 Hj0N).
We prove the intermediate claim HcEq: apply_fun (apply_fun F j0) y = apply_fun (apply_fun Fmap y) j0.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
Use symmetry.
An exact proof term for the current goal is (diagonal_map_coord_apply X F J y j0 HyX Hj0J).
We prove the intermediate claim HcR: apply_fun (apply_fun Fmap y) j0 ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J (apply_fun Fmap y) j0 Hj0J HfyY).
We prove the intermediate claim HvalR: apply_fun (apply_fun F j0) y ∈ R.
We prove the intermediate claim HFtopTot: topology_on X Tx ∧ total_function_on F J (function_space X R).
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ total_function_on F J (function_space X R)) (∀j1 : set, j1 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j1)) HsepABC).
We prove the intermediate claim HFtot: total_function_on F J (function_space X R).
An exact proof term for the current goal is (andER (topology_on X Tx) (total_function_on F J (function_space X R)) HFtopTot).
We prove the intermediate claim HFon: function_on F J (function_space X R).
An exact proof term for the current goal is (total_function_on_function_on F J (function_space X R) HFtot).
We prove the intermediate claim HFj0FS: apply_fun F j0 ∈ function_space X R.
An exact proof term for the current goal is (HFon j0 Hj0J).
We prove the intermediate claim HFj0on: function_on (apply_fun F j0) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun F j0) X R HFj0FS).
An exact proof term for the current goal is (HFj0on y HyX).
We prove the intermediate claim Heps3posS: 0 < eps3.
An exact proof term for the current goal is (SNo_eps_pos (ordsucc (ordsucc N1)) Heps3O).
We prove the intermediate claim Heps3pos: Rlt 0 eps3.
An exact proof term for the current goal is (RltI 0 eps3 real_0 Heps3R Heps3posS).
We prove the intermediate claim HlowLt: Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) (apply_fun (apply_fun Fmap y) j0).
We prove the intermediate claim HmEpsLt0: minus_SNo eps3 < 0.
We prove the intermediate claim HmEpsLt0tmp: minus_SNo eps3 < minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 eps3 SNo_0 Heps3S Heps3posS).
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is HmEpsLt0tmp.
We prove the intermediate claim HmEpsLt0R: Rlt (minus_SNo eps3) 0.
An exact proof term for the current goal is (RltI (minus_SNo eps3) 0 (real_minus_SNo eps3 Heps3R) real_0 HmEpsLt0).
We prove the intermediate claim HsumLt: Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) (apply_fun (apply_fun Fmap y) j0).
We prove the intermediate claim HaS: SNo (apply_fun (apply_fun Fmap y) j0).
An exact proof term for the current goal is (real_SNo (apply_fun (apply_fun Fmap y) j0) HcR).
We prove the intermediate claim HltS: add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3) < add_SNo (apply_fun (apply_fun Fmap y) j0) 0.
An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3) 0 HaS (SNo_minus_SNo eps3 Heps3S) SNo_0 HmEpsLt0).
We prove the intermediate claim HltR: Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) (add_SNo (apply_fun (apply_fun Fmap y) j0) 0).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) (add_SNo (apply_fun (apply_fun Fmap y) j0) 0) (real_add_SNo (apply_fun (apply_fun Fmap y) j0) HcR (minus_SNo eps3) (real_minus_SNo eps3 Heps3R)) (real_add_SNo (apply_fun (apply_fun Fmap y) j0) HcR 0 real_0) HltS).
We prove the intermediate claim H0eq: add_SNo (apply_fun (apply_fun Fmap y) j0) 0 = apply_fun (apply_fun Fmap y) j0.
An exact proof term for the current goal is (add_SNo_0R (apply_fun (apply_fun Fmap y) j0) HaS).
rewrite the current goal using H0eq (from right to left) at position 2.
An exact proof term for the current goal is HltR.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim HupGt: Rlt (apply_fun (apply_fun Fmap y) j0) (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3).
An exact proof term for the current goal is (RltI (apply_fun (apply_fun Fmap y) j0) (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3) HcR (real_add_SNo (apply_fun (apply_fun Fmap y) j0) HcR eps3 Heps3R) (add_SNo_eps_Lt (apply_fun (apply_fun Fmap y) j0) (real_SNo (apply_fun (apply_fun Fmap y) j0) HcR) (ordsucc (ordsucc N1)) Heps3O)).
We prove the intermediate claim HlowVal: Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) (apply_fun (apply_fun F j0) y).
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is HlowLt.
We prove the intermediate claim HupVal: Rlt (apply_fun (apply_fun F j0) y) (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3).
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is HupGt.
We prove the intermediate claim HIjDef1: Ij j0 = ({t ∈ R|Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) t} ∩ {t ∈ R|Rlt t (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3)}).
Use reflexivity.
rewrite the current goal using HIjDef1 (from left to right).
We prove the intermediate claim HlowMem: apply_fun (apply_fun F j0) y ∈ {t ∈ R|Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) t}.
Apply SepI to the current goal.
An exact proof term for the current goal is HvalR.
An exact proof term for the current goal is HlowVal.
We prove the intermediate claim HupMem: apply_fun (apply_fun F j0) y ∈ {t ∈ R|Rlt t (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3)}.
Apply SepI to the current goal.
An exact proof term for the current goal is HvalR.
An exact proof term for the current goal is HupVal.
An exact proof term for the current goal is (binintersectI {t ∈ R|Rlt (add_SNo (apply_fun (apply_fun Fmap y) j0) (minus_SNo eps3)) t} {t ∈ R|Rlt t (add_SNo (apply_fun (apply_fun Fmap y) j0) eps3)} (apply_fun (apply_fun F j0) y) HlowMem HupMem).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx Vsmall Vcont HTx HVsmallTx HVcontTx).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (binintersectI Vsmall Vcont y HyVsmall HyVcont).
We prove the intermediate claim HctrlBall: ∀z : set, z ∈ V → Rlt (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) d.
Let z be given.
Assume HzV: z ∈ V.
We prove the intermediate claim HzVsmall: z ∈ Vsmall.
An exact proof term for the current goal is (binintersectE1 Vsmall Vcont z HzV).
We prove the intermediate claim HzVcont: z ∈ Vcont.
An exact proof term for the current goal is (binintersectE2 Vsmall Vcont z HzV).
We will prove Rlt (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) d.
We prove the intermediate claim HzX: z ∈ X.
We prove the intermediate claim HVsubX: Vsmall ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx Vsmall HTx HVsmallTx).
An exact proof term for the current goal is (HVsubX z HzVsmall).
We prove the intermediate claim HfzY: apply_fun Fmap z ∈ power_real J.
An exact proof term for the current goal is (HFmapfun z HzX).
Set fy to be the term apply_fun Fmap y.
Set fz to be the term apply_fun Fmap z.
We prove the intermediate claim HfyY0: fy ∈ power_real J.
An exact proof term for the current goal is HfyY.
We prove the intermediate claim HfzY0: fz ∈ power_real J.
An exact proof term for the current goal is HfzY.
We prove the intermediate claim HdYdef: dY = uniform_metric_power_real J.
Use reflexivity.
We prove the intermediate claim HdYapp: apply_fun dY (fy,fz) = power_real_uniform_metric_value J fy fz.
rewrite the current goal using HdYdef (from left to right).
An exact proof term for the current goal is (uniform_metric_power_real_apply J fy fz HfyY0 HfzY0).
We prove the intermediate claim HyEq: apply_fun dY (apply_fun Fmap y,apply_fun Fmap z) = apply_fun dY (fy,fz).
Use reflexivity.
rewrite the current goal using HyEq (from left to right).
rewrite the current goal using HdYapp (from left to right).
Set val to be the term power_real_uniform_metric_value J fy fz.
Set A to be the term power_real_clipped_diffs J fy fz.
We prove the intermediate claim Hlub: R_lub A val.
An exact proof term for the current goal is (power_real_uniform_metric_value_is_lub J fy fz HJne HfyY0 HfzY0).
We prove the intermediate claim Hmin: ∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle val u.
An exact proof term for the current goal is (andER (val ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a val) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle val u) Hlub).
We prove the intermediate claim Hexu: ∃u : set, u ∈ R ∧ Rlt u d ∧ ∀a : set, a ∈ A → a ∈ R → Rle a u.
We prove the intermediate claim Hub_u0: ∀a : set, a ∈ A → a ∈ R → Rle a u0.
Let a be given.
Assume HaA: a ∈ A.
Assume HaR: a ∈ R.
Apply (ReplE_impred J (λj0 : set ⇒ power_real_coord_clipped_diff fy fz j0) a HaA (Rle a u0)) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
Assume Haj: a = power_real_coord_clipped_diff fy fz j.
rewrite the current goal using Haj (from left to right).
Set n to be the term j 0.
Set b to be the term j 1.
We prove the intermediate claim Hjprod: j ∈ setprod ω B.
An exact proof term for the current goal is (SepE1 (setprod ω B) (λq : set ⇒ ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (q 0) ∧ (q 1) ∈ F0) j HjJ).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ B) j Hjprod).
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (ap1_Sigma ω (λ_ : set ⇒ B) j Hjprod).
We prove the intermediate claim HsuccNO: ordsucc N0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N0 HN0O).
We prove the intermediate claim Hordn: ordinal n.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n HnO).
We prove the intermediate claim HordSuccN0: ordinal (ordsucc N0).
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal (ordsucc N0) HsuccNO).
We prove the intermediate claim Hlarge: N0 ∈ n → Rle (power_real_coord_clipped_diff fy fz j) u0.
Assume HN0in: N0 ∈ n.
Set invn to be the term inv_nat (ordsucc n).
We prove the intermediate claim HsuccnO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HinvR: invn ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) HsuccnO).
We prove the intermediate claim HinvS: SNo invn.
An exact proof term for the current goal is (real_SNo invn HinvR).
We prove the intermediate claim HinvPos: Rlt 0 invn.
We prove the intermediate claim HsuccnNot0: ordsucc n ≠ 0.
An exact proof term for the current goal is (neq_ordsucc_0 n).
We prove the intermediate claim HsuccnNotIn0: ordsucc n ∉ {0}.
Assume Hs0: ordsucc n ∈ {0}.
An exact proof term for the current goal is (HsuccnNot0 (SingE 0 (ordsucc n) Hs0)).
We prove the intermediate claim HsuccnIn: ordsucc n ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc n) HsuccnO HsuccnNotIn0).
An exact proof term for the current goal is (inv_nat_pos (ordsucc n) HsuccnIn).
We prove the intermediate claim HinvNN: 0 ≤ invn.
An exact proof term for the current goal is (SNoLtLe 0 invn (RltE_lt 0 invn HinvPos)).
We prove the intermediate claim HinvN0R0: invN0 ∈ R.
An exact proof term for the current goal is HinvN0R.
We prove the intermediate claim HinvN0S0: SNo invN0.
An exact proof term for the current goal is HinvN0S.
We prove the intermediate claim HinvLt: Rlt invn invN0.
An exact proof term for the current goal is (inv_nat_ordsucc_antitone_local2 N0 n HN0O HnO HN0in).
We prove the intermediate claim HinvLeInvN0: Rle invn invN0.
An exact proof term for the current goal is (RleI invn invN0 HinvR HinvN0R0 (not_Rlt_sym invn invN0 HinvLt)).
We prove the intermediate claim HinvN0LtU0: Rlt invN0 u0.
We prove the intermediate claim HltS: invN0 < u0.
An exact proof term for the current goal is (add_SNo_eps_Lt invN0 HinvN0S0 N1 HN1O).
An exact proof term for the current goal is (RltI invN0 u0 HinvN0R0 Hu0R HltS).
We prove the intermediate claim HinvN0LeU0: Rle invN0 u0.
An exact proof term for the current goal is (RleI invN0 u0 HinvN0R0 Hu0R (not_Rlt_sym invN0 u0 HinvN0LtU0)).
We prove the intermediate claim HinvLeU0: Rle invn u0.
An exact proof term for the current goal is (Rle_tra invn invN0 u0 HinvLeInvN0 HinvN0LeU0).
We prove the intermediate claim HcoordEqy: apply_fun fy j = apply_fun (apply_fun F j) y.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J y j HyX HjJ).
We prove the intermediate claim HcoordEqz: apply_fun fz j = apply_fun (apply_fun F j) z.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J z j HzX HjJ).
We prove the intermediate claim HbdEq: power_real_coord_clipped_diff fy fz j = R_bounded_distance (apply_fun (apply_fun F j) y) (apply_fun (apply_fun F j) z).
We prove the intermediate claim Htmp: power_real_coord_clipped_diff fy fz j = R_bounded_distance (apply_fun fy j) (apply_fun fz j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J fy fz j HjJ HfyY0 HfzY0).
rewrite the current goal using Htmp (from left to right).
rewrite the current goal using HcoordEqy (from left to right).
rewrite the current goal using HcoordEqz (from left to right).
Use reflexivity.
rewrite the current goal using HbdEq (from left to right).
Set sy to be the term apply_fun (apply_fun F j) y.
Set sz to be the term apply_fun (apply_fun F j) z.
We prove the intermediate claim HsyR: sy ∈ R.
rewrite the current goal using HcoordEqy (from right to left).
An exact proof term for the current goal is (power_real_coord_in_R J fy j HjJ HfyY0).
We prove the intermediate claim HszR: sz ∈ R.
rewrite the current goal using HcoordEqz (from right to left).
An exact proof term for the current goal is (power_real_coord_in_R J fz j HjJ HfzY0).
Set t to be the term add_SNo sy (minus_SNo sz).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (real_add_SNo sy HsyR (minus_SNo sz) (real_minus_SNo sz HszR)).
We prove the intermediate claim HabsR: abs_SNo t ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R t HtR).
We prove the intermediate claim HbdLeAbs: Rle (R_bounded_distance sy sz) (abs_SNo t).
We prove the intermediate claim Hbddef: R_bounded_distance sy sz = if (Rlt (abs_SNo t) 1) then (abs_SNo t) else 1.
Use reflexivity.
Apply (xm (Rlt (abs_SNo t) 1) (Rle (R_bounded_distance sy sz) (abs_SNo t))) to the current goal.
Assume Hlt: Rlt (abs_SNo t) 1.
rewrite the current goal using Hbddef (from left to right).
We prove the intermediate claim Hif: (if (Rlt (abs_SNo t) 1) then (abs_SNo t) else 1) = (abs_SNo t).
An exact proof term for the current goal is (If_i_1 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hlt).
rewrite the current goal using Hif (from left to right).
An exact proof term for the current goal is (RleI (abs_SNo t) (abs_SNo t) HabsR HabsR (not_Rlt_refl (abs_SNo t) HabsR)).
Assume Hnlt: ¬ (Rlt (abs_SNo t) 1).
rewrite the current goal using Hbddef (from left to right).
We prove the intermediate claim Hif: (if (Rlt (abs_SNo t) 1) then (abs_SNo t) else 1) = 1.
An exact proof term for the current goal is (If_i_0 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hnlt).
rewrite the current goal using Hif (from left to right).
An exact proof term for the current goal is (RleI 1 (abs_SNo t) real_1 HabsR Hnlt).
We prove the intermediate claim HabsLeInv: Rle (abs_SNo t) invn.
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBopen b HbB).
We prove the intermediate claim Hexb0: ∃f0 : set, continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x)).
An exact proof term for the current goal is (open_set_has_positive_support_function_unit_interval X Tx b Hnorm HclosedG HbTx).
Set P to be the term (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x))).
We prove the intermediate claim HPb: P (bump0 b).
An exact proof term for the current goal is (Eps_i_ex P Hexb0).
We prove the intermediate claim Hb0c0: continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HPb).
We prove the intermediate claim Hb0cont: continuous_map X Tx unit_interval unit_interval_topology (bump0 b).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0c0).
We prove the intermediate claim Hb0fun: function_on (bump0 b) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (bump0 b) Hb0cont).
Set u to be the term apply_fun (bump0 b) y.
Set v to be the term apply_fun (bump0 b) z.
We prove the intermediate claim HuI: u ∈ unit_interval.
An exact proof term for the current goal is (Hb0fun y HyX).
We prove the intermediate claim HvI: v ∈ unit_interval.
An exact proof term for the current goal is (Hb0fun z HzX).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R u HuI).
We prove the intermediate claim HvR: v ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R v HvI).
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 HvS: SNo v.
An exact proof term for the current goal is (real_SNo v HvR).
We prove the intermediate claim HuProp: ¬ (Rlt u 0) ∧ ¬ (Rlt 1 u).
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) u HuI).
We prove the intermediate claim HvProp: ¬ (Rlt v 0) ∧ ¬ (Rlt 1 v).
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) v HvI).
We prove the intermediate claim Hnotu0: ¬ (Rlt u 0).
An exact proof term for the current goal is (andEL (¬ (Rlt u 0)) (¬ (Rlt 1 u)) HuProp).
We prove the intermediate claim Hnot1u: ¬ (Rlt 1 u).
An exact proof term for the current goal is (andER (¬ (Rlt u 0)) (¬ (Rlt 1 u)) HuProp).
We prove the intermediate claim Hnotv0: ¬ (Rlt v 0).
An exact proof term for the current goal is (andEL (¬ (Rlt v 0)) (¬ (Rlt 1 v)) HvProp).
We prove the intermediate claim Hnot1v: ¬ (Rlt 1 v).
An exact proof term for the current goal is (andER (¬ (Rlt v 0)) (¬ (Rlt 1 v)) HvProp).
We prove the intermediate claim H0leuR: Rle 0 u.
An exact proof term for the current goal is (RleI 0 u real_0 HuR Hnotu0).
We prove the intermediate claim HuLe1R: Rle u 1.
An exact proof term for the current goal is (RleI u 1 HuR real_1 Hnot1u).
We prove the intermediate claim H0levR: Rle 0 v.
An exact proof term for the current goal is (RleI 0 v real_0 HvR Hnotv0).
We prove the intermediate claim HvLe1R: Rle v 1.
An exact proof term for the current goal is (RleI v 1 HvR real_1 Hnot1v).
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 HuLe1: u ≤ 1.
An exact proof term for the current goal is (SNoLe_of_Rle u 1 HuLe1R).
We prove the intermediate claim H0lev: 0 ≤ v.
An exact proof term for the current goal is (SNoLe_of_Rle 0 v H0levR).
We prove the intermediate claim HvLe1: v ≤ 1.
An exact proof term for the current goal is (SNoLe_of_Rle v 1 HvLe1R).
Set delta to be the term add_SNo u (minus_SNo v).
We prove the intermediate claim HdeltaDef: delta = add_SNo u (minus_SNo v).
Use reflexivity.
We prove the intermediate claim HmvS: SNo (minus_SNo v).
An exact proof term for the current goal is (SNo_minus_SNo v HvS).
We prove the intermediate claim HdeltaS: SNo delta.
rewrite the current goal using HdeltaDef (from left to right).
An exact proof term for the current goal is (SNo_add_SNo u (minus_SNo v) HuS HmvS).
We prove the intermediate claim HmvLe0: minus_SNo v ≤ 0.
We prove the intermediate claim HmvLe0R: Rle (minus_SNo v) 0.
An exact proof term for the current goal is (Rle_minus_nonneg v HvR Hnotv0).
An exact proof term for the current goal is (SNoLe_of_Rle (minus_SNo v) 0 HmvLe0R).
We prove the intermediate claim HdeltaLeU: delta ≤ u.
rewrite the current goal using HdeltaDef (from left to right).
We prove the intermediate claim Hu0: add_SNo u 0 = u.
An exact proof term for the current goal is (add_SNo_0R u HuS).
rewrite the current goal using Hu0 (from right to left) at position 2.
An exact proof term for the current goal is (add_SNo_Le2 u (minus_SNo v) 0 HuS HmvS SNo_0 HmvLe0).
We prove the intermediate claim HdeltaLe1: delta ≤ 1.
An exact proof term for the current goal is (SNoLe_tra delta u 1 HdeltaS HuS SNo_1 HdeltaLeU HuLe1).
We prove the intermediate claim Hm1LeMv: minus_SNo 1 ≤ minus_SNo v.
An exact proof term for the current goal is (minus_SNo_Le_contra v 1 HvS SNo_1 HvLe1).
We prove the intermediate claim HmvLeDelta: minus_SNo v ≤ delta.
rewrite the current goal using HdeltaDef (from left to right).
We prove the intermediate claim HmvLe: minus_SNo v ≤ add_SNo (minus_SNo v) u.
An exact proof term for the current goal is (SNoLe_add_nonneg_right (minus_SNo v) u HmvS HuS H0leu).
We prove the intermediate claim Hcomuv: add_SNo u (minus_SNo v) = add_SNo (minus_SNo v) u.
An exact proof term for the current goal is (add_SNo_com u (minus_SNo v) HuS HmvS).
rewrite the current goal using Hcomuv (from left to right).
An exact proof term for the current goal is HmvLe.
We prove the intermediate claim Hm1LeDelta: minus_SNo 1 ≤ delta.
An exact proof term for the current goal is (SNoLe_tra (minus_SNo 1) (minus_SNo v) delta (SNo_minus_SNo 1 SNo_1) HmvS HdeltaS Hm1LeMv HmvLeDelta).
We prove the intermediate claim HabsDeltaLe1: abs_SNo delta ≤ 1.
An exact proof term for the current goal is (abs_SNo_Le_of_bounds delta 1 HdeltaS SNo_1 Hm1LeDelta HdeltaLe1).
We prove the intermediate claim HtEq1: t = add_SNo sy (minus_SNo sz).
Use reflexivity.
We prove the intermediate claim HbumpDef: bump b = graph X (λx0 : set ⇒ apply_fun (bump0 b) x0).
Use reflexivity.
We prove the intermediate claim Hybump: apply_fun (bump b) y = u.
rewrite the current goal using HbumpDef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun (bump0 b) x0) y HyX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hzbump: apply_fun (bump b) z = v.
rewrite the current goal using HbumpDef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun (bump0 b) x0) z HzX) (from left to right).
Use reflexivity.
We prove the intermediate claim HFdef: F = graph J (λp : set ⇒ bump_scaled (p 0) (p 1)).
Use reflexivity.
We prove the intermediate claim HappF: apply_fun F j = bump_scaled (j 0) (j 1).
rewrite the current goal using HFdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph J (λp : set ⇒ bump_scaled (p 0) (p 1)) j HjJ).
We prove the intermediate claim HinvnDef: invn = inv_nat (ordsucc n).
Use reflexivity.
We prove the intermediate claim HsyDef: sy = apply_fun (apply_fun F j) y.
Use reflexivity.
We prove the intermediate claim HszDef: sz = apply_fun (apply_fun F j) z.
Use reflexivity.
We prove the intermediate claim HsyEq: sy = mul_SNo u invn.
rewrite the current goal using HsyDef (from left to right).
rewrite the current goal using HappF (from left to right).
We prove the intermediate claim HbscDef: bump_scaled n b = compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n))).
Use reflexivity.
rewrite the current goal using HbscDef (from left to right).
We prove the intermediate claim Hcomp: apply_fun (compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n)))) y = apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) y).
An exact proof term for the current goal is (compose_fun_apply X (bump b) (mul_const_fun (inv_nat (ordsucc n))) y HyX).
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using Hybump (from left to right).
rewrite the current goal using HinvnDef (from right to left).
We prove the intermediate claim Hmc: apply_fun (mul_const_fun invn) u = mul_SNo u invn.
An exact proof term for the current goal is (mul_const_fun_apply invn u HinvR HuR).
rewrite the current goal using Hmc (from left to right).
Use reflexivity.
We prove the intermediate claim HszEq: sz = mul_SNo v invn.
rewrite the current goal using HszDef (from left to right).
rewrite the current goal using HappF (from left to right).
We prove the intermediate claim HbscDef: bump_scaled n b = compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n))).
Use reflexivity.
rewrite the current goal using HbscDef (from left to right).
We prove the intermediate claim Hcomp: apply_fun (compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n)))) z = apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) z).
An exact proof term for the current goal is (compose_fun_apply X (bump b) (mul_const_fun (inv_nat (ordsucc n))) z HzX).
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using Hzbump (from left to right).
rewrite the current goal using HinvnDef (from right to left).
We prove the intermediate claim Hmc: apply_fun (mul_const_fun invn) v = mul_SNo v invn.
An exact proof term for the current goal is (mul_const_fun_apply invn v HinvR HvR).
rewrite the current goal using Hmc (from left to right).
Use reflexivity.
We prove the intermediate claim HtEq2: t = mul_SNo delta invn.
rewrite the current goal using HtEq1 (from left to right).
rewrite the current goal using HsyEq (from left to right).
rewrite the current goal using HszEq (from left to right).
We prove the intermediate claim HmSz: minus_SNo (mul_SNo v invn) = mul_SNo (minus_SNo v) invn.
We prove the intermediate claim Hc1: mul_SNo v invn = mul_SNo invn v.
An exact proof term for the current goal is (mul_SNo_com v invn HvS HinvS).
We prove the intermediate claim Hc2: mul_SNo (minus_SNo v) invn = mul_SNo invn (minus_SNo v).
An exact proof term for the current goal is (mul_SNo_com (minus_SNo v) invn HmvS HinvS).
We prove the intermediate claim Hmd: mul_SNo invn (minus_SNo v) = minus_SNo (mul_SNo invn v).
An exact proof term for the current goal is (mul_SNo_minus_distrR invn v HinvS HvS).
rewrite the current goal using Hc1 (from left to right).
rewrite the current goal using Hc2 (from left to right).
rewrite the current goal using Hmd (from right to left).
Use reflexivity.
rewrite the current goal using HmSz (from left to right).
We prove the intermediate claim Hdistr: mul_SNo (add_SNo u (minus_SNo v)) invn = add_SNo (mul_SNo u invn) (mul_SNo (minus_SNo v) invn).
An exact proof term for the current goal is (mul_SNo_distrR u (minus_SNo v) invn HuS HmvS HinvS).
rewrite the current goal using Hdistr (from right to left).
Use reflexivity.
We prove the intermediate claim HabstLe: abs_SNo t ≤ invn.
rewrite the current goal using HtEq2 (from left to right).
We prove the intermediate claim HabsMul: abs_SNo (mul_SNo delta invn) = mul_SNo (abs_SNo delta) (abs_SNo invn).
An exact proof term for the current goal is (abs_SNo_mul_eq delta invn HdeltaS HinvS).
rewrite the current goal using HabsMul (from left to right).
We prove the intermediate claim HabsInv: abs_SNo invn = invn.
An exact proof term for the current goal is (nonneg_abs_SNo invn HinvNN).
rewrite the current goal using HabsInv (from left to right) at position 1.
We prove the intermediate claim HabsDeltaS: SNo (abs_SNo delta).
An exact proof term for the current goal is (SNo_abs_SNo delta HdeltaS).
We prove the intermediate claim HmulLe: mul_SNo (abs_SNo delta) invn ≤ mul_SNo 1 invn.
An exact proof term for the current goal is (nonneg_mul_SNo_Le' (abs_SNo delta) 1 invn HabsDeltaS SNo_1 HinvS HinvNN HabsDeltaLe1).
We prove the intermediate claim Hone: mul_SNo 1 invn = invn.
An exact proof term for the current goal is (mul_SNo_oneL invn HinvS).
rewrite the current goal using Hone (from right to left) at position 2.
An exact proof term for the current goal is HmulLe.
An exact proof term for the current goal is (Rle_of_SNoLe (abs_SNo t) invn HabsR HinvR HabstLe).
We prove the intermediate claim HbdLeInv: Rle (R_bounded_distance sy sz) invn.
An exact proof term for the current goal is (Rle_tra (R_bounded_distance sy sz) (abs_SNo t) invn HbdLeAbs HabsLeInv).
An exact proof term for the current goal is (Rle_tra (R_bounded_distance sy sz) invn u0 HbdLeInv HinvLeU0).
Apply (ordinal_trichotomy_or_impred n (ordsucc N0) Hordn HordSuccN0 (Rle (power_real_coord_clipped_diff fy fz j) u0)) to the current goal.
Assume HnSmall: n ∈ ordsucc N0.
We prove the intermediate claim HjInfo: ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (j 0) ∧ (j 1) ∈ F0.
An exact proof term for the current goal is (SepE2 (setprod ω B) (λq : set ⇒ ∃F0 : set, F0 ∈ Fams ∧ idx F0 = (q 0) ∧ (q 1) ∈ F0) j HjJ).
Apply HjInfo to the current goal.
Let F0 be given.
Assume HF0pack.
We prove the intermediate claim HF0left: F0 ∈ Fams ∧ idx F0 = (j 0).
An exact proof term for the current goal is (andEL (F0 ∈ Fams ∧ idx F0 = (j 0)) ((j 1) ∈ F0) HF0pack).
We prove the intermediate claim HF0Fams: F0 ∈ Fams.
An exact proof term for the current goal is (andEL (F0 ∈ Fams) (idx F0 = (j 0)) HF0left).
We prove the intermediate claim HidxEq0: idx F0 = (j 0).
An exact proof term for the current goal is (andER (F0 ∈ Fams) (idx F0 = (j 0)) HF0left).
We prove the intermediate claim HbF0_0: (j 1) ∈ F0.
An exact proof term for the current goal is (andER (F0 ∈ Fams ∧ idx F0 = (j 0)) ((j 1) ∈ F0) HF0pack).
We prove the intermediate claim HnDef: n = j 0.
Use reflexivity.
We prove the intermediate claim HbDef: b = j 1.
Use reflexivity.
We prove the intermediate claim HidxEq: idx F0 = n.
rewrite the current goal using HnDef (from left to right).
An exact proof term for the current goal is HidxEq0.
We prove the intermediate claim HbF0: b ∈ F0.
rewrite the current goal using HbDef (from left to right).
An exact proof term for the current goal is HbF0_0.
We prove the intermediate claim HF0small: F0 ∈ FamsSmall.
We prove the intermediate claim HsubN: {n} ⊆ ordsucc N0.
An exact proof term for the current goal is (singleton_subset n (ordsucc N0) HnSmall).
We prove the intermediate claim HsubIdx: {idx F0} ⊆ {n}.
Let x be given.
Assume Hx: x ∈ {idx F0}.
We will prove x ∈ {n}.
We prove the intermediate claim HxEqIdx: x = idx F0.
An exact proof term for the current goal is (SingE (idx F0) x Hx).
We prove the intermediate claim HxEqN: x = n.
An exact proof term for the current goal is (eq_i_tra x (idx F0) n HxEqIdx HidxEq).
rewrite the current goal using HxEqN (from left to right).
An exact proof term for the current goal is (SingI n).
We prove the intermediate claim HidxSmall: idx F0 ∈ ordsucc N0.
We prove the intermediate claim Hsub: {idx F0} ⊆ ordsucc N0.
An exact proof term for the current goal is (Subq_tra {idx F0} {n} (ordsucc N0) HsubIdx HsubN).
An exact proof term for the current goal is (Hsub (idx F0) (SingI (idx F0))).
Apply SepI to the current goal.
An exact proof term for the current goal is HF0Fams.
An exact proof term for the current goal is HidxSmall.
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ F0 ∧ ∀b0 : set, b0 ∈ F0 → b0 ∩ Vsmall ≠ Empty → b0 ∈ S.
An exact proof term for the current goal is (HVsmallLF F0 HF0small).
Apply (xm (b ∩ Vsmall = Empty)) to the current goal.
Assume HbcapEmpty: b ∩ Vsmall = Empty.
We prove the intermediate claim HyNotb: y ∉ b.
Assume Hyb: y ∈ b.
We prove the intermediate claim Hycap: y ∈ b ∩ Vsmall.
An exact proof term for the current goal is (binintersectI b Vsmall y Hyb HyVsmall).
We prove the intermediate claim HyEmpty: y ∈ Empty.
rewrite the current goal using HbcapEmpty (from right to left).
An exact proof term for the current goal is Hycap.
An exact proof term for the current goal is (EmptyE y HyEmpty).
We prove the intermediate claim HzNotb: z ∉ b.
Assume Hzb: z ∈ b.
We prove the intermediate claim Hzcap: z ∈ b ∩ Vsmall.
An exact proof term for the current goal is (binintersectI b Vsmall z Hzb HzVsmall).
We prove the intermediate claim HzEmpty: z ∈ Empty.
rewrite the current goal using HbcapEmpty (from right to left).
An exact proof term for the current goal is Hzcap.
An exact proof term for the current goal is (EmptyE z HzEmpty).
We prove the intermediate claim HyOut: y ∈ X ∖ b.
An exact proof term for the current goal is (setminusI X b y HyX HyNotb).
We prove the intermediate claim HzOut: z ∈ X ∖ b.
An exact proof term for the current goal is (setminusI X b z HzX HzNotb).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBopen b HbB).
Set P to be the term (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ b → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ b → Rlt 0 (apply_fun f0 x))).
We prove the intermediate claim Hexb0: ∃f0 : set, P f0.
An exact proof term for the current goal is (open_set_has_positive_support_function_unit_interval X Tx b Hnorm HclosedG HbTx).
We prove the intermediate claim HPb: P (bump0 b).
An exact proof term for the current goal is (Eps_i_ex P Hexb0).
We prove the intermediate claim Hb0AB: (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b) ∧ (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0)) (∀x : set, x ∈ b → Rlt 0 (apply_fun (bump0 b) x)) HPb).
We prove the intermediate claim Hb0zero: ∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0AB).
We prove the intermediate claim Hyb0: apply_fun (bump0 b) y = 0.
An exact proof term for the current goal is (Hb0zero y HyOut).
We prove the intermediate claim Hzb0: apply_fun (bump0 b) z = 0.
An exact proof term for the current goal is (Hb0zero z HzOut).
We prove the intermediate claim HappF: apply_fun F j = bump_scaled (j 0) (j 1).
We prove the intermediate claim HFdef: F = graph J (λp : set ⇒ bump_scaled (p 0) (p 1)).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph J (λp : set ⇒ bump_scaled (p 0) (p 1)) j HjJ).
We prove the intermediate claim HbscDef: bump_scaled n b = compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n))).
Use reflexivity.
We prove the intermediate claim HbumpDef: bump b = graph X (λx0 : set ⇒ apply_fun (bump0 b) x0).
Use reflexivity.
We prove the intermediate claim Hfyj: apply_fun fy j = apply_fun (apply_fun F j) y.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J y j HyX HjJ).
We prove the intermediate claim Hfzj: apply_fun fz j = apply_fun (apply_fun F j) z.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J z j HzX HjJ).
We prove the intermediate claim HfjEq: apply_fun F j = bump_scaled n b.
rewrite the current goal using HappF (from left to right).
rewrite the current goal using HnDef (from right to left) at position 1.
rewrite the current goal using HbDef (from right to left) at position 2.
Use reflexivity.
We prove the intermediate claim Hfj_y_0: apply_fun (apply_fun F j) y = 0.
rewrite the current goal using HfjEq (from left to right).
rewrite the current goal using HbscDef (from left to right).
We prove the intermediate claim Hcomp: apply_fun (compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n)))) y = apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) y).
An exact proof term for the current goal is (compose_fun_apply X (bump b) (mul_const_fun (inv_nat (ordsucc n))) y HyX).
rewrite the current goal using Hcomp (from left to right).
We prove the intermediate claim HinvR0: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) (omega_ordsucc n HnO)).
We prove the intermediate claim HinvS0: SNo (inv_nat (ordsucc n)).
An exact proof term for the current goal is (real_SNo (inv_nat (ordsucc n)) HinvR0).
We prove the intermediate claim Hb0cont: continuous_map X Tx unit_interval unit_interval_topology (bump0 b).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0AB).
We prove the intermediate claim Hb0fun: function_on (bump0 b) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (bump0 b) Hb0cont).
We prove the intermediate claim HbumpEqy: apply_fun (bump b) y = apply_fun (bump0 b) y.
rewrite the current goal using HbumpDef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun (bump0 b) x0) y HyX) (from left to right).
Use reflexivity.
We prove the intermediate claim HbumpRy: apply_fun (bump b) y ∈ R.
rewrite the current goal using HbumpEqy (from left to right).
We prove the intermediate claim HyI: apply_fun (bump0 b) y ∈ unit_interval.
An exact proof term for the current goal is (Hb0fun y HyX).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (bump0 b) y) HyI).
We prove the intermediate claim Hmul: apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) y) = mul_SNo (apply_fun (bump b) y) (inv_nat (ordsucc n)).
An exact proof term for the current goal is (mul_const_fun_apply (inv_nat (ordsucc n)) (apply_fun (bump b) y) HinvR0 HbumpRy).
rewrite the current goal using Hmul (from left to right).
rewrite the current goal using HbumpEqy (from left to right) at position 1.
rewrite the current goal using Hyb0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL (inv_nat (ordsucc n)) HinvS0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hfj_z_0: apply_fun (apply_fun F j) z = 0.
rewrite the current goal using HfjEq (from left to right).
rewrite the current goal using HbscDef (from left to right).
We prove the intermediate claim Hcomp: apply_fun (compose_fun X (bump b) (mul_const_fun (inv_nat (ordsucc n)))) z = apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) z).
An exact proof term for the current goal is (compose_fun_apply X (bump b) (mul_const_fun (inv_nat (ordsucc n))) z HzX).
rewrite the current goal using Hcomp (from left to right).
We prove the intermediate claim HinvR0: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) (omega_ordsucc n HnO)).
We prove the intermediate claim HinvS0: SNo (inv_nat (ordsucc n)).
An exact proof term for the current goal is (real_SNo (inv_nat (ordsucc n)) HinvR0).
We prove the intermediate claim Hb0cont: continuous_map X Tx unit_interval unit_interval_topology (bump0 b).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology (bump0 b)) (∀x : set, x ∈ X ∖ b → apply_fun (bump0 b) x = 0) Hb0AB).
We prove the intermediate claim Hb0fun: function_on (bump0 b) X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology (bump0 b) Hb0cont).
We prove the intermediate claim HbumpEqz: apply_fun (bump b) z = apply_fun (bump0 b) z.
rewrite the current goal using HbumpDef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun (bump0 b) x0) z HzX) (from left to right).
Use reflexivity.
We prove the intermediate claim HbumpRz: apply_fun (bump b) z ∈ R.
rewrite the current goal using HbumpEqz (from left to right).
We prove the intermediate claim HzI: apply_fun (bump0 b) z ∈ unit_interval.
An exact proof term for the current goal is (Hb0fun z HzX).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (bump0 b) z) HzI).
We prove the intermediate claim Hmul: apply_fun (mul_const_fun (inv_nat (ordsucc n))) (apply_fun (bump b) z) = mul_SNo (apply_fun (bump b) z) (inv_nat (ordsucc n)).
An exact proof term for the current goal is (mul_const_fun_apply (inv_nat (ordsucc n)) (apply_fun (bump b) z) HinvR0 HbumpRz).
rewrite the current goal using Hmul (from left to right).
rewrite the current goal using HbumpEqz (from left to right) at position 1.
rewrite the current goal using Hzb0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL (inv_nat (ordsucc n)) HinvS0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hfyj0: apply_fun fy j = 0.
rewrite the current goal using Hfyj (from left to right).
An exact proof term for the current goal is Hfj_y_0.
We prove the intermediate claim Hfzj0: apply_fun fz j = 0.
rewrite the current goal using Hfzj (from left to right).
An exact proof term for the current goal is Hfj_z_0.
We prove the intermediate claim HcdEq: power_real_coord_clipped_diff fy fz j = R_bounded_distance (apply_fun fy j) (apply_fun fz j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J fy fz j HjJ HfyY0 HfzY0).
rewrite the current goal using HcdEq (from left to right).
rewrite the current goal using Hfyj0 (from left to right).
rewrite the current goal using Hfzj0 (from left to right).
rewrite the current goal using (R_bounded_distance_self_zero 0 real_0) (from left to right).
We prove the intermediate claim HsuccN0O: ordsucc N0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N0 HN0O).
We prove the intermediate claim HsuccN0Not0: ordsucc N0 ≠ 0.
An exact proof term for the current goal is (neq_ordsucc_0 N0).
We prove the intermediate claim HsuccN0NotIn0: ordsucc N0 ∉ {0}.
Assume Hs0: ordsucc N0 ∈ {0}.
An exact proof term for the current goal is (HsuccN0Not0 (SingE 0 (ordsucc N0) Hs0)).
We prove the intermediate claim HsuccN0In: ordsucc N0 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc N0) HsuccN0O HsuccN0NotIn0).
We prove the intermediate claim HinvN0Pos: Rlt 0 invN0.
An exact proof term for the current goal is (inv_nat_pos (ordsucc N0) HsuccN0In).
We prove the intermediate claim HinvN0PosS: 0 < invN0.
An exact proof term for the current goal is (RltE_lt 0 invN0 HinvN0Pos).
We prove the intermediate claim Heps1PosS: 0 < eps1.
We prove the intermediate claim Heps1Def: eps1 = eps_ N1.
Use reflexivity.
rewrite the current goal using Heps1Def (from left to right).
An exact proof term for the current goal is (SNo_eps_pos N1 HN1O).
We prove the intermediate claim H0LtU0S: 0 < u0.
We prove the intermediate claim Hu0Def: u0 = add_SNo invN0 eps1.
Use reflexivity.
We prove the intermediate claim Heps1Def: eps1 = eps_ N1.
Use reflexivity.
We prove the intermediate claim HinvLtU0S: invN0 < u0.
rewrite the current goal using Hu0Def (from left to right).
rewrite the current goal using Heps1Def (from left to right).
An exact proof term for the current goal is (add_SNo_eps_Lt invN0 HinvN0S N1 HN1O).
An exact proof term for the current goal is (SNoLt_tra 0 invN0 u0 SNo_0 HinvN0S Hu0S HinvN0PosS HinvLtU0S).
We prove the intermediate claim H0leU0: 0 ≤ u0.
An exact proof term for the current goal is (SNoLtLe 0 u0 H0LtU0S).
An exact proof term for the current goal is (Rle_of_SNoLe 0 u0 real_0 Hu0R H0leU0).
Assume HbcapNonEmpty: b ∩ Vsmall ≠ Empty.
We prove the intermediate claim HbSfun: b ∈ Sfun F0.
An exact proof term for the current goal is ((andER (finite (Sfun F0) ∧ (Sfun F0) ⊆ F0) (∀b0 : set, b0 ∈ F0 → b0 ∩ Vsmall ≠ Empty → b0 ∈ (Sfun F0)) (HSfunSpec F0 HF0small)) b HbF0 HbcapNonEmpty).
We prove the intermediate claim HjEta: j = (j 0,j 1).
An exact proof term for the current goal is (setprod_eta ω B j Hjprod).
We prove the intermediate claim HjEqnb: j = (n,b).
We prove the intermediate claim Hj01: (j 0,j 1) = (n,b).
Apply tuple_2_ext to the current goal.
Use symmetry.
An exact proof term for the current goal is HnDef.
Use symmetry.
An exact proof term for the current goal is HbDef.
An exact proof term for the current goal is (eq_i_tra j (j 0,j 1) (n,b) HjEta Hj01).
We prove the intermediate claim HjEqIdx: j = (idx F0,b).
We prove the intermediate claim HnbEq: (n,b) = (idx F0,b).
Apply tuple_2_ext to the current goal.
Use symmetry.
An exact proof term for the current goal is HidxEq.
Use reflexivity.
An exact proof term for the current goal is (eq_i_tra j (n,b) (idx F0,b) HjEqnb HnbEq).
We prove the intermediate claim HjJsel: j ∈ Jsel F0.
rewrite the current goal using HjEqIdx (from left to right).
We prove the intermediate claim HJselDef: Jsel F0 = Repl (Sfun F0) (λb0 : set ⇒ (idx F0,b0)).
Use reflexivity.
rewrite the current goal using HJselDef (from left to right).
An exact proof term for the current goal is (ReplI (Sfun F0) (λb0 : set ⇒ (idx F0,b0)) b HbSfun).
We prove the intermediate claim HJselFam: (Jsel F0) ∈ Jfam.
An exact proof term for the current goal is (ReplI FamsSmall Jsel F0 HF0small).
We prove the intermediate claim HjNeed: j ∈ Jneed.
We prove the intermediate claim HJneedDef: Jneed = ⋃ Jfam.
Use reflexivity.
rewrite the current goal using HJneedDef (from left to right).
An exact proof term for the current goal is (UnionI Jfam j (Jsel F0) HjJsel HJselFam).
We prove the intermediate claim HNjInCfam: Nj j ∈ Cfam.
An exact proof term for the current goal is (ReplI Jneed Nj j HjNeed).
We prove the intermediate claim HVcontDef: Vcont = intersection_of_family X Cfam.
Use reflexivity.
We prove the intermediate claim HyInt: y ∈ intersection_of_family X Cfam.
rewrite the current goal using HVcontDef (from right to left).
An exact proof term for the current goal is HyVcont.
We prove the intermediate claim HzInt: z ∈ intersection_of_family X Cfam.
rewrite the current goal using HVcontDef (from right to left).
An exact proof term for the current goal is HzVcont.
We prove the intermediate claim HyNj: y ∈ Nj j.
An exact proof term for the current goal is (intersection_of_familyE2 X Cfam y HyInt (Nj j) HNjInCfam).
We prove the intermediate claim HzNj: z ∈ Nj j.
An exact proof term for the current goal is (intersection_of_familyE2 X Cfam z HzInt (Nj j) HNjInCfam).
We prove the intermediate claim HNjDef: Nj j = preimage_of X (apply_fun F j) (Ij j).
Use reflexivity.
We prove the intermediate claim HyPre: y ∈ preimage_of X (apply_fun F j) (Ij j).
rewrite the current goal using HNjDef (from right to left).
An exact proof term for the current goal is HyNj.
We prove the intermediate claim HzPre: z ∈ preimage_of X (apply_fun F j) (Ij j).
rewrite the current goal using HNjDef (from right to left).
An exact proof term for the current goal is HzNj.
We prove the intermediate claim HpreDef0: preimage_of X (apply_fun F j) (Ij j) = {x ∈ X|apply_fun (apply_fun F j) x ∈ (Ij j)}.
Use reflexivity.
We prove the intermediate claim HySep: y ∈ {x ∈ X|apply_fun (apply_fun F j) x ∈ (Ij j)}.
rewrite the current goal using HpreDef0 (from right to left).
An exact proof term for the current goal is HyPre.
We prove the intermediate claim HzSep: z ∈ {x ∈ X|apply_fun (apply_fun F j) x ∈ (Ij j)}.
rewrite the current goal using HpreDef0 (from right to left).
An exact proof term for the current goal is HzPre.
We prove the intermediate claim HyValIj0: apply_fun (apply_fun F j) y ∈ Ij j.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (apply_fun F j) x0 ∈ (Ij j)) y HySep).
We prove the intermediate claim HzValIj0: apply_fun (apply_fun F j) z ∈ Ij j.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (apply_fun F j) x0 ∈ (Ij j)) z HzSep).
We prove the intermediate claim Hfyj: apply_fun fy j = apply_fun (apply_fun F j) y.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J y j HyX HjJ).
We prove the intermediate claim Hfzj: apply_fun fz j = apply_fun (apply_fun F j) z.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J z j HzX HjJ).
We prove the intermediate claim HyValIj: apply_fun fy j ∈ Ij j.
rewrite the current goal using Hfyj (from left to right).
An exact proof term for the current goal is HyValIj0.
We prove the intermediate claim HzValIj: apply_fun fz j ∈ Ij j.
rewrite the current goal using Hfzj (from left to right).
An exact proof term for the current goal is HzValIj0.
We prove the intermediate claim HcdEq: power_real_coord_clipped_diff fy fz j = R_bounded_distance (apply_fun fy j) (apply_fun fz j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J fy fz j HjJ HfyY0 HfzY0).
rewrite the current goal using HcdEq (from left to right).
Set sy to be the term apply_fun fy j.
Set sz to be the term apply_fun fz j.
We prove the intermediate claim HsyR: sy ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J fy j HjJ HfyY0).
We prove the intermediate claim HszR: sz ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J fz j HjJ HfzY0).
We prove the intermediate claim HsyS: SNo sy.
An exact proof term for the current goal is (real_SNo sy HsyR).
We prove the intermediate claim HszS: SNo sz.
An exact proof term for the current goal is (real_SNo sz HszR).
We prove the intermediate claim HIjDef1: Ij j = ({t ∈ R|Rlt (add_SNo sy (minus_SNo eps3)) t} ∩ {t ∈ R|Rlt t (add_SNo sy eps3)}).
Use reflexivity.
We prove the intermediate claim HzValIj1: sz ∈ ({t ∈ R|Rlt (add_SNo sy (minus_SNo eps3)) t} ∩ {t ∈ R|Rlt t (add_SNo sy eps3)}).
rewrite the current goal using HIjDef1 (from right to left).
An exact proof term for the current goal is HzValIj.
We prove the intermediate claim HzLow: sz ∈ {t ∈ R|Rlt (add_SNo sy (minus_SNo eps3)) t}.
An exact proof term for the current goal is (binintersectE1 {t ∈ R|Rlt (add_SNo sy (minus_SNo eps3)) t} {t ∈ R|Rlt t (add_SNo sy eps3)} sz HzValIj1).
We prove the intermediate claim HzUp: sz ∈ {t ∈ R|Rlt t (add_SNo sy eps3)}.
An exact proof term for the current goal is (binintersectE2 {t ∈ R|Rlt (add_SNo sy (minus_SNo eps3)) t} {t ∈ R|Rlt t (add_SNo sy eps3)} sz HzValIj1).
We prove the intermediate claim HleftR: Rlt (add_SNo sy (minus_SNo eps3)) sz.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt (add_SNo sy (minus_SNo eps3)) t) sz HzLow).
We prove the intermediate claim HrightR: Rlt sz (add_SNo sy eps3).
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt t (add_SNo sy eps3)) sz HzUp).
We prove the intermediate claim HleftS: add_SNo sy (minus_SNo eps3) < sz.
An exact proof term for the current goal is (RltE_lt (add_SNo sy (minus_SNo eps3)) sz HleftR).
We prove the intermediate claim HrightS: sz < add_SNo sy eps3.
An exact proof term for the current goal is (RltE_lt sz (add_SNo sy eps3) HrightR).
Set t to be the term add_SNo sy (minus_SNo sz).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (real_add_SNo sy HsyR (minus_SNo sz) (real_minus_SNo sz HszR)).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HmSyS: SNo (minus_SNo sy).
An exact proof term for the current goal is (SNo_minus_SNo sy HsyS).
We prove the intermediate claim HmSzS: SNo (minus_SNo sz).
An exact proof term for the current goal is (SNo_minus_SNo sz HszS).
We prove the intermediate claim Hmeps3S: SNo (minus_SNo eps3).
An exact proof term for the current goal is (SNo_minus_SNo eps3 Heps3S).
We prove the intermediate claim HsyEps3S: SNo (add_SNo sy eps3).
An exact proof term for the current goal is (SNo_add_SNo sy eps3 HsyS Heps3S).
We prove the intermediate claim HsyMeps3S: SNo (add_SNo sy (minus_SNo eps3)).
An exact proof term for the current goal is (SNo_add_SNo sy (minus_SNo eps3) HsyS (SNo_minus_SNo eps3 Heps3S)).
Set diff to be the term add_SNo sz (minus_SNo sy).
We prove the intermediate claim HdiffS: SNo diff.
An exact proof term for the current goal is (SNo_add_SNo sz (minus_SNo sy) HszS HmSyS).
We prove the intermediate claim HdiffLtTmp: diff < add_SNo (add_SNo sy eps3) (minus_SNo sy).
An exact proof term for the current goal is (add_SNo_Lt1 sz (minus_SNo sy) (add_SNo sy eps3) HszS HmSyS HsyEps3S HrightS).
We prove the intermediate claim HRhs: add_SNo (add_SNo sy eps3) (minus_SNo sy) = eps3.
We prove the intermediate claim Hswap: add_SNo (add_SNo sy eps3) (minus_SNo sy) = add_SNo (add_SNo sy (minus_SNo sy)) eps3.
An exact proof term for the current goal is (add_SNo_com_3b_1_2 sy eps3 (minus_SNo sy) HsyS Heps3S HmSyS).
We prove the intermediate claim Hrest: add_SNo (add_SNo sy (minus_SNo sy)) eps3 = eps3.
We prove the intermediate claim HsyInv: add_SNo sy (minus_SNo sy) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv sy HsyS).
rewrite the current goal using HsyInv (from left to right).
rewrite the current goal using (add_SNo_0L eps3 Heps3S) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (eq_i_tra (add_SNo (add_SNo sy eps3) (minus_SNo sy)) (add_SNo (add_SNo sy (minus_SNo sy)) eps3) eps3 Hswap Hrest).
We prove the intermediate claim HdiffLt: diff < eps3.
rewrite the current goal using HRhs (from right to left).
An exact proof term for the current goal is HdiffLtTmp.
We prove the intermediate claim HdiffGtTmp: add_SNo (add_SNo sy (minus_SNo eps3)) (minus_SNo sy) < diff.
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo sy (minus_SNo eps3)) (minus_SNo sy) sz HsyMeps3S HmSyS HszS HleftS).
We prove the intermediate claim HLhs: add_SNo (add_SNo sy (minus_SNo eps3)) (minus_SNo sy) = minus_SNo eps3.
We prove the intermediate claim Hswap: add_SNo (add_SNo sy (minus_SNo eps3)) (minus_SNo sy) = add_SNo (add_SNo sy (minus_SNo sy)) (minus_SNo eps3).
An exact proof term for the current goal is (add_SNo_com_3b_1_2 sy (minus_SNo eps3) (minus_SNo sy) HsyS Hmeps3S HmSyS).
We prove the intermediate claim Hrest: add_SNo (add_SNo sy (minus_SNo sy)) (minus_SNo eps3) = minus_SNo eps3.
We prove the intermediate claim HsyInv: add_SNo sy (minus_SNo sy) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv sy HsyS).
rewrite the current goal using HsyInv (from left to right).
rewrite the current goal using (add_SNo_0L (minus_SNo eps3) Hmeps3S) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (eq_i_tra (add_SNo (add_SNo sy (minus_SNo eps3)) (minus_SNo sy)) (add_SNo (add_SNo sy (minus_SNo sy)) (minus_SNo eps3)) (minus_SNo eps3) Hswap Hrest).
We prove the intermediate claim HdiffGt: minus_SNo eps3 < diff.
rewrite the current goal using HLhs (from right to left).
An exact proof term for the current goal is HdiffGtTmp.
We prove the intermediate claim HdiffLo: minus_SNo eps3 ≤ diff.
An exact proof term for the current goal is (SNoLtLe (minus_SNo eps3) diff HdiffGt).
We prove the intermediate claim HdiffHi: diff ≤ eps3.
An exact proof term for the current goal is (SNoLtLe diff eps3 HdiffLt).
We prove the intermediate claim HabsDiffLe: abs_SNo diff ≤ eps3.
An exact proof term for the current goal is (abs_SNo_Le_of_bounds diff eps3 HdiffS Heps3S HdiffLo HdiffHi).
We prove the intermediate claim HtDef: t = add_SNo sy (minus_SNo sz).
Use reflexivity.
We prove the intermediate claim HdiffDef: diff = add_SNo sz (minus_SNo sy).
Use reflexivity.
We prove the intermediate claim HabsSwap0: abs_SNo t = abs_SNo diff.
rewrite the current goal using HtDef (from left to right).
rewrite the current goal using HdiffDef (from left to right).
An exact proof term for the current goal is (abs_SNo_dist_swap sy sz HsyS HszS).
We prove the intermediate claim HabsLe: abs_SNo t ≤ eps3.
rewrite the current goal using HabsSwap0 (from left to right).
An exact proof term for the current goal is HabsDiffLe.
We prove the intermediate claim HabsR: abs_SNo t ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R t HtR).
We prove the intermediate claim HbdLeAbs: Rle (R_bounded_distance sy sz) (abs_SNo t).
We prove the intermediate claim Hbddef: R_bounded_distance sy sz = if (Rlt (abs_SNo t) 1) then (abs_SNo t) else 1.
Use reflexivity.
Apply (xm (Rlt (abs_SNo t) 1) (Rle (R_bounded_distance sy sz) (abs_SNo t))) to the current goal.
Assume Hlt1: Rlt (abs_SNo t) 1.
rewrite the current goal using Hbddef (from left to right).
We prove the intermediate claim Hif: (if (Rlt (abs_SNo t) 1) then (abs_SNo t) else 1) = (abs_SNo t).
An exact proof term for the current goal is (If_i_1 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hlt1).
rewrite the current goal using Hif (from left to right).
An exact proof term for the current goal is (RleI (abs_SNo t) (abs_SNo t) HabsR HabsR (not_Rlt_refl (abs_SNo t) HabsR)).
Assume Hnlt1: ¬ (Rlt (abs_SNo t) 1).
rewrite the current goal using Hbddef (from left to right).
We prove the intermediate claim Hif: (if (Rlt (abs_SNo t) 1) then (abs_SNo t) else 1) = 1.
An exact proof term for the current goal is (If_i_0 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hnlt1).
rewrite the current goal using Hif (from left to right).
An exact proof term for the current goal is (RleI 1 (abs_SNo t) real_1 HabsR Hnlt1).
We prove the intermediate claim HabsLeR: Rle (abs_SNo t) eps3.
An exact proof term for the current goal is (Rle_of_SNoLe (abs_SNo t) eps3 HabsR Heps3R HabsLe).
We prove the intermediate claim HbdLeEps3: Rle (R_bounded_distance sy sz) eps3.
An exact proof term for the current goal is (Rle_tra (R_bounded_distance sy sz) (abs_SNo t) eps3 HbdLeAbs HabsLeR).
We prove the intermediate claim HN1in1: N1 ∈ ordsucc N1.
An exact proof term for the current goal is (ordsuccI2 N1).
We prove the intermediate claim HsuccSub: ordsucc N1 ⊆ ordsucc (ordsucc N1).
An exact proof term for the current goal is (ordsuccI1 (ordsucc N1)).
We prove the intermediate claim HN1in2: N1 ∈ ordsucc (ordsucc N1).
An exact proof term for the current goal is (HsuccSub N1 HN1in1).
We prove the intermediate claim Heps3LtEps1S: eps3 < eps1.
An exact proof term for the current goal is (SNo_eps_decr (ordsucc (ordsucc N1)) Heps3O N1 HN1in2).
We prove the intermediate claim Heps3LeEps1: eps3 ≤ eps1.
An exact proof term for the current goal is (SNoLtLe eps3 eps1 Heps3LtEps1S).
We prove the intermediate claim HsuccN0O: ordsucc N0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N0 HN0O).
We prove the intermediate claim HsuccN0Not0: ordsucc N0 ≠ 0.
An exact proof term for the current goal is (neq_ordsucc_0 N0).
We prove the intermediate claim HsuccN0NotIn0: ordsucc N0 ∉ {0}.
Assume Hs0: ordsucc N0 ∈ {0}.
An exact proof term for the current goal is (HsuccN0Not0 (SingE 0 (ordsucc N0) Hs0)).
We prove the intermediate claim HsuccN0In: ordsucc N0 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc N0) HsuccN0O HsuccN0NotIn0).
We prove the intermediate claim HinvN0Pos: Rlt 0 invN0.
An exact proof term for the current goal is (inv_nat_pos (ordsucc N0) HsuccN0In).
We prove the intermediate claim HinvN0PosS: 0 < invN0.
An exact proof term for the current goal is (RltE_lt 0 invN0 HinvN0Pos).
We prove the intermediate claim HinvN0NN: 0 ≤ invN0.
An exact proof term for the current goal is (SNoLtLe 0 invN0 HinvN0PosS).
We prove the intermediate claim Heps1LeU0S: eps1 ≤ add_SNo eps1 invN0.
An exact proof term for the current goal is (SNoLe_add_nonneg_right eps1 invN0 Heps1S HinvN0S HinvN0NN).
We prove the intermediate claim Hu0Def: u0 = add_SNo invN0 eps1.
Use reflexivity.
We prove the intermediate claim Hcom: add_SNo invN0 eps1 = add_SNo eps1 invN0.
An exact proof term for the current goal is (add_SNo_com invN0 eps1 HinvN0S Heps1S).
We prove the intermediate claim Heps1LeU0: eps1 ≤ u0.
rewrite the current goal using Hu0Def (from left to right).
rewrite the current goal using Hcom (from left to right).
An exact proof term for the current goal is Heps1LeU0S.
We prove the intermediate claim Heps3LeU0: eps3 ≤ u0.
An exact proof term for the current goal is (SNoLe_tra eps3 eps1 u0 Heps3S Heps1S Hu0S Heps3LeEps1 Heps1LeU0).
We prove the intermediate claim Heps3LeU0R: Rle eps3 u0.
An exact proof term for the current goal is (Rle_of_SNoLe eps3 u0 Heps3R Hu0R Heps3LeU0).
An exact proof term for the current goal is (Rle_tra (R_bounded_distance sy sz) eps3 u0 HbdLeEps3 Heps3LeU0R).
Assume HnEq: n = ordsucc N0.
Apply Hlarge to the current goal.
rewrite the current goal using HnEq (from left to right).
An exact proof term for the current goal is (ordsuccI2 N0).
Assume HnLarge: (ordsucc N0) ∈ n.
Apply Hlarge to the current goal.
We prove the intermediate claim Htransn: TransSet n.
An exact proof term for the current goal is (ordinal_TransSet n Hordn).
We prove the intermediate claim Hsub: ordsucc N0 ⊆ n.
An exact proof term for the current goal is (Htransn (ordsucc N0) HnLarge).
An exact proof term for the current goal is (Hsub N0 (ordsuccI2 N0)).
We use u0 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 Hu0R.
An exact proof term for the current goal is Hu0Ltd.
An exact proof term for the current goal is Hub_u0.
Apply Hexu to the current goal.
Let u be given.
Assume HuPack.
We prove the intermediate claim Hub: ∀a : set, a ∈ A → a ∈ R → Rle a u.
An exact proof term for the current goal is (andER (u ∈ R ∧ Rlt u d) (∀a : set, a ∈ A → a ∈ R → Rle a u) HuPack).
We prove the intermediate claim HuPair: u ∈ R ∧ Rlt u d.
An exact proof term for the current goal is (andEL (u ∈ R ∧ Rlt u d) (∀a : set, a ∈ A → a ∈ R → Rle a u) HuPack).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (andEL (u ∈ R) (Rlt u d) HuPair).
We prove the intermediate claim HuLtd: Rlt u d.
An exact proof term for the current goal is (andER (u ∈ R) (Rlt u d) HuPair).
We prove the intermediate claim Hle: Rle val u.
An exact proof term for the current goal is (Hmin u HuR Hub).
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid val u d Hle HuLtd).
We use V 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 HVTx.
An exact proof term for the current goal is HyV.
Let z be given.
Assume HzV: z ∈ V.
An exact proof term for the current goal is (HctrlBall z HzV).
Apply HexV0 to the current goal.
Let V be given.
Assume HVpack0.
We prove the intermediate claim HVpair0: V ∈ Tx ∧ y ∈ V.
An exact proof term for the current goal is (andEL (V ∈ Tx ∧ y ∈ V) (∀z : set, z ∈ V → Rlt (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) d) HVpack0).
We prove the intermediate claim HVTx0: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (y ∈ V) HVpair0).
We prove the intermediate claim HyV0: y ∈ V.
An exact proof term for the current goal is (andER (V ∈ Tx) (y ∈ V) HVpair0).
We prove the intermediate claim HVctrl0: ∀z : set, z ∈ V → Rlt (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) d.
An exact proof term for the current goal is (andER (V ∈ Tx ∧ y ∈ V) (∀z : set, z ∈ V → Rlt (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) d) HVpack0).
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVpair0.
Let z be given.
Assume HzV0: z ∈ V.
We will prove z ∈ Ball.
We prove the intermediate claim HzX: z ∈ X.
We prove the intermediate claim HVsubX: V ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V HTx HVTx0).
An exact proof term for the current goal is (HVsubX z HzV0).
We prove the intermediate claim HfzY: apply_fun Fmap z ∈ power_real J.
An exact proof term for the current goal is (HFmapfun z HzX).
We prove the intermediate claim Hczpair: (c,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X c z HcX HzX).
We prove the intermediate claim Hyzpair: (y,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y z HyX HzX).
We prove the intermediate claim HdXczEq: apply_fun dX (c,z) = apply_fun dY (apply_fun Fmap c,apply_fun Fmap z).
rewrite the current goal using HdXdef2 (from left to right).
We prove the intermediate claim Htmp: apply_fun (graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1)))) (c,z) = apply_fun dY (apply_fun Fmap ((c,z) 0),apply_fun Fmap ((c,z) 1)).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (c,z) Hczpair).
rewrite the current goal using Htmp (from left to right).
rewrite the current goal using (tuple_2_0_eq c z) (from left to right).
rewrite the current goal using (tuple_2_1_eq c z) (from left to right).
Use reflexivity.
We prove the intermediate claim HdXyzEq: apply_fun dX (y,z) = apply_fun dY (apply_fun Fmap y,apply_fun Fmap z).
rewrite the current goal using HdXdef2 (from left to right).
We prove the intermediate claim Htmp: apply_fun (graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1)))) (y,z) = apply_fun dY (apply_fun Fmap ((y,z) 0),apply_fun Fmap ((y,z) 1)).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (y,z) Hyzpair).
rewrite the current goal using Htmp (from left to right).
rewrite the current goal using (tuple_2_0_eq y z) (from left to right).
rewrite the current goal using (tuple_2_1_eq y z) (from left to right).
Use reflexivity.
We prove the intermediate claim HdYyzR: apply_fun dY (apply_fun Fmap y,apply_fun Fmap z) ∈ R.
We prove the intermediate claim HpairYZ: (apply_fun Fmap y,apply_fun Fmap z) ∈ setprod (power_real J) (power_real J).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (power_real J) (power_real J) (apply_fun Fmap y) (apply_fun Fmap z) HfyY HfzY).
An exact proof term for the current goal is (HdYfun (apply_fun Fmap y,apply_fun Fmap z) HpairYZ).
We prove the intermediate claim HtriLe: Rle (apply_fun dY (apply_fun Fmap c,apply_fun Fmap z)) (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z))).
An exact proof term for the current goal is (metric_triangle_Rle (power_real J) dY (apply_fun Fmap c) (apply_fun Fmap y) (apply_fun Fmap z) HmY HfcY HfyY HfzY).
We prove the intermediate claim HdyzLt: Rlt (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) d.
An exact proof term for the current goal is (HVctrl0 z HzV0).
We prove the intermediate claim HdyzLtS: apply_fun dY (apply_fun Fmap y,apply_fun Fmap z) < d.
An exact proof term for the current goal is (RltE_lt (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) d HdyzLt).
We prove the intermediate claim HcyR: apply_fun dY (apply_fun Fmap c,apply_fun Fmap y) ∈ R.
rewrite the current goal using HdistEq (from right to left).
An exact proof term for the current goal is HdistR.
We prove the intermediate claim HcyS: SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)).
An exact proof term for the current goal is (real_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) HcyR).
We prove the intermediate claim HdyzS: SNo (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)).
An exact proof term for the current goal is (real_SNo (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) HdYyzR).
We prove the intermediate claim Hsum1LtS: add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) < add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) d.
An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) d HcyS HdyzS HdS HdyzLtS).
We prove the intermediate claim Hsum1R: add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) HcyR (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z)) HdYyzR).
We prove the intermediate claim Hsum2R: add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) d ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) HcyR d HdR).
We prove the intermediate claim Hsum1LtR1: Rlt (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z))) (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) d).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z))) (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) d) Hsum1R Hsum2R Hsum1LtS).
We prove the intermediate claim Hsum2LtRtmp: Rlt (add_SNo d (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y))) r.
rewrite the current goal using HdistEq (from right to left).
An exact proof term for the current goal is HsumLtR.
We prove the intermediate claim Hcomm: add_SNo d (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) = add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) d.
An exact proof term for the current goal is (add_SNo_com d (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) HdS HcyS).
We prove the intermediate claim Hsum2LtR: Rlt (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) d) r.
rewrite the current goal using Hcomm (from right to left).
An exact proof term for the current goal is Hsum2LtRtmp.
We prove the intermediate claim HsumLtR2: Rlt (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z))) r.
An exact proof term for the current goal is (Rlt_tra (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z))) (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) d) r Hsum1LtR1 Hsum2LtR).
We prove the intermediate claim HczLt: Rlt (apply_fun dY (apply_fun Fmap c,apply_fun Fmap z)) r.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (apply_fun dY (apply_fun Fmap c,apply_fun Fmap z)) (add_SNo (apply_fun dY (apply_fun Fmap c,apply_fun Fmap y)) (apply_fun dY (apply_fun Fmap y,apply_fun Fmap z))) r HtriLe HsumLtR2).
We prove the intermediate claim HczLtX: Rlt (apply_fun dX (c,z)) r.
rewrite the current goal using HdXczEq (from left to right).
An exact proof term for the current goal is HczLt.
An exact proof term for the current goal is (open_ballI X dX c r z HzX HczLtX).
An exact proof term for the current goal is HexVJne.
Apply HexV to the current goal.
Let V be given.
Assume HVpack: V ∈ Tx ∧ y ∈ V ∧ V ⊆ Ball.
We prove the intermediate claim HVpair: V ∈ Tx ∧ y ∈ V.
An exact proof term for the current goal is (andEL (V ∈ Tx ∧ y ∈ V) (V ⊆ Ball) HVpack).
We prove the intermediate claim HVsub: V ⊆ Ball.
An exact proof term for the current goal is (andER (V ∈ Tx ∧ y ∈ V) (V ⊆ Ball) HVpack).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (y ∈ V) HVpair).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andER (V ∈ Tx) (y ∈ V) HVpair).
We prove the intermediate claim HVFam: V ∈ Fam.
An exact proof term for the current goal is (SepI Tx (λV0 : set ⇒ V0 ⊆ Ball) V HVTx HVsub).
An exact proof term for the current goal is (UnionI Fam y V HyV HVFam).
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionInTx.
We prove the intermediate claim Hinc: generated_topology X Bx ⊆ Tx.
An exact proof term for the current goal is (generated_topology_finer_weak X Bx Tx HTx HBxSub).
An exact proof term for the current goal is (Hinc U HUgen).
Let U be given.
Assume HU: U ∈ Tx.
We will prove U ∈ metric_topology X dX.
Set Bx to be the term famunion X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim Hmtdef: metric_topology X dX = generated_topology X Bx.
Use reflexivity.
rewrite the current goal using Hmtdef (from left to right).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HU).
We prove the intermediate claim HUPowX: U ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X U HUsubX).
We prove the intermediate claim HUcond: ∀x ∈ U, ∃b0 ∈ Bx, x ∈ b0 ∧ b0 ⊆ U.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsubX x HxU).
We prove the intermediate claim Hexj: ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x) ∧ ∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0.
An exact proof term for the current goal is (HsepNeigh x HxX U HU HxU).
Apply Hexj to the current goal.
Let j be given.
Assume Hjpack: j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x) ∧ ∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0.
We prove the intermediate claim Hjpair: j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (andEL (j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x)) (∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0) Hjpack).
We prove the intermediate claim HjJ: j ∈ J.
An exact proof term for the current goal is (andEL (j ∈ J) (Rlt 0 (apply_fun (apply_fun F j) x)) Hjpair).
We prove the intermediate claim Hrpos: Rlt 0 (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (andER (j ∈ J) (Rlt 0 (apply_fun (apply_fun F j) x)) Hjpair).
We prove the intermediate claim HzeroOut: ∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0.
An exact proof term for the current goal is (andER (j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x)) (∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0) Hjpack).
Set r to be the term apply_fun (apply_fun F j) x.
We prove the intermediate claim HrR: r ∈ R.
We prove the intermediate claim HFjFS: apply_fun F j ∈ function_space X R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y F J (function_space X R) j HtotF HjJ).
We prove the intermediate claim HFjfun: function_on (apply_fun F j) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun F j) X R HFjFS).
An exact proof term for the current goal is (HFjfun x HxX).
We prove the intermediate claim Hexeps: ∃eps : set, eps ∈ R ∧ Rlt 0 eps ∧ Rlt eps r ∧ Rlt eps 1.
An exact proof term for the current goal is (exists_eps_lt_two_pos_Euclid r 1 HrR real_1 Hrpos Rlt_0_1).
Apply Hexeps to the current goal.
Let eps be given.
Assume HepsPack: eps ∈ R ∧ Rlt 0 eps ∧ Rlt eps r ∧ Rlt eps 1.
We prove the intermediate claim HepsLeft: (eps ∈ R ∧ Rlt 0 eps) ∧ Rlt eps r.
An exact proof term for the current goal is (andEL ((eps ∈ R ∧ Rlt 0 eps) ∧ Rlt eps r) (Rlt eps 1) HepsPack).
We prove the intermediate claim HepsLt1: Rlt eps 1.
An exact proof term for the current goal is (andER ((eps ∈ R ∧ Rlt 0 eps) ∧ Rlt eps r) (Rlt eps 1) HepsPack).
We prove the intermediate claim HepsPair: eps ∈ R ∧ Rlt 0 eps.
An exact proof term for the current goal is (andEL (eps ∈ R ∧ Rlt 0 eps) (Rlt eps r) HepsLeft).
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) HepsPair).
We prove the intermediate claim HepsPos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) HepsPair).
We prove the intermediate claim HepsLt: Rlt eps r.
An exact proof term for the current goal is (andER (eps ∈ R ∧ Rlt 0 eps) (Rlt eps r) HepsLeft).
We use (open_ball X dX x eps) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HballIn: open_ball X dX x eps ∈ {open_ball X dX x r|r ∈ R, Rlt 0 r}.
An exact proof term for the current goal is (ReplSepI R (λr : set ⇒ Rlt 0 r) (λr : set ⇒ open_ball X dX x r) eps HepsR HepsPos).
An exact proof term for the current goal is (famunionI X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}) x (open_ball X dX x eps) HxX HballIn).
Apply andI to the current goal.
We will prove x ∈ open_ball X dX x eps.
We prove the intermediate claim Hltxx: Rlt (apply_fun dX (x,x)) eps.
We prove the intermediate claim HxxIn: (x,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x x HxX HxX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
We prove the intermediate claim HxxEq: apply_fun dX (x,x) = apply_fun dY (apply_fun Fmap ((x,x) 0),apply_fun Fmap ((x,x) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,x) HxxIn).
rewrite the current goal using HxxEq (from left to right).
rewrite the current goal using (tuple_2_0_eq x x) (from left to right).
rewrite the current goal using (tuple_2_1_eq x x) (from left to right).
We prove the intermediate claim HfxY: apply_fun Fmap x ∈ power_real J.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HdY0: apply_fun dY (apply_fun Fmap x,apply_fun Fmap x) = 0.
An exact proof term for the current goal is (metric_on_diag_zero (power_real J) dY (apply_fun Fmap x) HmY HfxY).
rewrite the current goal using HdY0 (from left to right).
An exact proof term for the current goal is HepsPos.
An exact proof term for the current goal is (open_ballI X dX x eps x HxX Hltxx).
Let y be given.
Assume Hyb0: y ∈ open_ball X dX x eps.
We will prove y ∈ U.
Apply (xm (y ∈ U)) to the current goal.
An exact proof term for the current goal is (λHyU ⇒ HyU).
Assume HynU: y ∉ U.
Apply FalseE to the current goal.
We prove the intermediate claim Hcontra: False.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X dX x eps y Hyb0).
We prove the intermediate claim HyOut: y ∈ X ∖ U.
An exact proof term for the current goal is (setminusI X U y HyX HynU).
We prove the intermediate claim Hfy0: apply_fun (apply_fun F j) y = 0.
An exact proof term for the current goal is (HzeroOut y HyOut).
We prove the intermediate claim HJne: J ≠ Empty.
Assume HJeq: J = Empty.
We will prove False.
We prove the intermediate claim HjEmpty: j ∈ Empty.
rewrite the current goal using HJeq (from right to left).
An exact proof term for the current goal is HjJ.
An exact proof term for the current goal is (EmptyE j HjEmpty False).
We prove the intermediate claim HfxY: apply_fun Fmap x ∈ power_real J.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ power_real J.
An exact proof term for the current goal is (HFmapfun y HyX).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HdXdef2: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
We prove the intermediate claim HdxyEq: apply_fun dX (x,y) = apply_fun dY (apply_fun Fmap ((x,y) 0),apply_fun Fmap ((x,y) 1)).
rewrite the current goal using HdXdef2 (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,y) HxyIn).
We prove the intermediate claim HdxyEq2: apply_fun dX (x,y) = apply_fun dY (apply_fun Fmap x,apply_fun Fmap y).
rewrite the current goal using HdxyEq (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdlt: Rlt (apply_fun dX (x,y)) eps.
An exact proof term for the current goal is (open_ballE2 X dX x eps y Hyb0).
We prove the intermediate claim HdYlt: Rlt (apply_fun dY (apply_fun Fmap x,apply_fun Fmap y)) eps.
rewrite the current goal using HdxyEq2 (from right to left).
An exact proof term for the current goal is Hdlt.
We prove the intermediate claim HdYapp: apply_fun dY (apply_fun Fmap x,apply_fun Fmap y) = power_real_uniform_metric_value J (apply_fun Fmap x) (apply_fun Fmap y).
We prove the intermediate claim HdYdef: dY = uniform_metric_power_real J.
Use reflexivity.
rewrite the current goal using HdYdef (from left to right).
An exact proof term for the current goal is (uniform_metric_power_real_apply J (apply_fun Fmap x) (apply_fun Fmap y) HfxY HfyY).
We prove the intermediate claim Hltval: Rlt (power_real_uniform_metric_value J (apply_fun Fmap x) (apply_fun Fmap y)) eps.
rewrite the current goal using HdYapp (from right to left).
An exact proof term for the current goal is HdYlt.
Set A to be the term power_real_clipped_diffs J (apply_fun Fmap x) (apply_fun Fmap y).
Set l to be the term power_real_uniform_metric_value J (apply_fun Fmap x) (apply_fun Fmap y).
Set a to be the term power_real_coord_clipped_diff (apply_fun Fmap x) (apply_fun Fmap y) j.
We prove the intermediate claim Hlub: R_lub A l.
An exact proof term for the current goal is (power_real_uniform_metric_value_is_lub J (apply_fun Fmap x) (apply_fun Fmap y) HJne HfxY HfyY).
We prove the intermediate claim Hcore: l ∈ R ∧ ∀b : set, b ∈ A → b ∈ R → Rle b l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀b : set, b ∈ A → b ∈ R → Rle b l) (∀u : set, u ∈ R → (∀b : set, b ∈ A → b ∈ R → Rle b u) → Rle l u) Hlub).
We prove the intermediate claim Hub: ∀b : set, b ∈ A → b ∈ R → Rle b l.
An exact proof term for the current goal is (andER (l ∈ R) (∀b : set, b ∈ A → b ∈ R → Rle b l) Hcore).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (ReplI J (λj0 : set ⇒ power_real_coord_clipped_diff (apply_fun Fmap x) (apply_fun Fmap y) j0) j HjJ).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (power_real_clipped_diffs_in_R J (apply_fun Fmap x) (apply_fun Fmap y) a HfxY HfyY HaA).
We prove the intermediate claim Hale: Rle a l.
An exact proof term for the current goal is (Hub a HaA HaR).
We prove the intermediate claim Hltleps: Rlt l eps.
We prove the intermediate claim HlDef: l = power_real_uniform_metric_value J (apply_fun Fmap x) (apply_fun Fmap y).
Use reflexivity.
rewrite the current goal using HlDef (from left to right).
An exact proof term for the current goal is Hltval.
We prove the intermediate claim Halt: Rlt a eps.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid a l eps Hale Hltleps).
We prove the intermediate claim HcoordEqx: apply_fun (apply_fun Fmap x) j = apply_fun (apply_fun F j) x.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J x j HxX HjJ).
We prove the intermediate claim HcoordEqy: apply_fun (apply_fun Fmap y) j = apply_fun (apply_fun F j) y.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_coord_apply X F J y j HyX HjJ).
We prove the intermediate claim Haxdef: a = R_bounded_distance (apply_fun (apply_fun F j) x) (apply_fun (apply_fun F j) y).
We prove the intermediate claim HaDef: a = power_real_coord_clipped_diff (apply_fun Fmap x) (apply_fun Fmap y) j.
Use reflexivity.
We prove the intermediate claim HaEq0: a = R_bounded_distance (apply_fun (apply_fun Fmap x) j) (apply_fun (apply_fun Fmap y) j).
rewrite the current goal using HaDef (from left to right).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J (apply_fun Fmap x) (apply_fun Fmap y) j HjJ HfxY HfyY).
rewrite the current goal using HaEq0 (from left to right).
rewrite the current goal using HcoordEqx (from left to right).
rewrite the current goal using HcoordEqy (from left to right).
Use reflexivity.
We prove the intermediate claim HxvalR: apply_fun (apply_fun F j) x ∈ R.
An exact proof term for the current goal is HrR.
We prove the intermediate claim HyvalR: apply_fun (apply_fun F j) y ∈ R.
We prove the intermediate claim HFjFS: apply_fun F j ∈ function_space X R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y F J (function_space X R) j HtotF HjJ).
We prove the intermediate claim HFjfun: function_on (apply_fun F j) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun F j) X R HFjFS).
An exact proof term for the current goal is (HFjfun y HyX).
We prove the intermediate claim Halt2: Rlt (R_bounded_distance (apply_fun (apply_fun F j) x) (apply_fun (apply_fun F j) y)) eps.
rewrite the current goal using Haxdef (from right to left).
An exact proof term for the current goal is Halt.
We prove the intermediate claim Habslt: abs_SNo (add_SNo (apply_fun (apply_fun F j) x) (minus_SNo (apply_fun (apply_fun F j) y))) < eps.
An exact proof term for the current goal is (R_bounded_distance_lt_lt1_imp_abs_lt (apply_fun (apply_fun F j) x) (apply_fun (apply_fun F j) y) eps HxvalR HyvalR HepsR HepsLt1 Halt2).
We prove the intermediate claim HyzeroS: apply_fun (apply_fun F j) y = 0.
An exact proof term for the current goal is Hfy0.
We prove the intermediate claim HxS: SNo (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (real_SNo (apply_fun (apply_fun F j) x) HrR).
We prove the intermediate claim HabsEq: abs_SNo (apply_fun (apply_fun F j) x) = apply_fun (apply_fun F j) x.
An exact proof term for the current goal is (pos_abs_SNo (apply_fun (apply_fun F j) x) (RltE_lt 0 (apply_fun (apply_fun F j) x) Hrpos)).
We prove the intermediate claim Habseq2: abs_SNo (add_SNo (apply_fun (apply_fun F j) x) (minus_SNo (apply_fun (apply_fun F j) y))) = abs_SNo (apply_fun (apply_fun F j) x).
rewrite the current goal using HyzeroS (from left to right).
An exact proof term for the current goal is (abs_SNo_add_minus_zero (apply_fun (apply_fun F j) x) HxS).
We prove the intermediate claim Habsx: abs_SNo (apply_fun (apply_fun F j) x) < eps.
rewrite the current goal using Habseq2 (from right to left).
An exact proof term for the current goal is Habslt.
We prove the intermediate claim Hxlt: apply_fun (apply_fun F j) x < eps.
rewrite the current goal using HabsEq (from right to left).
An exact proof term for the current goal is Habsx.
We prove the intermediate claim HxltR: Rlt (apply_fun (apply_fun F j) x) eps.
An exact proof term for the current goal is (RltI (apply_fun (apply_fun F j) x) eps HrR HepsR Hxlt).
We prove the intermediate claim Hrr: Rlt (apply_fun (apply_fun F j) x) (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (Rlt_tra (apply_fun (apply_fun F j) x) eps (apply_fun (apply_fun F j) x) HxltR HepsLt).
An exact proof term for the current goal is ((not_Rlt_refl (apply_fun (apply_fun F j) x) HrR) Hrr).
An exact proof term for the current goal is Hcontra.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x ∈ U0, ∃b0 ∈ Bx, x ∈ b0 ∧ b0 ⊆ U0) U HUPowX HUcond).
∎