Let X and Tx be given.
Assume Hreg: regular_space X Tx.
Assume Hscc: second_countable_space X Tx.
We will prove ∃d : set, metric_on X d ∧ metric_topology X d = Tx.
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 Hnorm: normal_space X Tx.
An exact proof term for the current goal is (regular_countable_basis_normal X Tx Hreg Hscc).
We prove the intermediate claim HexB: ∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hscc).
Apply HexB to the current goal.
Let B be given.
Assume HBpack: basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
Set J to be the term ω.
We prove the intermediate claim HexSep: ∃F : set, separating_family_of_functions X Tx F J.
We prove the intermediate claim HBpair: basis_on X B ∧ countable_set B.
An exact proof term for the current goal is (andEL (basis_on X B ∧ countable_set B) (basis_generates X B Tx) HBpack).
We prove the intermediate claim HB: basis_on X B.
An exact proof term for the current goal is (andEL (basis_on X B) (countable_set B) HBpair).
We prove the intermediate claim HBcount: countable_set B.
An exact proof term for the current goal is (andER (basis_on X B) (countable_set B) HBpair).
We prove the intermediate claim HBgen: basis_generates X B Tx.
An exact proof term for the current goal is (andER (basis_on X B ∧ countable_set B) (basis_generates X B Tx) HBpack).
Set P to be the term {p ∈ (B ⨯ B)|closure_of X Tx (proj0 p) ⊆ proj1 p}.
We prove the intermediate claim HPsub: P ⊆ (B ⨯ B).
Let p be given.
Assume HpP: p ∈ P.
An exact proof term for the current goal is (SepE1 (B ⨯ B) (λp0 : set ⇒ closure_of X Tx (proj0 p0) ⊆ proj1 p0) p HpP).
We prove the intermediate claim HBBcount: countable_set (B ⨯ B).
An exact proof term for the current goal is (setprod_countable B B HBcount HBcount).
We prove the intermediate claim HPcount: countable_set P.
An exact proof term for the current goal is (atleastp_tra P (B ⨯ B) ω (Subq_atleastp P (B ⨯ B) HPsub) HBBcount).
Apply HPcount to the current goal.
Let enc be given.
Assume Henc: inj P ω enc.
Set pair_of to be the term (λn : set ⇒ inv P enc n).
Set bump to be the term (λp : set ⇒ if p ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) else const_fun X 0).
Set F to be the term graph J (λn : set ⇒ bump (pair_of n)).
We use F to witness the existential quantifier.
We will prove separating_family_of_functions X Tx F J.
We prove the intermediate claim HgenEq: generated_topology X B = Tx.
An exact proof term for the current goal is (andER (basis_on X B) (generated_topology X B = Tx) HBgen).
We prove the intermediate claim HTyR: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
We prove the intermediate claim HconstFS: const_fun X 0 ∈ function_space X R.
Set f0 to be the term const_fun X 0.
We prove the intermediate claim Hsub: f0 ⊆ setprod X R.
Let q be given.
Assume Hq: q ∈ f0.
We will prove q ∈ setprod X R.
Apply (ReplE_impred X (λa0 : set ⇒ (a0,0)) q Hq (q ∈ setprod X R)) to the current goal.
Let a be given.
Assume HaX: a ∈ X.
Assume Heq: q = (a,0).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X R a 0 HaX H0R).
We prove the intermediate claim Hpow: f0 ∈ 𝒫 (setprod X R).
An exact proof term for the current goal is (PowerI (setprod X R) f0 Hsub).
We prove the intermediate claim Hfun: function_on f0 X R.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun f0 x ∈ R.
We prove the intermediate claim Happ: apply_fun f0 x = 0.
An exact proof term for the current goal is (const_fun_apply X 0 x HxX).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is H0R.
An exact proof term for the current goal is (SepI (𝒫 (setprod X R)) (λf0 : set ⇒ function_on f0 X R) f0 Hpow Hfun).
We prove the intermediate claim HconstCont: continuous_map X Tx R R_standard_topology (const_fun X 0).
An exact proof term for the current goal is (const_fun_continuous X Tx R R_standard_topology 0 HTx HTyR H0R).
We prove the intermediate claim Hbump_ex: ∀p : set, p ∈ P → ∃f : set, f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1).
Let p be given.
Assume HpP: p ∈ P.
We prove the intermediate claim HpBB: p ∈ (B ⨯ B).
An exact proof term for the current goal is (SepE1 (B ⨯ B) (λp0 : set ⇒ closure_of X Tx (proj0 p0) ⊆ proj1 p0) p HpP).
We prove the intermediate claim HclSub: closure_of X Tx (proj0 p) ⊆ proj1 p.
An exact proof term for the current goal is (SepE2 (B ⨯ B) (λp0 : set ⇒ closure_of X Tx (proj0 p0) ⊆ proj1 p0) p HpP).
We prove the intermediate claim HUinB: proj0 p ∈ B.
An exact proof term for the current goal is (proj0_Sigma B (λx0 : set ⇒ B) p HpBB).
We prove the intermediate claim HVinB: proj1 p ∈ B.
An exact proof term for the current goal is (proj1_Sigma B (λx0 : set ⇒ B) p HpBB).
We prove the intermediate claim HUgen: proj0 p ∈ generated_topology X B.
An exact proof term for the current goal is (basis_in_generated X B (proj0 p) HB HUinB).
We prove the intermediate claim HVgen: proj1 p ∈ generated_topology X B.
An exact proof term for the current goal is (basis_in_generated X B (proj1 p) HB HVinB).
We prove the intermediate claim HUtx: proj0 p ∈ Tx.
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HUgen.
We prove the intermediate claim HVtx: proj1 p ∈ Tx.
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HVgen.
We prove the intermediate claim HclClosed: closed_in X Tx (closure_of X Tx (proj0 p)).
An exact proof term for the current goal is (andER (closure_of X Tx (closure_of X Tx (proj0 p)) = closure_of X Tx (proj0 p)) (closed_in X Tx (closure_of X Tx (proj0 p))) (closure_idempotent_and_closed X Tx (proj0 p) HTx)).
We prove the intermediate claim HcV: closed_in X Tx (X ∖ (proj1 p)).
An exact proof term for the current goal is (closed_of_open_complement X Tx (proj1 p) HTx HVtx).
We prove the intermediate claim Hdisj: (X ∖ (proj1 p)) ∩ (closure_of X Tx (proj0 p)) = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ (X ∖ (proj1 p)) ∩ (closure_of X Tx (proj0 p)).
We will prove z ∈ Empty.
We prove the intermediate claim HzOut: z ∈ X ∖ (proj1 p).
An exact proof term for the current goal is (binintersectE1 (X ∖ (proj1 p)) (closure_of X Tx (proj0 p)) z Hz).
We prove the intermediate claim HzCl: z ∈ closure_of X Tx (proj0 p).
An exact proof term for the current goal is (binintersectE2 (X ∖ (proj1 p)) (closure_of X Tx (proj0 p)) z Hz).
We prove the intermediate claim HznotV: z ∉ proj1 p.
An exact proof term for the current goal is (setminusE2 X (proj1 p) z HzOut).
We prove the intermediate claim HzV: z ∈ proj1 p.
An exact proof term for the current goal is (HclSub z HzCl).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HznotV HzV).
We prove the intermediate claim H01: Rle 0 1.
An exact proof term for the current goal is (Rlt_implies_Rle 0 1 Rlt_0_1).
We prove the intermediate claim Hexg: ∃g : set, continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) g ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun g x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun g x0 = 1).
An exact proof term for the current goal is (Urysohn_lemma X Tx (X ∖ (proj1 p)) (closure_of X Tx (proj0 p)) 0 1 H01 Hnorm HcV HclClosed Hdisj).
Apply Hexg to the current goal.
Let g be given.
Assume Hgpack.
We prove the intermediate claim HgAB: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) g ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun g x0 = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) g ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun g x0 = 0)) (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun g x0 = 1) Hgpack).
We prove the intermediate claim Hg1: ∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun g x0 = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) g ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun g x0 = 0)) (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun g x0 = 1) Hgpack).
We prove the intermediate claim HgcontI: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) g.
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) g) (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun g x0 = 0) HgAB).
We prove the intermediate claim Hg0: ∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun g x0 = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) g) (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun g x0 = 0) HgAB).
We prove the intermediate claim HgcontR: continuous_map X Tx R R_standard_topology g.
We prove the intermediate claim HsubI: closed_interval 0 1 ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R 0 1).
We prove the intermediate claim HTi: closed_interval_topology 0 1 = subspace_topology R R_standard_topology (closed_interval 0 1).
Use reflexivity.
An exact proof term for the current goal is (continuous_map_range_expand X Tx (closed_interval 0 1) (closed_interval_topology 0 1) R R_standard_topology g HgcontI HsubI HTyR HTi).
Set h to be the term (λx0 : set ⇒ apply_fun g x0).
Set f to be the term graph X h.
We use f to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim Hsub: f ⊆ setprod X R.
Let q be given.
Assume Hq: q ∈ f.
We will prove q ∈ setprod X R.
Apply (ReplE_impred X (λa0 : set ⇒ (a0,h a0)) q Hq (q ∈ setprod X R)) to the current goal.
Let a be given.
Assume HaX: a ∈ X.
Assume Heq: q = (a,h a).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HhaR: h a ∈ R.
We prove the intermediate claim Hgfun: function_on g X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology g HgcontR).
An exact proof term for the current goal is (Hgfun a HaX).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X R a (h a) HaX HhaR).
We prove the intermediate claim Hpow: f ∈ 𝒫 (setprod X R).
An exact proof term for the current goal is (PowerI (setprod X R) f Hsub).
We prove the intermediate claim Hfun: function_on f X R.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
We will prove apply_fun f x0 ∈ R.
We prove the intermediate claim Happ: apply_fun f x0 = h x0.
An exact proof term for the current goal is (apply_fun_graph X h x0 Hx0X).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hgfun: function_on g X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology g HgcontR).
An exact proof term for the current goal is (Hgfun x0 Hx0X).
An exact proof term for the current goal is (SepI (𝒫 (setprod X R)) (λf0 : set ⇒ function_on f0 X R) f Hpow Hfun).
We will prove continuous_map X Tx R R_standard_topology f.
We will prove topology_on X Tx ∧ topology_on R R_standard_topology ∧ function_on f X R ∧ ∀V : set, V ∈ R_standard_topology → preimage_of X f V ∈ Tx.
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 HTyR.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
We will prove apply_fun f x0 ∈ R.
We prove the intermediate claim Happ: apply_fun f x0 = h x0.
An exact proof term for the current goal is (apply_fun_graph X h x0 Hx0X).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hgfun: function_on g X R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology g HgcontR).
An exact proof term for the current goal is (Hgfun x0 Hx0X).
Let V be given.
Assume HV: V ∈ R_standard_topology.
We prove the intermediate claim HpreEq: preimage_of X f V = preimage_of X g V.
Apply set_ext to the current goal.
Let x0 be given.
Assume Hx0: x0 ∈ preimage_of X f V.
We will prove x0 ∈ preimage_of X g V.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λx1 : set ⇒ apply_fun f x1 ∈ V) x0 Hx0).
We prove the intermediate claim Hfx0: apply_fun f x0 ∈ V.
An exact proof term for the current goal is (SepE2 X (λx1 : set ⇒ apply_fun f x1 ∈ V) x0 Hx0).
We prove the intermediate claim Happ: apply_fun f x0 = apply_fun g x0.
We prove the intermediate claim H1: apply_fun f x0 = h x0.
An exact proof term for the current goal is (apply_fun_graph X h x0 Hx0X).
rewrite the current goal using H1 (from left to right).
Use reflexivity.
We prove the intermediate claim Hgx0V: apply_fun g x0 ∈ V.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is Hfx0.
An exact proof term for the current goal is (SepI X (λx1 : set ⇒ apply_fun g x1 ∈ V) x0 Hx0X Hgx0V).
Let x0 be given.
Assume Hx0: x0 ∈ preimage_of X g V.
We will prove x0 ∈ preimage_of X f V.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λx1 : set ⇒ apply_fun g x1 ∈ V) x0 Hx0).
We prove the intermediate claim Hgx0: apply_fun g x0 ∈ V.
An exact proof term for the current goal is (SepE2 X (λx1 : set ⇒ apply_fun g x1 ∈ V) x0 Hx0).
We prove the intermediate claim Happ: apply_fun f x0 = apply_fun g x0.
We prove the intermediate claim H1: apply_fun f x0 = h x0.
An exact proof term for the current goal is (apply_fun_graph X h x0 Hx0X).
rewrite the current goal using H1 (from left to right).
Use reflexivity.
We prove the intermediate claim Hfx0V: apply_fun f x0 ∈ V.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is Hgx0.
An exact proof term for the current goal is (SepI X (λx1 : set ⇒ apply_fun f x1 ∈ V) x0 Hx0X Hfx0V).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology g HgcontR V HV).
Let x0 be given.
Assume Hx0: x0 ∈ (X ∖ (proj1 p)).
We will prove apply_fun f x0 = 0.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (setminusE1 X (proj1 p) x0 Hx0).
We prove the intermediate claim Happ: apply_fun f x0 = h x0.
An exact proof term for the current goal is (apply_fun_graph X h x0 Hx0X).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (Hg0 x0 Hx0).
Let x0 be given.
Assume Hx0: x0 ∈ closure_of X Tx (proj0 p).
We will prove apply_fun f x0 = 1.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λx1 : set ⇒ ∀U : set, U ∈ Tx → x1 ∈ U → U ∩ (proj0 p) ≠ Empty) x0 Hx0).
We prove the intermediate claim Happ: apply_fun f x0 = h x0.
An exact proof term for the current goal is (apply_fun_graph X h x0 Hx0X).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (Hg1 x0 Hx0).
We prove the intermediate claim Hbump_mem: ∀p : set, bump p ∈ function_space X R.
Let p be given.
Apply (xm (p ∈ P)) to the current goal.
Assume HpP: p ∈ P.
We prove the intermediate claim HbDef: bump p = Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)).
We prove the intermediate claim Hb: bump = (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p0)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p0) → apply_fun f x0 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hb (from left to right).
We prove the intermediate claim Hbeta_bump: (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p0)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p0) → apply_fun f x0 = 1)) else const_fun X 0) p = (if p ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hbeta_bump (from left to right).
rewrite the current goal using (If_i_1 (p ∈ P) (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))) (const_fun X 0) HpP) (from left to right).
Use reflexivity.
rewrite the current goal using HbDef (from left to right).
We prove the intermediate claim Hex: ∃f : set, f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1).
An exact proof term for the current goal is (Hbump_ex p HpP).
We prove the intermediate claim Hprop: (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))) ∈ function_space X R.
Set Ep to be the term (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))).
We prove the intermediate claim HEp: Ep = (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))).
Use reflexivity.
rewrite the current goal using HEp (from right to left).
We prove the intermediate claim Htmp: (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) Ep.
rewrite the current goal using HEp (from left to right).
An exact proof term for the current goal is (Eps_i_ex (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) Hex).
We prove the intermediate claim Htmp123: (Ep ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology Ep) ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun Ep x0 = 0).
An exact proof term for the current goal is (andEL ((Ep ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology Ep) ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun Ep x0 = 0)) (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun Ep x0 = 1) Htmp).
We prove the intermediate claim Htmp12: Ep ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology Ep.
An exact proof term for the current goal is (andEL (Ep ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology Ep) (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun Ep x0 = 0) Htmp123).
An exact proof term for the current goal is (andEL (Ep ∈ function_space X R) (continuous_map X Tx R R_standard_topology Ep) Htmp12).
An exact proof term for the current goal is Hprop.
Assume HpN: p ∉ P.
We prove the intermediate claim HbDef: bump p = const_fun X 0.
We prove the intermediate claim Hb: bump = (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p0)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p0) → apply_fun f x0 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hb (from left to right).
We prove the intermediate claim Hbeta_bump0: (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p0)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p0) → apply_fun f x0 = 1)) else const_fun X 0) p = (if p ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hbeta_bump0 (from left to right).
rewrite the current goal using (If_i_0 (p ∈ P) (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))) (const_fun X 0) HpN) (from left to right).
Use reflexivity.
rewrite the current goal using HbDef (from left to right).
An exact proof term for the current goal is HconstFS.
We prove the intermediate claim Hbump_cont: ∀p : set, continuous_map X Tx R R_standard_topology (bump p).
Let p be given.
Apply (xm (p ∈ P)) to the current goal.
Assume HpP: p ∈ P.
We prove the intermediate claim HbDef: bump p = Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)).
We prove the intermediate claim Hb: bump = (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p0)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p0) → apply_fun f x0 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hb (from left to right).
We prove the intermediate claim Hbeta_bump: (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p0)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p0) → apply_fun f x0 = 1)) else const_fun X 0) p = (if p ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hbeta_bump (from left to right).
rewrite the current goal using (If_i_1 (p ∈ P) (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))) (const_fun X 0) HpP) (from left to right).
Use reflexivity.
rewrite the current goal using HbDef (from left to right).
We prove the intermediate claim Hex: ∃f : set, f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1).
An exact proof term for the current goal is (Hbump_ex p HpP).
We prove the intermediate claim Htmp: (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))).
An exact proof term for the current goal is (Eps_i_ex (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) Hex).
We prove the intermediate claim Hcont: continuous_map X Tx R R_standard_topology (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))).
Set Ep to be the term (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))).
We prove the intermediate claim HEp: Ep = (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))).
Use reflexivity.
rewrite the current goal using HEp (from right to left).
We prove the intermediate claim Htmp0: (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) Ep.
rewrite the current goal using HEp (from left to right).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Htmp123: (Ep ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology Ep) ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun Ep x0 = 0).
An exact proof term for the current goal is (andEL ((Ep ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology Ep) ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun Ep x0 = 0)) (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun Ep x0 = 1) Htmp0).
We prove the intermediate claim Htmp12: Ep ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology Ep.
An exact proof term for the current goal is (andEL (Ep ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology Ep) (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun Ep x0 = 0) Htmp123).
An exact proof term for the current goal is (andER (Ep ∈ function_space X R) (continuous_map X Tx R R_standard_topology Ep) Htmp12).
An exact proof term for the current goal is Hcont.
Assume HpN: p ∉ P.
We prove the intermediate claim HbDef: bump p = const_fun X 0.
We prove the intermediate claim Hb: bump = (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p0)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p0) → apply_fun f x0 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hb (from left to right).
We prove the intermediate claim Hbeta_bump0: (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p0)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p0) → apply_fun f x0 = 1)) else const_fun X 0) p = (if p ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hbeta_bump0 (from left to right).
rewrite the current goal using (If_i_0 (p ∈ P) (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x0 : set, x0 ∈ (X ∖ (proj1 p)) → apply_fun f x0 = 0) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (proj0 p) → apply_fun f x0 = 1))) (const_fun X 0) HpN) (from left to right).
Use reflexivity.
rewrite the current goal using HbDef (from left to right).
An exact proof term for the current goal is HconstCont.
We will prove (((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 → ∀U : set, U ∈ Tx → x0 ∈ U → ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x0) ∧ ∀x : set, x ∈ X ∖ U → apply_fun (apply_fun F j) x = 0)).
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 Hfun: function_on F J (function_space X R).
Let n be given.
Assume HnJ: n ∈ J.
We will prove apply_fun F n ∈ function_space X R.
We prove the intermediate claim HFdef: F = graph J (λn0 : set ⇒ bump (pair_of n0)).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
We prove the intermediate claim Happ: apply_fun (graph J (λn0 : set ⇒ bump (pair_of n0))) n = bump (pair_of n).
An exact proof term for the current goal is (apply_fun_graph J (λn0 : set ⇒ bump (pair_of n0)) n HnJ).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (Hbump_mem (pair_of n)).
We prove the intermediate claim Htot': ∀n : set, n ∈ J → ∃y : set, y ∈ function_space X R ∧ (n,y) ∈ F.
Let n be given.
Assume HnJ: n ∈ J.
We use (bump (pair_of n)) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (Hbump_mem (pair_of n)).
We prove the intermediate claim HFdef: F = graph J (λn0 : set ⇒ bump (pair_of n0)).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
An exact proof term for the current goal is (ReplI J (λa0 : set ⇒ (a0,bump (pair_of a0))) n HnJ).
An exact proof term for the current goal is (andI (function_on F J (function_space X R)) (∀x : set, x ∈ J → ∃y : set, y ∈ function_space X R ∧ (x,y) ∈ F) Hfun Htot').
Let n be given.
Assume HnJ: n ∈ J.
We will prove continuous_map X Tx R R_standard_topology (apply_fun F n).
We prove the intermediate claim HFdef: F = graph J (λn0 : set ⇒ bump (pair_of n0)).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
We prove the intermediate claim Happ: apply_fun (graph J (λn0 : set ⇒ bump (pair_of n0))) n = (λn0 : set ⇒ bump (pair_of n0)) n.
An exact proof term for the current goal is (apply_fun_graph J (λn0 : set ⇒ bump (pair_of n0)) n HnJ).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hbeta: (λn0 : set ⇒ bump (pair_of n0)) n = bump (pair_of n).
Use reflexivity.
rewrite the current goal using Hbeta (from left to right).
An exact proof term for the current goal is (Hbump_cont (pair_of n)).
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Let U be given.
Assume HUtx: U ∈ Tx.
Assume Hx0U: x0 ∈ U.
We prove the intermediate claim HUgen: U ∈ generated_topology X B.
rewrite the current goal using HgenEq (from left to right).
An exact proof term for the current goal is HUtx.
We prove the intermediate claim HUloc: ∀x : set, x ∈ U → ∃b : set, b ∈ B ∧ x ∈ b ∧ b ⊆ U.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim Hprop: ∀x1 ∈ U, ∃b ∈ B, x1 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x1 ∈ U0, ∃b ∈ B, x1 ∈ b ∧ b ⊆ U0) U HUgen).
Apply (Hprop x HxU) to the current goal.
Let b be given.
Assume Hbpack.
We use b 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 (andEL (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpack).
We prove the intermediate claim Hbrest: x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpack).
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbrest).
We prove the intermediate claim Hbrest: x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpack).
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbrest).
Apply (HUloc x0 Hx0U) to the current goal.
Let V be given.
Assume HVpack.
We prove the intermediate claim HVpack12: V ∈ B ∧ x0 ∈ V.
An exact proof term for the current goal is (andEL (V ∈ B ∧ x0 ∈ V) (V ⊆ U) HVpack).
We prove the intermediate claim HVsubU: V ⊆ U.
An exact proof term for the current goal is (andER (V ∈ B ∧ x0 ∈ V) (V ⊆ U) HVpack).
We prove the intermediate claim HVB: V ∈ B.
An exact proof term for the current goal is (andEL (V ∈ B) (x0 ∈ V) HVpack12).
We prove the intermediate claim Hx0V: x0 ∈ V.
An exact proof term for the current goal is (andER (V ∈ B) (x0 ∈ V) HVpack12).
We prove the intermediate claim HVgen: V ∈ generated_topology X B.
An exact proof term for the current goal is (basis_in_generated X B V HB HVB).
We prove the intermediate claim HVtx: V ∈ Tx.
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HVgen.
We prove the intermediate claim HexW: ∃W : set, W ∈ Tx ∧ x0 ∈ W ∧ closure_of X Tx W ⊆ V.
An exact proof term for the current goal is (regular_space_shrink_neighborhood X Tx x0 V Hreg Hx0X HVtx Hx0V).
Apply HexW to the current goal.
Let W be given.
Assume HWpack.
We prove the intermediate claim HWpack12: W ∈ Tx ∧ x0 ∈ W.
An exact proof term for the current goal is (andEL (W ∈ Tx ∧ x0 ∈ W) (closure_of X Tx W ⊆ V) HWpack).
We prove the intermediate claim HclWsubV: closure_of X Tx W ⊆ V.
An exact proof term for the current goal is (andER (W ∈ Tx ∧ x0 ∈ W) (closure_of X Tx W ⊆ V) HWpack).
We prove the intermediate claim HWtx: W ∈ Tx.
An exact proof term for the current goal is (andEL (W ∈ Tx) (x0 ∈ W) HWpack12).
We prove the intermediate claim Hx0W: x0 ∈ W.
An exact proof term for the current goal is (andER (W ∈ Tx) (x0 ∈ W) HWpack12).
We prove the intermediate claim HWgen: W ∈ generated_topology X B.
rewrite the current goal using HgenEq (from left to right).
An exact proof term for the current goal is HWtx.
We prove the intermediate claim HWloc: ∀x : set, x ∈ W → ∃b : set, b ∈ B ∧ x ∈ b ∧ b ⊆ W.
Let x be given.
Assume HxW: x ∈ W.
We prove the intermediate claim Hprop: ∀x1 ∈ W, ∃b ∈ B, x1 ∈ b ∧ b ⊆ W.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x1 ∈ U0, ∃b ∈ B, x1 ∈ b ∧ b ⊆ U0) W HWgen).
Apply (Hprop x HxW) to the current goal.
Let b be given.
Assume Hbpack.
We use b 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 (andEL (b ∈ B) (x ∈ b ∧ b ⊆ W) Hbpack).
We prove the intermediate claim Hbrest: x ∈ b ∧ b ⊆ W.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ W) Hbpack).
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ W) Hbrest).
We prove the intermediate claim Hbrest: x ∈ b ∧ b ⊆ W.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ W) Hbpack).
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ W) Hbrest).
Apply (HWloc x0 Hx0W) to the current goal.
Let U0 be given.
Assume HU0pack.
We prove the intermediate claim HU0pack12: U0 ∈ B ∧ x0 ∈ U0.
An exact proof term for the current goal is (andEL (U0 ∈ B ∧ x0 ∈ U0) (U0 ⊆ W) HU0pack).
We prove the intermediate claim HU0subW: U0 ⊆ W.
An exact proof term for the current goal is (andER (U0 ∈ B ∧ x0 ∈ U0) (U0 ⊆ W) HU0pack).
We prove the intermediate claim HU0B: U0 ∈ B.
An exact proof term for the current goal is (andEL (U0 ∈ B) (x0 ∈ U0) HU0pack12).
We prove the intermediate claim Hx0U0: x0 ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ B) (x0 ∈ U0) HU0pack12).
We prove the intermediate claim HWsubX: W ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx W HTx HWtx).
We prove the intermediate claim HclU0subclW: closure_of X Tx U0 ⊆ closure_of X Tx W.
An exact proof term for the current goal is (closure_monotone X Tx U0 W HTx HU0subW HWsubX).
We prove the intermediate claim HclU0subV: closure_of X Tx U0 ⊆ V.
An exact proof term for the current goal is (Subq_tra (closure_of X Tx U0) (closure_of X Tx W) V HclU0subclW HclWsubV).
Set p to be the term (U0,V).
We prove the intermediate claim Hpdef: p = (U0,V).
Use reflexivity.
We prove the intermediate claim HpBB: p ∈ (B ⨯ B).
An exact proof term for the current goal is (tuple_2_setprod B B U0 HU0B V HVB).
We prove the intermediate claim HpP: p ∈ P.
We prove the intermediate claim HpProp: closure_of X Tx (proj0 p) ⊆ proj1 p.
rewrite the current goal using Hpdef (from left to right).
rewrite the current goal using (tuple_pair U0 V) (from right to left).
rewrite the current goal using (proj0_pair_eq U0 V) (from left to right).
rewrite the current goal using (proj1_pair_eq U0 V) (from left to right).
An exact proof term for the current goal is HclU0subV.
An exact proof term for the current goal is (SepI (B ⨯ B) (λp0 : set ⇒ closure_of X Tx (proj0 p0) ⊆ proj1 p0) p HpBB HpProp).
Set j to be the term enc p.
We prove the intermediate claim Hjdef: j = enc p.
Use reflexivity.
We prove the intermediate claim HJdef: J = ω.
Use reflexivity.
We prove the intermediate claim Henc_dom: ∀u ∈ P, enc u ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ P, enc u ∈ ω) (∀u v ∈ P, enc u = enc v → u = v) Henc).
We prove the intermediate claim HjJ: j ∈ J.
rewrite the current goal using HJdef (from left to right).
rewrite the current goal using Hjdef (from left to right).
An exact proof term for the current goal is (Henc_dom p HpP).
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 HFdef: F = graph J (λn0 : set ⇒ bump (pair_of n0)).
Use reflexivity.
We prove the intermediate claim HpairEq: pair_of j = p.
We prove the intermediate claim Hinj: ∀u v ∈ P, enc u = enc v → u = v.
An exact proof term for the current goal is (andER (∀u ∈ P, enc u ∈ ω) (∀u v ∈ P, enc u = enc v → u = v) Henc).
We prove the intermediate claim HinvEq: inv P enc (enc p) = p.
An exact proof term for the current goal is (inj_linv P enc Hinj p HpP).
rewrite the current goal using Hjdef (from left to right).
An exact proof term for the current goal is HinvEq.
We prove the intermediate claim Hfj: apply_fun F j = bump p.
rewrite the current goal using HFdef (from left to right).
We prove the intermediate claim Happ: apply_fun (graph J (λn0 : set ⇒ bump (pair_of n0))) j = (λn0 : set ⇒ bump (pair_of n0)) j.
An exact proof term for the current goal is (apply_fun_graph J (λn0 : set ⇒ bump (pair_of n0)) j HjJ).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hbeta: (λn0 : set ⇒ bump (pair_of n0)) j = bump (pair_of j).
Use reflexivity.
rewrite the current goal using Hbeta (from left to right).
rewrite the current goal using HpairEq (from left to right).
Use reflexivity.
We prove the intermediate claim Hclx0: x0 ∈ closure_of X Tx U0.
We prove the intermediate claim HU0subX: U0 ⊆ X.
An exact proof term for the current goal is (basis_elem_subset X B U0 HB HU0B).
An exact proof term for the current goal is (subset_of_closure X Tx U0 HTx HU0subX x0 Hx0U0).
We prove the intermediate claim HbDef: bump p = Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1)).
We prove the intermediate claim Hb: bump = (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p0)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p0) → apply_fun f x1 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hb (from left to right).
We prove the intermediate claim Hbeta_bump_p: (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p0)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p0) → apply_fun f x1 = 1)) else const_fun X 0) p = (if p ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hbeta_bump_p (from left to right).
rewrite the current goal using (If_i_1 (p ∈ P) (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) (const_fun X 0) HpP) (from left to right).
Use reflexivity.
We prove the intermediate claim Hex: ∃f : set, f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1).
An exact proof term for the current goal is (Hbump_ex p HpP).
We prove the intermediate claim Htmp: (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1)) (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))).
An exact proof term for the current goal is (Eps_i_ex (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1)) Hex).
We prove the intermediate claim Hval: apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x0 = 1.
We prove the intermediate claim Hrest: (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 1).
We prove the intermediate claim Hmid: (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 1).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hrest2: (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 1).
An exact proof term for the current goal is (andER ((Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 0)) (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 1) Hmid).
An exact proof term for the current goal is Hrest2.
Apply (Hrest x0) to the current goal.
rewrite the current goal using Hpdef (from left to right).
rewrite the current goal using (tuple_pair U0 V) (from right to left).
rewrite the current goal using (proj0_pair_eq U0 V) (from left to right).
An exact proof term for the current goal is Hclx0.
We prove the intermediate claim Hx01: apply_fun (apply_fun F j) x0 = 1.
rewrite the current goal using Hfj (from left to right) at position 1.
rewrite the current goal using HbDef (from left to right) at position 1.
An exact proof term for the current goal is Hval.
We prove the intermediate claim Hpos: Rlt 0 (apply_fun (apply_fun F j) x0).
rewrite the current goal using Hx01 (from left to right).
An exact proof term for the current goal is Rlt_0_1.
An exact proof term for the current goal is Hpos.
Let x be given.
Assume HxOut: x ∈ X ∖ U.
We prove the intermediate claim HxOutV: x ∈ X ∖ V.
An exact proof term for the current goal is (setminus_antimonotone X V U HVsubU x HxOut).
We prove the intermediate claim HFdef: F = graph J (λn0 : set ⇒ bump (pair_of n0)).
Use reflexivity.
We prove the intermediate claim HpairEq: pair_of j = p.
We prove the intermediate claim Hinj: ∀u v ∈ P, enc u = enc v → u = v.
An exact proof term for the current goal is (andER (∀u ∈ P, enc u ∈ ω) (∀u v ∈ P, enc u = enc v → u = v) Henc).
We prove the intermediate claim HinvEq: inv P enc (enc p) = p.
An exact proof term for the current goal is (inj_linv P enc Hinj p HpP).
rewrite the current goal using Hjdef (from left to right).
An exact proof term for the current goal is HinvEq.
We prove the intermediate claim Hfj: apply_fun F j = bump p.
rewrite the current goal using HFdef (from left to right).
We prove the intermediate claim Happ: apply_fun (graph J (λn0 : set ⇒ bump (pair_of n0))) j = (λn0 : set ⇒ bump (pair_of n0)) j.
An exact proof term for the current goal is (apply_fun_graph J (λn0 : set ⇒ bump (pair_of n0)) j HjJ).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hbeta: (λn0 : set ⇒ bump (pair_of n0)) j = bump (pair_of j).
Use reflexivity.
rewrite the current goal using Hbeta (from left to right).
rewrite the current goal using HpairEq (from left to right).
Use reflexivity.
We prove the intermediate claim HbDef: bump p = Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1)).
We prove the intermediate claim Hb: bump = (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p0)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p0) → apply_fun f x1 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hb (from left to right).
We prove the intermediate claim Hbeta_bump_p: (λp0 : set ⇒ if p0 ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p0)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p0) → apply_fun f x1 = 1)) else const_fun X 0) p = (if p ∈ P then Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1)) else const_fun X 0).
Use reflexivity.
rewrite the current goal using Hbeta_bump_p (from left to right).
rewrite the current goal using (If_i_1 (p ∈ P) (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) (const_fun X 0) HpP) (from left to right).
Use reflexivity.
rewrite the current goal using Hfj (from left to right).
rewrite the current goal using HbDef (from left to right).
We prove the intermediate claim Hex: ∃f : set, f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1).
An exact proof term for the current goal is (Hbump_ex p HpP).
We prove the intermediate claim Htmp: (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1)) (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))).
An exact proof term for the current goal is (Eps_i_ex (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1)) Hex).
We prove the intermediate claim Hzero: ∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 0.
We prove the intermediate claim Hmid: (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 1).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hrest: (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 0).
We prove the intermediate claim Hmid123: (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 0).
An exact proof term for the current goal is (andEL ((Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 0)) (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 1) Hmid).
An exact proof term for the current goal is (andER ((Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1)))) (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x1 = 0) Hmid123).
An exact proof term for the current goal is Hrest.
We prove the intermediate claim Hx0: apply_fun (Eps_i (λf : set ⇒ f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x1 : set, x1 ∈ (X ∖ (proj1 p)) → apply_fun f x1 = 0) ∧ (∀x1 : set, x1 ∈ closure_of X Tx (proj0 p) → apply_fun f x1 = 1))) x = 0.
Apply (Hzero x) to the current goal.
rewrite the current goal using Hpdef (from left to right).
rewrite the current goal using (tuple_pair U0 V) (from right to left).
rewrite the current goal using (proj1_pair_eq U0 V) (from left to right).
An exact proof term for the current goal is HxOutV.
An exact proof term for the current goal is Hx0.
Apply HexSep to the current goal.
Let F be given.
Assume Hsep: separating_family_of_functions X Tx F J.
Set Fmap to be the term diagonal_map X F J.
We prove the intermediate claim HFmap: embedding_of X Tx (power_real J) (product_topology_full J (const_space_family J R R_standard_topology)) Fmap.
Set Xi to be the term const_space_family J R R_standard_topology.
Set Ty0 to be the term product_topology_full J Xi.
We prove the intermediate claim HcontFmap: continuous_map X Tx (power_real J) Ty0 Fmap.
We prove the intermediate claim HpR: power_real J = product_space J Xi.
Use reflexivity.
We prove the intermediate claim HTyDef: Ty0 = product_topology_full J Xi.
Use reflexivity.
rewrite the current goal using HpR (from left to right).
rewrite the current goal using HTyDef (from left to right).
We will prove continuous_map X Tx (product_space J Xi) (product_topology_full J Xi) Fmap.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HsepCore: (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)).
An exact proof term for the current goal is (andEL ((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))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x0) ∧ ∀x1 : set, x1 ∈ X ∖ U0 → apply_fun (apply_fun F j0) x1 = 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)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepCore).
We prove the intermediate claim Htot: 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 HfunPow: function_on Fmap X (power_real J).
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_function_on_power_real X F J Htot).
We prove the intermediate claim Hfun: function_on Fmap X (product_space J Xi).
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun Fmap x ∈ product_space J Xi.
rewrite the current goal using HpR (from right to left).
An exact proof term for the current goal is (HfunPow x HxX).
Apply (xm (J = Empty)) to the current goal.
Assume HJ0: J = Empty.
rewrite the current goal using HJ0 (from left to right).
We prove the intermediate claim HTy0: topology_on (product_space Empty Xi) (product_topology_full Empty Xi).
An exact proof term for the current goal is (product_topology_full_empty_is_topology Xi).
We prove the intermediate claim HX0: product_space Empty Xi = {Empty}.
An exact proof term for the current goal is (product_space_empty_index Xi).
We prove the intermediate claim HEmptyY: Empty ∈ product_space Empty Xi.
rewrite the current goal using HX0 (from left to right).
An exact proof term for the current goal is (SingI Empty).
We prove the intermediate claim HXieq: Xi = const_space_family Empty R R_standard_topology.
We prove the intermediate claim HXidef: Xi = const_space_family J R R_standard_topology.
Use reflexivity.
rewrite the current goal using HXidef (from left to right).
rewrite the current goal using HJ0 (from left to right).
Use reflexivity.
We prove the intermediate claim HFmapConst: Fmap = const_fun X Empty.
We prove the intermediate claim HFmapE: Fmap = diagonal_map X F Empty.
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HJ0 (from left to right).
Use reflexivity.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ Fmap.
We will prove p ∈ const_fun X Empty.
We prove the intermediate claim HpDiag: p ∈ diagonal_map X F Empty.
rewrite the current goal using HFmapE (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Hdiag0: diagonal_map X F Empty = graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HpGraph: p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
rewrite the current goal using Hdiag0 (from right to left).
An exact proof term for the current goal is HpDiag.
Apply (ReplE_impred X (λx0 : set ⇒ (x0,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0))) p HpGraph (p ∈ const_fun X Empty)) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume Hpeq: p = (x0,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
We prove the intermediate claim Hem: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0) = Empty.
We prove the intermediate claim HgraphDef: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0) = {(j0,apply_fun (apply_fun F j0) x0)|j0 ∈ Empty}.
Use reflexivity.
rewrite the current goal using HgraphDef (from left to right).
An exact proof term for the current goal is (Repl_Empty (λj0 : set ⇒ (j0,apply_fun (apply_fun F j0) x0))).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Hem (from left to right).
An exact proof term for the current goal is (ReplI X (λa0 : set ⇒ (a0,Empty)) x0 Hx0X).
Let p be given.
Assume Hp: p ∈ const_fun X Empty.
We will prove p ∈ Fmap.
We prove the intermediate claim HFmapE: Fmap = diagonal_map X F Empty.
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HJ0 (from left to right).
Use reflexivity.
We prove the intermediate claim Hdiag0: diagonal_map X F Empty = graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HpGraph: p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Apply (ReplE_impred X (λa0 : set ⇒ (a0,Empty)) p Hp (p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)))) to the current goal.
Let x2 be given.
Assume Hx2X: x2 ∈ X.
Assume Hpeq: p = (x2,Empty).
We prove the intermediate claim Hem: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2) = Empty.
We prove the intermediate claim HgraphDef: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2) = {(j0,apply_fun (apply_fun F j0) x2)|j0 ∈ Empty}.
Use reflexivity.
rewrite the current goal using HgraphDef (from left to right).
An exact proof term for the current goal is (Repl_Empty (λj0 : set ⇒ (j0,apply_fun (apply_fun F j0) x2))).
We prove the intermediate claim HpEq2: p = (x2,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2)).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Hem (from left to right).
Use reflexivity.
rewrite the current goal using HpEq2 (from left to right).
An exact proof term for the current goal is (ReplI X (λx1 : set ⇒ (x1,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x1))) x2 Hx2X).
We prove the intermediate claim HpDiag: p ∈ diagonal_map X F Empty.
rewrite the current goal using Hdiag0 (from left to right).
An exact proof term for the current goal is HpGraph.
rewrite the current goal using HFmapE (from left to right).
An exact proof term for the current goal is HpDiag.
We prove the intermediate claim HdiagConst: diagonal_map X F Empty = const_fun X Empty.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ diagonal_map X F Empty.
We will prove p ∈ const_fun X Empty.
We prove the intermediate claim Hdiag0: diagonal_map X F Empty = graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HpGraph: p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
rewrite the current goal using Hdiag0 (from right to left).
An exact proof term for the current goal is Hp.
Apply (ReplE_impred X (λx0 : set ⇒ (x0,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0))) p HpGraph (p ∈ const_fun X Empty)) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume Hpeq: p = (x0,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
We prove the intermediate claim Hem: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0) = Empty.
We prove the intermediate claim HgraphDef: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0) = {(j0,apply_fun (apply_fun F j0) x0)|j0 ∈ Empty}.
Use reflexivity.
rewrite the current goal using HgraphDef (from left to right).
An exact proof term for the current goal is (Repl_Empty (λj0 : set ⇒ (j0,apply_fun (apply_fun F j0) x0))).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Hem (from left to right).
An exact proof term for the current goal is (ReplI X (λa0 : set ⇒ (a0,Empty)) x0 Hx0X).
Let p be given.
Assume Hp: p ∈ const_fun X Empty.
We will prove p ∈ diagonal_map X F Empty.
We prove the intermediate claim Hdiag0: diagonal_map X F Empty = graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HpGraph: p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Apply (ReplE_impred X (λa0 : set ⇒ (a0,Empty)) p Hp (p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)))) to the current goal.
Let x2 be given.
Assume Hx2X: x2 ∈ X.
Assume Hpeq: p = (x2,Empty).
We prove the intermediate claim Hem: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2) = Empty.
We prove the intermediate claim HgraphDef: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2) = {(j0,apply_fun (apply_fun F j0) x2)|j0 ∈ Empty}.
Use reflexivity.
rewrite the current goal using HgraphDef (from left to right).
An exact proof term for the current goal is (Repl_Empty (λj0 : set ⇒ (j0,apply_fun (apply_fun F j0) x2))).
We prove the intermediate claim HpEq2: p = (x2,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2)).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Hem (from left to right).
Use reflexivity.
rewrite the current goal using HpEq2 (from left to right).
An exact proof term for the current goal is (ReplI X (λx1 : set ⇒ (x1,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x1))) x2 Hx2X).
rewrite the current goal using Hdiag0 (from left to right).
An exact proof term for the current goal is HpGraph.
We prove the intermediate claim Hconst: continuous_map X Tx (product_space Empty Xi) (product_topology_full Empty Xi) (const_fun X Empty).
An exact proof term for the current goal is (const_fun_continuous X Tx (product_space Empty Xi) (product_topology_full Empty Xi) Empty HTx HTy0 HEmptyY).
rewrite the current goal using HdiagConst (from left to right).
rewrite the current goal using HXieq (from right to left).
An exact proof term for the current goal is Hconst.
Assume HJne: J ≠ Empty.
We prove the intermediate claim HcompTop: ∀i : set, i ∈ J → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiJ: i ∈ J.
We prove the intermediate claim Hset: space_family_set Xi i = R.
An exact proof term for the current goal is (space_family_set_const_space_family J R R_standard_topology i HiJ).
We prove the intermediate claim Htop: space_family_topology Xi i = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology i HiJ).
rewrite the current goal using Hset (from left to right).
rewrite the current goal using Htop (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HSsub: subbasis_on (product_space J Xi) (product_subbasis_full J Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on J Xi HJne HcompTop).
We prove the intermediate claim HcontCoord: ∀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)) HsepCore).
Apply (continuous_map_from_subbasis X Tx (product_space J Xi) (product_subbasis_full J Xi) Fmap HTx Hfun HSsub) to the current goal.
Let s be given.
Assume HsS: s ∈ product_subbasis_full J Xi.
We will prove preimage_of X Fmap s ∈ Tx.
Set Fam to be the term (λi0 : set ⇒ {product_cylinder J Xi i0 U0|U0 ∈ space_family_topology Xi i0}).
We prove the intermediate claim HsFam: s ∈ (⋃i0 ∈ JFam i0).
An exact proof term for the current goal is HsS.
Apply (famunionE_impred J Fam s HsFam (preimage_of X Fmap s ∈ Tx)) to the current goal.
Let i be given.
Assume HiJ: i ∈ J.
Assume HsFi: s ∈ Fam i.
We prove the intermediate claim HexU: ∃U ∈ space_family_topology Xi i, s = product_cylinder J Xi i U.
An exact proof term for the current goal is (ReplE (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder J Xi i U0) s HsFi).
Apply HexU to the current goal.
Let U be given.
Assume HUand: U ∈ space_family_topology Xi i ∧ s = product_cylinder J Xi i U.
We prove the intermediate claim HUtop: U ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (U ∈ space_family_topology Xi i) (s = product_cylinder J Xi i U) HUand).
We prove the intermediate claim Hseq: s = product_cylinder J Xi i U.
An exact proof term for the current goal is (andER (U ∈ space_family_topology Xi i) (s = product_cylinder J Xi i U) HUand).
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim Hconti: continuous_map X Tx R R_standard_topology (apply_fun F i).
An exact proof term for the current goal is (HcontCoord i HiJ).
We prove the intermediate claim HUstd: U ∈ R_standard_topology.
We prove the intermediate claim Htopi: space_family_topology Xi i = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology i HiJ).
rewrite the current goal using Htopi (from right to left).
An exact proof term for the current goal is HUtop.
We prove the intermediate claim HpreEq: preimage_of X Fmap (product_cylinder J Xi i U) = preimage_of X (apply_fun F i) U.
Apply set_ext to the current goal.
Let x be given.
Assume HxPre: x ∈ preimage_of X Fmap (product_cylinder J Xi i U).
We will prove x ∈ preimage_of X (apply_fun F i) U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun Fmap x0 ∈ product_cylinder J Xi i U) x HxPre).
We prove the intermediate claim HfxCyl: apply_fun Fmap x ∈ product_cylinder J Xi i U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun Fmap x0 ∈ product_cylinder J Xi i U) x HxPre).
We prove the intermediate claim HcylProp: i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun (apply_fun Fmap x) i ∈ U.
An exact proof term for the current goal is (SepE2 (product_space J Xi) (λf0 : set ⇒ i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) (apply_fun Fmap x) HfxCyl).
We prove the intermediate claim HcoordU: apply_fun (apply_fun Fmap x) i ∈ U.
We prove the intermediate claim H12: i ∈ J ∧ U ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (i ∈ J ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun Fmap x) i ∈ U) HcylProp).
An exact proof term for the current goal is (andER (i ∈ J ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun Fmap x) i ∈ U) HcylProp).
We prove the intermediate claim HFmapx: apply_fun Fmap x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun Fmap x) i = apply_fun (apply_fun F i) x.
rewrite the current goal using HFmapx (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) i HiJ) (from left to right).
Use reflexivity.
We prove the intermediate claim HfiU: apply_fun (apply_fun F i) x ∈ U.
rewrite the current goal using HcoordEq (from right to left).
An exact proof term for the current goal is HcoordU.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun (apply_fun F i) x0 ∈ U) x HxX HfiU).
Let x be given.
Assume HxPre: x ∈ preimage_of X (apply_fun F i) U.
We will prove x ∈ preimage_of X Fmap (product_cylinder J Xi i U).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun (apply_fun F i) x0 ∈ U) x HxPre).
We prove the intermediate claim HfiU: apply_fun (apply_fun F i) x ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (apply_fun F i) x0 ∈ U) x HxPre).
We prove the intermediate claim HFmapx: apply_fun Fmap x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun Fmap x) i = apply_fun (apply_fun F i) x.
rewrite the current goal using HFmapx (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) i HiJ) (from left to right).
Use reflexivity.
We prove the intermediate claim HcoordU: apply_fun (apply_fun Fmap x) i ∈ U.
rewrite the current goal using HcoordEq (from left to right).
An exact proof term for the current goal is HfiU.
We prove the intermediate claim Hpred: i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun (apply_fun Fmap x) i ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HiJ.
An exact proof term for the current goal is HUtop.
An exact proof term for the current goal is HcoordU.
We prove the intermediate claim HfxCyl: apply_fun Fmap x ∈ product_cylinder J Xi i U.
An exact proof term for the current goal is (SepI (product_space J Xi) (λf0 : set ⇒ i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) (apply_fun Fmap x) (Hfun x HxX) Hpred).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun Fmap x0 ∈ product_cylinder J Xi i U) x HxX HfxCyl).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology (apply_fun F i) Hconti U HUstd).
We prove the intermediate claim HlocFmap: ∀x U : set, x ∈ X → U ∈ Tx → x ∈ U → ∃V : set, V ∈ Ty0 ∧ apply_fun Fmap x ∈ V ∧ preimage_of X Fmap V ⊆ U.
Let x be given.
Let U be given.
Assume HxX: x ∈ X.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim HsepCore: ((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))).
An exact proof term for the current goal is (andEL (((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)))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x0) ∧ ∀x1 : set, x1 ∈ X ∖ U0 → apply_fun (apply_fun F j0) x1 = 0) Hsep).
We prove the intermediate claim Hneigh: ∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x0) ∧ ∀x1 : set, x1 ∈ X ∖ U0 → apply_fun (apply_fun F j0) x1 = 0.
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)))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x0) ∧ ∀x1 : set, x1 ∈ X ∖ U0 → apply_fun (apply_fun F j0) x1 = 0) Hsep).
We prove the intermediate claim Hexj: ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x) ∧ ∀x1 : set, x1 ∈ X ∖ U → apply_fun (apply_fun F j0) x1 = 0.
An exact proof term for the current goal is (Hneigh x HxX U HU HxU).
Apply Hexj to the current goal.
Let j be given.
Assume Hjpack.
We prove the intermediate claim Hj12: 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)) (∀x1 : set, x1 ∈ X ∖ U → apply_fun (apply_fun F j) x1 = 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)) Hj12).
We prove the intermediate claim Hjpos: 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)) Hj12).
We prove the intermediate claim Hjzero: ∀x1 : set, x1 ∈ X ∖ U → apply_fun (apply_fun F j) x1 = 0.
An exact proof term for the current goal is (andER (j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x)) (∀x1 : set, x1 ∈ X ∖ U → apply_fun (apply_fun F j) x1 = 0) Hjpack).
Set V to be the term product_cylinder J Xi j (open_ray_upper R 0).
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HTyDef: Ty0 = product_topology_full J Xi.
Use reflexivity.
rewrite the current goal using HTyDef (from left to right).
We prove the intermediate claim HprodDef: product_topology_full J Xi = generated_topology_from_subbasis (product_space J Xi) (product_subbasis_full J Xi).
Use reflexivity.
rewrite the current goal using HprodDef (from left to right).
We prove the intermediate claim HJne: J ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty J j HjJ).
We prove the intermediate claim HcompTop: ∀i : set, i ∈ J → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiJ: i ∈ J.
We prove the intermediate claim Hset: space_family_set Xi i = R.
An exact proof term for the current goal is (space_family_set_const_space_family J R R_standard_topology i HiJ).
We prove the intermediate claim Htop: space_family_topology Xi i = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology i HiJ).
rewrite the current goal using Hset (from left to right).
rewrite the current goal using Htop (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HSsub: subbasis_on (product_space J Xi) (product_subbasis_full J Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on J Xi HJne HcompTop).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim HopenRay: open_ray_upper R 0 ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R 0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R 0 H0R).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R 0) HsRay).
We prove the intermediate claim Htopj: space_family_topology Xi j = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology j HjJ).
We prove the intermediate claim HUtop: open_ray_upper R 0 ∈ space_family_topology Xi j.
rewrite the current goal using Htopj (from left to right).
An exact proof term for the current goal is HopenRay.
We prove the intermediate claim HVsub: V ∈ product_subbasis_full J Xi.
Set Fam to be the term (λi0 : set ⇒ {product_cylinder J Xi i0 U0|U0 ∈ space_family_topology Xi i0}).
We prove the intermediate claim HVfam: V ∈ Fam j.
An exact proof term for the current goal is (ReplI (space_family_topology Xi j) (λU0 : set ⇒ product_cylinder J Xi j U0) (open_ray_upper R 0) HUtop).
An exact proof term for the current goal is (famunionI J Fam j V HjJ HVfam).
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis (product_space J Xi) (product_subbasis_full J Xi) V HSsub HVsub).
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim Hfx: apply_fun Fmap x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim Hval: apply_fun (apply_fun Fmap x) j ∈ open_ray_upper R 0.
rewrite the current goal using Hfx (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) j HjJ) (from left to right).
We prove the intermediate claim HxjR: apply_fun (apply_fun F j) x ∈ R.
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)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepCore).
We prove the intermediate claim Htot: 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 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 Htot HjJ).
We prove the intermediate claim HfjFun: function_on (apply_fun F j) X R.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X R)) (λf0 : set ⇒ function_on f0 X R) (apply_fun F j) HfjFS).
An exact proof term for the current goal is (HfjFun x HxX).
We prove the intermediate claim Hord: order_rel R 0 (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (Rlt_implies_order_rel_R 0 (apply_fun (apply_fun F j) x) Hjpos).
An exact proof term for the current goal is (SepI R (λt : set ⇒ order_rel R 0 t) (apply_fun (apply_fun F j) x) HxjR Hord).
We prove the intermediate claim HVdef: V = {f0 ∈ product_space J Xi|j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0}.
Use reflexivity.
rewrite the current goal using HVdef (from left to right).
We prove the intermediate claim Htot: total_function_on F J (function_space X R).
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)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepCore).
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 HfunF: function_on Fmap X (power_real J).
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_function_on_power_real X F J Htot).
We prove the intermediate claim HpR: power_real J = product_space J Xi.
Use reflexivity.
We prove the intermediate claim HfxProd: apply_fun Fmap x ∈ product_space J Xi.
rewrite the current goal using HpR (from right to left).
An exact proof term for the current goal is (HfunF x HxX).
Apply (SepI (product_space J Xi) (λf0 : set ⇒ j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0) (apply_fun Fmap x) HfxProd) 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 HjJ.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim HopenRay: open_ray_upper R 0 ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R 0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R 0 H0R).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R 0) HsRay).
We prove the intermediate claim Htopj: space_family_topology Xi j = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology j HjJ).
rewrite the current goal using Htopj (from left to right).
An exact proof term for the current goal is HopenRay.
We prove the intermediate claim Hcoord: apply_fun (apply_fun Fmap x) j ∈ open_ray_upper R 0.
An exact proof term for the current goal is Hval.
An exact proof term for the current goal is Hcoord.
Let z be given.
Assume HzPre: z ∈ preimage_of X Fmap V.
We will prove z ∈ U.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun Fmap x0 ∈ V) z HzPre).
We prove the intermediate claim HzV: apply_fun Fmap z ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun Fmap x0 ∈ V) z HzPre).
We prove the intermediate claim HVdef: V = {f0 ∈ product_space J Xi|j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0}.
Use reflexivity.
We prove the intermediate claim HzV2: apply_fun Fmap z ∈ {f0 ∈ product_space J Xi|j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0}.
rewrite the current goal using HVdef (from right to left).
An exact proof term for the current goal is HzV.
We prove the intermediate claim Hcore: j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun (apply_fun Fmap z) j ∈ open_ray_upper R 0.
An exact proof term for the current goal is (SepE2 (product_space J Xi) (λf0 : set ⇒ j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0) (apply_fun Fmap z) HzV2).
We prove the intermediate claim Hzcoord: apply_fun (apply_fun Fmap z) j ∈ open_ray_upper R 0.
We prove the intermediate claim H12: j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j.
An exact proof term for the current goal is (andEL (j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j) (apply_fun (apply_fun Fmap z) j ∈ open_ray_upper R 0) Hcore).
An exact proof term for the current goal is (andER (j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j) (apply_fun (apply_fun Fmap z) j ∈ open_ray_upper R 0) Hcore).
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HFmapz: apply_fun Fmap z = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) z).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) z HzX).
We prove the intermediate claim Hzcoord2: apply_fun (apply_fun F j) z ∈ open_ray_upper R 0.
We prove the intermediate claim HcoordEq: apply_fun (apply_fun Fmap z) j = apply_fun (apply_fun F j) z.
rewrite the current goal using HFmapz (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) z) j HjJ) (from left to right).
Use reflexivity.
rewrite the current goal using HcoordEq (from right to left).
An exact proof term for the current goal is Hzcoord.
We prove the intermediate claim HzR: apply_fun (apply_fun F j) z ∈ R.
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)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepCore).
We prove the intermediate claim Htot: 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 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 Htot HjJ).
We prove the intermediate claim HfjFun: function_on (apply_fun F j) X R.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X R)) (λf0 : set ⇒ function_on f0 X R) (apply_fun F j) HfjFS).
An exact proof term for the current goal is (HfjFun z HzX).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hzord: order_rel R 0 (apply_fun (apply_fun F j) z).
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ order_rel R 0 t) (apply_fun (apply_fun F j) z) Hzcoord2).
We prove the intermediate claim Hzpos: Rlt 0 (apply_fun (apply_fun F j) z).
An exact proof term for the current goal is (order_rel_R_implies_Rlt 0 (apply_fun (apply_fun F j) z) Hzord).
Apply (xm (z ∈ U)) to the current goal.
Assume HzU: z ∈ U.
An exact proof term for the current goal is HzU.
Assume HznotU: z ∉ U.
We prove the intermediate claim HzOut: z ∈ X ∖ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is HzX.
An exact proof term for the current goal is HznotU.
We prove the intermediate claim Hz0: apply_fun (apply_fun F j) z = 0.
An exact proof term for the current goal is (Hjzero z HzOut).
We prove the intermediate claim Hbad: False.
We prove the intermediate claim Hzpos0: Rlt 0 0.
rewrite the current goal using Hz0 (from right to left) at position 2.
An exact proof term for the current goal is Hzpos.
An exact proof term for the current goal is ((not_Rlt_refl 0 H0R) Hzpos0).
An exact proof term for the current goal is (FalseE Hbad (z ∈ U)).
We prove the intermediate claim HinjFmap: ∀x y : set, x ∈ X → y ∈ X → apply_fun Fmap x = apply_fun Fmap y → x = y.
Let x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume Heq: apply_fun Fmap x = apply_fun Fmap y.
Apply (xm (x = y)) to the current goal.
Assume Hxy: x = y.
An exact proof term for the current goal is Hxy.
Assume Hne: x ≠ y.
We prove the intermediate claim Hexj: ∃j : set, j ∈ J ∧ apply_fun (apply_fun F j) x ≠ apply_fun (apply_fun F j) y.
An exact proof term for the current goal is (separating_family_of_functions_separates_points X Tx F J x y HTx HT1 Hsep HxX HyX Hne).
Apply Hexj to the current goal.
Let j be given.
Assume Hjpair.
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) x ≠ apply_fun (apply_fun F j) y) Hjpair).
We prove the intermediate claim Hneq: apply_fun (apply_fun F j) x ≠ apply_fun (apply_fun F j) y.
An exact proof term for the current goal is (andER (j ∈ J) (apply_fun (apply_fun F j) x ≠ apply_fun (apply_fun F j) y) Hjpair).
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HFmapx: apply_fun Fmap x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim HFmapy: apply_fun Fmap y = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) y HyX).
We prove the intermediate claim HgraphEq: graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y).
rewrite the current goal using HFmapx (from right to left) at position 1.
rewrite the current goal using HFmapy (from right to left) at position 1.
An exact proof term for the current goal is Heq.
We prove the intermediate claim Heqj: apply_fun (apply_fun F j) x = apply_fun (apply_fun F j) y.
We prove the intermediate claim HapplyEq: apply_fun (graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x)) j = apply_fun (graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y)) j.
rewrite the current goal using HgraphEq (from left to right).
Use reflexivity.
We prove the intermediate claim Hleft: apply_fun (graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x)) j = apply_fun (apply_fun F j) x.
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) j HjJ) (from left to right).
Use reflexivity.
We prove the intermediate claim Hright: apply_fun (graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y)) j = apply_fun (apply_fun F j) y.
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y) j HjJ) (from left to right).
Use reflexivity.
rewrite the current goal using Hleft (from right to left) at position 1.
rewrite the current goal using Hright (from right to left) at position 1.
An exact proof term for the current goal is HapplyEq.
We prove the intermediate claim Hbad: False.
An exact proof term for the current goal is (Hneq Heqj).
An exact proof term for the current goal is (FalseE Hbad (x = y)).
An exact proof term for the current goal is (embedding_of_from_local_refinement X Tx (power_real J) Ty0 Fmap HcontFmap HlocFmap HinjFmap).
Set Y to be the term R_omega_space.
Set Ty to be the term R_omega_product_topology.
We prove the intermediate claim HYeq: power_real J = Y.
An exact proof term for the current goal is power_real_omega_eq_Romega_space.
We prove the intermediate claim HTyeq: product_topology_full J (const_space_family J R R_standard_topology) = Ty.
Use reflexivity.
We prove the intermediate claim HmTy: metric_on Y Romega_D_metric ∧ Romega_D_metric_topology = Ty.
An exact proof term for the current goal is Romega_D_metric_induces_product_topology.
We prove the intermediate claim HFemb: embedding_of X Tx Y Ty Fmap.
rewrite the current goal using HYeq (from right to left).
rewrite the current goal using HTyeq (from right to left).
An exact proof term for the current goal is HFmap.
We prove the intermediate claim HcontFmapY: continuous_map X Tx Y Ty Fmap.
An exact proof term for the current goal is (embedding_of_continuous X Tx Y Ty Fmap HFemb).
We prove the intermediate claim HFmapfun: function_on Fmap X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y Ty Fmap HcontFmapY).
We prove the intermediate claim HmY: metric_on Y Romega_D_metric.
An exact proof term for the current goal is (andEL (metric_on Y Romega_D_metric) (Romega_D_metric_topology = Ty) HmTy).
Set d to be the term graph (setprod X X) (λpq : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
We use d to witness the existential quantifier.
Apply andI to the current goal.
We will prove metric_on X d.
We will prove function_on d (setprod X X) R ∧ (∀x y : set, x ∈ X → y ∈ X → apply_fun d (x,y) = apply_fun d (y,x)) ∧ (∀x : set, x ∈ X → apply_fun d (x,x) = 0) ∧ (∀x y : set, x ∈ X → y ∈ X → ¬ (Rlt (apply_fun d (x,y)) 0) ∧ (apply_fun d (x,y) = 0 → x = y)) ∧ (∀x y z : set, x ∈ X → y ∈ X → z ∈ X → ¬ (Rlt (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))) (apply_fun d (x,z)))).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HdYfun: function_on Romega_D_metric (setprod Y Y) R.
An exact proof term for the current goal is (metric_on_function_on Y Romega_D_metric HmY).
Let pq be given.
Assume Hpq: pq ∈ (setprod X X).
We will prove apply_fun d pq ∈ 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) ∈ Y.
An exact proof term for the current goal is (HFmapfun (pq 0) HxX).
We prove the intermediate claim HfyY: apply_fun Fmap (pq 1) ∈ Y.
An exact proof term for the current goal is (HFmapfun (pq 1) HyX).
We prove the intermediate claim HfxyIn: (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1)) ∈ setprod Y Y.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun Fmap (pq 0)) (apply_fun Fmap (pq 1)) HfxY HfyY).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) pq Hpq) (from left to right).
An exact proof term for the current goal is (HdYfun (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1)) HfxyIn).
Let x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
We prove the intermediate claim HfxY: apply_fun Fmap x ∈ Y.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ Y.
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).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,y) HxyIn) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (y,x) HyxIn) (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 Y Romega_D_metric (apply_fun Fmap x) (apply_fun Fmap y) HmY HfxY HfyY).
Let x be given.
Assume HxX: x ∈ X.
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 HfxY: apply_fun Fmap x ∈ Y.
An exact proof term for the current goal is (HFmapfun x HxX).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,x) HxxIn) (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 Y Romega_D_metric (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 d (x,y)) 0) ∧ (apply_fun d (x,y) = 0 → x = y).
Apply andI to the current goal.
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 HfxY: apply_fun Fmap x ∈ Y.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ Y.
An exact proof term for the current goal is (HFmapfun y HyX).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,y) HxyIn) (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 Y Romega_D_metric (apply_fun Fmap x) (apply_fun Fmap y) HmY HfxY HfyY).
Assume Hd0: apply_fun d (x,y) = 0.
Set Im to be the term image_of Fmap X.
Set Tim to be the term subspace_topology Y Ty Im.
We prove the intermediate claim Hhom: homeomorphism X Tx Im Tim Fmap.
An exact proof term for the current goal is (embedding_of_homeomorphism X Tx Y Ty Fmap HFemb).
We prove the intermediate claim Hinj: ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → apply_fun Fmap x1 = apply_fun Fmap x2 → x1 = x2.
An exact proof term for the current goal is (homeomorphism_injective X Tx Im Tim Fmap Hhom).
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 HfxY: apply_fun Fmap x ∈ Y.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ Y.
An exact proof term for the current goal is (HFmapfun y HyX).
We prove the intermediate claim HfyEq0: apply_fun Romega_D_metric (apply_fun Fmap x,apply_fun Fmap y) = 0.
We prove the intermediate claim HdxyEq: apply_fun d (x,y) = apply_fun Romega_D_metric (apply_fun Fmap x,apply_fun Fmap y).
We prove the intermediate claim Hddef: d = graph (setprod X X) (λpq : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
rewrite the current goal using Hddef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,y) HxyIn) (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.
rewrite the current goal using HdxyEq (from right to left).
An exact proof term for the current goal is Hd0.
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 Y Romega_D_metric (apply_fun Fmap x) (apply_fun Fmap y) HmY HfxY HfyY HfyEq0).
An exact proof term for the current goal is (Hinj 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 d (x,y)) (apply_fun d (y,z))) (apply_fun d (x,z))).
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 HfxY: apply_fun Fmap x ∈ Y.
An exact proof term for the current goal is (HFmapfun x HxX).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ Y.
An exact proof term for the current goal is (HFmapfun y HyX).
We prove the intermediate claim HfzY: apply_fun Fmap z ∈ Y.
An exact proof term for the current goal is (HFmapfun z HzX).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,y) HxyIn) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (y,z) HyzIn) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x,z) HxzIn) (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 Y Romega_D_metric (apply_fun Fmap x) (apply_fun Fmap y) (apply_fun Fmap z) HmY HfxY HfyY HfzY).
We will prove metric_topology X d = Tx.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ metric_topology X d.
We will prove U ∈ Tx.
Set Bx to be the term famunion X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HUgen: U ∈ generated_topology X Bx.
We prove the intermediate claim Hdef: metric_topology X d = generated_topology X Bx.
Use reflexivity.
rewrite the current goal using Hdef (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 Hb: b ∈ Bx.
Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) b Hb (b ∈ Tx)) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume HbIn: b ∈ {open_ball X d x0 r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d x0 r0) b HbIn (b ∈ Tx)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hbeq: b = open_ball X d x0 r0.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hx0Y: apply_fun Fmap x0 ∈ Y.
An exact proof term for the current goal is (HFmapfun x0 Hx0X).
We prove the intermediate claim HballYTy: open_ball Y Romega_D_metric (apply_fun Fmap x0) r0 ∈ Ty.
We prove the intermediate claim HTyEq: Romega_D_metric_topology = Ty.
An exact proof term for the current goal is (andER (metric_on Y Romega_D_metric) (Romega_D_metric_topology = Ty) HmTy).
We will prove open_ball Y Romega_D_metric (apply_fun Fmap x0) r0 ∈ Ty.
rewrite the current goal using HTyEq (from right to left).
We prove the intermediate claim HMTdefY: metric_topology Y Romega_D_metric = Romega_D_metric_topology.
Use reflexivity.
rewrite the current goal using HMTdefY (from right to left).
An exact proof term for the current goal is (open_ball_in_metric_topology Y Romega_D_metric (apply_fun Fmap x0) r0 HmY Hx0Y Hr0pos).
We prove the intermediate claim HballPre: preimage_of X Fmap (open_ball Y Romega_D_metric (apply_fun Fmap x0) r0) = open_ball X d x0 r0.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ preimage_of X Fmap (open_ball Y Romega_D_metric (apply_fun Fmap x0) r0).
We will prove z ∈ open_ball X d x0 r0.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λt : set ⇒ apply_fun Fmap t ∈ open_ball Y Romega_D_metric (apply_fun Fmap x0) r0) z Hz).
We prove the intermediate claim HfzBall: apply_fun Fmap z ∈ open_ball Y Romega_D_metric (apply_fun Fmap x0) r0.
An exact proof term for the current goal is (SepE2 X (λt : set ⇒ apply_fun Fmap t ∈ open_ball Y Romega_D_metric (apply_fun Fmap x0) r0) z Hz).
We prove the intermediate claim HltY: Rlt (apply_fun Romega_D_metric (apply_fun Fmap x0,apply_fun Fmap z)) r0.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ Rlt (apply_fun Romega_D_metric (apply_fun Fmap x0,y0)) r0) (apply_fun Fmap z) HfzBall).
We prove the intermediate claim HdEq: apply_fun d (x0,z) = apply_fun Romega_D_metric (apply_fun Fmap x0,apply_fun Fmap z).
We prove the intermediate claim HxzIn: (x0,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x0 z Hx0X HzX).
We prove the intermediate claim Hddef: d = graph (setprod X X) (λpq : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
rewrite the current goal using Hddef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x0,z) HxzIn) (from left to right).
rewrite the current goal using (tuple_2_0_eq x0 z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x0 z) (from left to right).
Use reflexivity.
We prove the intermediate claim Hlt: Rlt (apply_fun d (x0,z)) r0.
rewrite the current goal using HdEq (from left to right).
An exact proof term for the current goal is HltY.
An exact proof term for the current goal is (open_ballI X d x0 r0 z HzX Hlt).
Let z be given.
Assume Hz: z ∈ open_ball X d x0 r0.
We will prove z ∈ preimage_of X Fmap (open_ball Y Romega_D_metric (apply_fun Fmap x0) r0).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λt : set ⇒ Rlt (apply_fun d (x0,t)) r0) z Hz).
We prove the intermediate claim HltX: Rlt (apply_fun d (x0,z)) r0.
An exact proof term for the current goal is (SepE2 X (λt : set ⇒ Rlt (apply_fun d (x0,t)) r0) z Hz).
We prove the intermediate claim HdEq: apply_fun d (x0,z) = apply_fun Romega_D_metric (apply_fun Fmap x0,apply_fun Fmap z).
We prove the intermediate claim HxzIn: (x0,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x0 z Hx0X HzX).
We prove the intermediate claim Hddef: d = graph (setprod X X) (λpq : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
rewrite the current goal using Hddef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x0,z) HxzIn) (from left to right).
rewrite the current goal using (tuple_2_0_eq x0 z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x0 z) (from left to right).
Use reflexivity.
We prove the intermediate claim HzY: apply_fun Fmap z ∈ Y.
An exact proof term for the current goal is (HFmapfun z HzX).
We prove the intermediate claim HballMem: apply_fun Fmap z ∈ open_ball Y Romega_D_metric (apply_fun Fmap x0) r0.
We prove the intermediate claim HltY0: Rlt (apply_fun Romega_D_metric (apply_fun Fmap x0,apply_fun Fmap z)) r0.
rewrite the current goal using HdEq (from right to left).
An exact proof term for the current goal is HltX.
An exact proof term for the current goal is (open_ballI Y Romega_D_metric (apply_fun Fmap x0) r0 (apply_fun Fmap z) HzY HltY0).
An exact proof term for the current goal is (SepI X (λt : set ⇒ apply_fun Fmap t ∈ open_ball Y Romega_D_metric (apply_fun Fmap x0) r0) z HzX HballMem).
rewrite the current goal using HballPre (from right to left).
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty Fmap HcontFmapY (open_ball Y Romega_D_metric (apply_fun Fmap x0) r0) HballYTy).
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 d.
Set Bx to be the term famunion X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim Hdef: metric_topology X d = generated_topology X Bx.
Use reflexivity.
rewrite the current goal using Hdef (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 HUPower: U ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X U HUsubX).
Set Im to be the term image_of Fmap X.
Set Tim to be the term subspace_topology Y Ty Im.
We prove the intermediate claim Hhom: homeomorphism X Tx Im Tim Fmap.
An exact proof term for the current goal is (embedding_of_homeomorphism X Tx Y Ty Fmap HFemb).
We prove the intermediate claim Hexg: ∃g : set, continuous_map Im Tim X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun Fmap x) = x) ∧ (∀y : set, y ∈ Im → apply_fun Fmap (apply_fun g y) = y).
An exact proof term for the current goal is (homeomorphism_inverse_package X Tx Im Tim Fmap Hhom).
Apply Hexg to the current goal.
Let g be given.
Assume Hgpack.
We prove the intermediate claim Hgpair1: continuous_map Im Tim X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun Fmap x) = x).
An exact proof term for the current goal is (andEL (continuous_map Im Tim X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun Fmap x) = x)) (∀y : set, y ∈ Im → apply_fun Fmap (apply_fun g y) = y) Hgpack).
We prove the intermediate claim Hgcont: continuous_map Im Tim X Tx g.
An exact proof term for the current goal is (andEL (continuous_map Im Tim X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun Fmap x) = x) Hgpair1).
We prove the intermediate claim Hginv: ∀x : set, x ∈ X → apply_fun g (apply_fun Fmap x) = x.
An exact proof term for the current goal is (andER (continuous_map Im Tim X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun Fmap x) = x) Hgpair1).
We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b0 ∈ Bx, x0 ∈ b0 ∧ b0 ⊆ U.
Let x0 be given.
Assume Hx0U: x0 ∈ U.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (HUsubX x0 Hx0U).
We prove the intermediate claim Hfx0Y: apply_fun Fmap x0 ∈ Y.
An exact proof term for the current goal is (HFmapfun x0 Hx0X).
We prove the intermediate claim Hfx0Im: apply_fun Fmap x0 ∈ Im.
An exact proof term for the current goal is (ReplI X (λx1 : set ⇒ apply_fun Fmap x1) x0 Hx0X).
Set V to be the term preimage_of Im g U.
We prove the intermediate claim HVopen: V ∈ Tim.
An exact proof term for the current goal is (continuous_map_preimage Im Tim X Tx g Hgcont U HU).
We prove the intermediate claim Hgx0U: apply_fun g (apply_fun Fmap x0) ∈ U.
rewrite the current goal using (Hginv x0 Hx0X) (from left to right).
An exact proof term for the current goal is Hx0U.
We prove the intermediate claim Hfx0V: apply_fun Fmap x0 ∈ V.
An exact proof term for the current goal is (SepI Im (λy0 : set ⇒ apply_fun g y0 ∈ U) (apply_fun Fmap x0) Hfx0Im Hgx0U).
We prove the intermediate claim HexW: ∃W ∈ Ty, V = W ∩ Im.
An exact proof term for the current goal is (subspace_topologyE Y Ty Im V HVopen).
Apply HexW to the current goal.
Let W be given.
Assume HWpair.
We prove the intermediate claim HWopen: W ∈ Ty.
An exact proof term for the current goal is (andEL (W ∈ Ty) (V = W ∩ Im) HWpair).
We prove the intermediate claim HVequiv: V = W ∩ Im.
An exact proof term for the current goal is (andER (W ∈ Ty) (V = W ∩ Im) HWpair).
We prove the intermediate claim Hfx0W: apply_fun Fmap x0 ∈ W.
We prove the intermediate claim Hfx0WIm: apply_fun Fmap x0 ∈ W ∩ Im.
rewrite the current goal using HVequiv (from right to left).
An exact proof term for the current goal is Hfx0V.
An exact proof term for the current goal is (binintersectE1 W Im (apply_fun Fmap x0) Hfx0WIm).
We prove the intermediate claim HTyEq: Romega_D_metric_topology = Ty.
An exact proof term for the current goal is (andER (metric_on Y Romega_D_metric) (Romega_D_metric_topology = Ty) HmTy).
We prove the intermediate claim HWrtop: W ∈ Romega_D_metric_topology.
rewrite the current goal using HTyEq (from left to right).
An exact proof term for the current goal is HWopen.
We prove the intermediate claim HMTdefY: metric_topology Y Romega_D_metric = Romega_D_metric_topology.
Use reflexivity.
We prove the intermediate claim HWmt: W ∈ metric_topology Y Romega_D_metric.
rewrite the current goal using HMTdefY (from left to right).
An exact proof term for the current goal is HWrtop.
Set By to be the term famunion Y (λy0 : set ⇒ {open_ball Y Romega_D_metric y0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HWgen: W ∈ generated_topology Y By.
We prove the intermediate claim HMTgen: metric_topology Y Romega_D_metric = generated_topology Y By.
Use reflexivity.
rewrite the current goal using HMTgen (from right to left).
An exact proof term for the current goal is HWmt.
We prove the intermediate claim HWprop: ∀y0 ∈ W, ∃bY ∈ By, y0 ∈ bY ∧ bY ⊆ W.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ ∀y0 ∈ U0, ∃bY ∈ By, y0 ∈ bY ∧ bY ⊆ U0) W HWgen).
Apply (HWprop (apply_fun Fmap x0) Hfx0W) to the current goal.
Let bY be given.
Assume HbYpack.
We prove the intermediate claim HbYIn: bY ∈ By.
An exact proof term for the current goal is (andEL (bY ∈ By) (apply_fun Fmap x0 ∈ bY ∧ bY ⊆ W) HbYpack).
We prove the intermediate claim HbYpair: apply_fun Fmap x0 ∈ bY ∧ bY ⊆ W.
An exact proof term for the current goal is (andER (bY ∈ By) (apply_fun Fmap x0 ∈ bY ∧ bY ⊆ W) HbYpack).
We prove the intermediate claim Hfx0bY: apply_fun Fmap x0 ∈ bY.
An exact proof term for the current goal is (andEL (apply_fun Fmap x0 ∈ bY) (bY ⊆ W) HbYpair).
We prove the intermediate claim HbYsubW: bY ⊆ W.
An exact proof term for the current goal is (andER (apply_fun Fmap x0 ∈ bY) (bY ⊆ W) HbYpair).
Apply (famunionE_impred Y (λc0 : set ⇒ {open_ball Y Romega_D_metric c0 r|r ∈ R, Rlt 0 r}) bY HbYIn (∃b0 ∈ Bx, x0 ∈ b0 ∧ b0 ⊆ U)) to the current goal.
Let c0 be given.
Assume Hc0Y: c0 ∈ Y.
Assume HbYIn2: bY ∈ {open_ball Y Romega_D_metric c0 r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball Y Romega_D_metric c0 r0) bY HbYIn2 (∃b0 ∈ Bx, x0 ∈ b0 ∧ b0 ⊆ U)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume HbYeq: bY = open_ball Y Romega_D_metric c0 r0.
We prove the intermediate claim Hfx0inBall: apply_fun Fmap x0 ∈ open_ball Y Romega_D_metric c0 r0.
rewrite the current goal using HbYeq (from right to left).
An exact proof term for the current goal is Hfx0bY.
We prove the intermediate claim HballSubW: open_ball Y Romega_D_metric c0 r0 ⊆ W.
rewrite the current goal using HbYeq (from right to left).
An exact proof term for the current goal is HbYsubW.
We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball Y Romega_D_metric (apply_fun Fmap x0) s ⊆ open_ball Y Romega_D_metric c0 r0.
An exact proof term for the current goal is (open_ball_refine_center Y Romega_D_metric c0 (apply_fun Fmap x0) r0 HmY Hc0Y Hfx0Y Hr0R Hr0pos Hfx0inBall).
Apply Hexs to the current goal.
Let s be given.
Assume Hspack.
We prove the intermediate claim Hs1: s ∈ R ∧ Rlt 0 s.
An exact proof term for the current goal is (andEL (s ∈ R ∧ Rlt 0 s) (open_ball Y Romega_D_metric (apply_fun Fmap x0) s ⊆ open_ball Y Romega_D_metric c0 r0) Hspack).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (andEL (s ∈ R) (Rlt 0 s) Hs1).
We prove the intermediate claim Hspos: Rlt 0 s.
An exact proof term for the current goal is (andER (s ∈ R) (Rlt 0 s) Hs1).
We prove the intermediate claim HsSubBall: open_ball Y Romega_D_metric (apply_fun Fmap x0) s ⊆ open_ball Y Romega_D_metric c0 r0.
An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball Y Romega_D_metric (apply_fun Fmap x0) s ⊆ open_ball Y Romega_D_metric c0 r0) Hspack).
We prove the intermediate claim HballSubW2: open_ball Y Romega_D_metric (apply_fun Fmap x0) s ⊆ W.
An exact proof term for the current goal is (Subq_tra (open_ball Y Romega_D_metric (apply_fun Fmap x0) s) (open_ball Y Romega_D_metric c0 r0) W HsSubBall HballSubW).
We use (open_ball X d x0 s) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HbIn: open_ball X d x0 s ∈ {open_ball X d x0 r|r ∈ R, Rlt 0 r}.
An exact proof term for the current goal is (ReplSepI R (λr1 : set ⇒ Rlt 0 r1) (λr1 : set ⇒ open_ball X d x0 r1) s HsR Hspos).
An exact proof term for the current goal is (famunionI X (λx1 : set ⇒ {open_ball X d x1 r|r ∈ R, Rlt 0 r}) x0 (open_ball X d x0 s) Hx0X HbIn).
Apply andI to the current goal.
We prove the intermediate claim HdEq0: apply_fun d (x0,x0) = apply_fun Romega_D_metric (apply_fun Fmap x0,apply_fun Fmap x0).
We prove the intermediate claim HxxIn: (x0,x0) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x0 x0 Hx0X Hx0X).
We prove the intermediate claim Hddef: d = graph (setprod X X) (λpq : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
rewrite the current goal using Hddef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x0,x0) HxxIn) (from left to right).
rewrite the current goal using (tuple_2_0_eq x0 x0) (from left to right).
rewrite the current goal using (tuple_2_1_eq x0 x0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdiag0: apply_fun Romega_D_metric (apply_fun Fmap x0,apply_fun Fmap x0) = 0.
An exact proof term for the current goal is (metric_on_diag_zero Y Romega_D_metric (apply_fun Fmap x0) HmY Hfx0Y).
We prove the intermediate claim Hlt0: Rlt (apply_fun d (x0,x0)) s.
rewrite the current goal using HdEq0 (from left to right).
rewrite the current goal using Hdiag0 (from left to right).
An exact proof term for the current goal is Hspos.
An exact proof term for the current goal is (open_ballI X d x0 s x0 Hx0X Hlt0).
Let y be given.
Assume Hy: y ∈ open_ball X d x0 s.
We will prove y ∈ U.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x0 s y Hy).
We prove the intermediate claim HltX: Rlt (apply_fun d (x0,y)) s.
An exact proof term for the current goal is (open_ballE2 X d x0 s y Hy).
We prove the intermediate claim HfyY: apply_fun Fmap y ∈ Y.
An exact proof term for the current goal is (HFmapfun y HyX).
We prove the intermediate claim HdEq: apply_fun d (x0,y) = apply_fun Romega_D_metric (apply_fun Fmap x0,apply_fun Fmap y).
We prove the intermediate claim HxyIn: (x0,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x0 y Hx0X HyX).
We prove the intermediate claim Hddef: d = graph (setprod X X) (λpq : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq 0),apply_fun Fmap (pq 1))).
Use reflexivity.
rewrite the current goal using Hddef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun Romega_D_metric (apply_fun Fmap (pq0 0),apply_fun Fmap (pq0 1))) (x0,y) HxyIn) (from left to right).
rewrite the current goal using (tuple_2_0_eq x0 y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x0 y) (from left to right).
Use reflexivity.
We prove the intermediate claim HballYmem: apply_fun Fmap y ∈ open_ball Y Romega_D_metric (apply_fun Fmap x0) s.
We prove the intermediate claim HltY: Rlt (apply_fun Romega_D_metric (apply_fun Fmap x0,apply_fun Fmap y)) s.
rewrite the current goal using HdEq (from right to left).
An exact proof term for the current goal is HltX.
An exact proof term for the current goal is (open_ballI Y Romega_D_metric (apply_fun Fmap x0) s (apply_fun Fmap y) HfyY HltY).
We prove the intermediate claim HfyW: apply_fun Fmap y ∈ W.
An exact proof term for the current goal is (HballSubW2 (apply_fun Fmap y) HballYmem).
We prove the intermediate claim HfyIm: apply_fun Fmap y ∈ Im.
An exact proof term for the current goal is (ReplI X (λx1 : set ⇒ apply_fun Fmap x1) y HyX).
We prove the intermediate claim HfyV: apply_fun Fmap y ∈ V.
rewrite the current goal using HVequiv (from left to right).
An exact proof term for the current goal is (binintersectI W Im (apply_fun Fmap y) HfyW HfyIm).
We prove the intermediate claim HgyU: apply_fun g (apply_fun Fmap y) ∈ U.
An exact proof term for the current goal is (SepE2 Im (λy0 : set ⇒ apply_fun g y0 ∈ U) (apply_fun Fmap y) HfyV).
rewrite the current goal using (Hginv y HyX) (from right to left).
An exact proof term for the current goal is HgyU.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ Bx, x0 ∈ b0 ∧ b0 ⊆ U0) U HUPower HUprop).
∎