Let X, Tx and m be given.
Assume Hloc: locally_m_euclidean X Tx m.
We prove the intermediate claim HmTx: m ∈ ω ∧ topology_on X Tx.
An exact proof term for the current goal is (andEL (m ∈ ω ∧ topology_on X Tx) (∀x : set, x ∈ X → ∃U : set, ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) Hloc).
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (andEL (m ∈ ω) (topology_on X Tx) HmTx).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andER (m ∈ ω) (topology_on X Tx) HmTx).
We prove the intermediate claim Hchart: ∀x : set, x ∈ X → ∃U : set, ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
An exact proof term for the current goal is (andER (m ∈ ω ∧ topology_on X Tx) (∀x : set, x ∈ X → ∃U : set, ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) Hloc).
We will prove locally_compact X Tx ∧ locally_metrizable_space X Tx.
Apply andI to the current goal.
We will prove locally_compact X Tx.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U)).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
Apply (Hchart x HxX) to the current goal.
Let U be given.
Assume HexV: ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
Apply HexV to the current goal.
Let V be given.
Assume Hexf: ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
Apply Hexf to the current goal.
Let f be given.
Assume Hpack: open_in X Tx U ∧ x ∈ U ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
We prove the intermediate claim Hleft: (((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V).
An exact proof term for the current goal is (andEL ((((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V)) (homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) Hpack).
We prove the intermediate claim H12: open_in X Tx U ∧ x ∈ U.
An exact proof term for the current goal is (andEL (open_in X Tx U ∧ x ∈ U) (V ⊆ (euclidean_space m)) (andEL ((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V) Hleft)).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U (andEL (open_in X Tx U) (x ∈ U) H12)).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (open_in X Tx U) (x ∈ U) H12).
We prove the intermediate claim HVsub: V ⊆ (euclidean_space m).
An exact proof term for the current goal is (andER (open_in X Tx U ∧ x ∈ U) (V ⊆ (euclidean_space m)) (andEL ((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V) Hleft)).
We prove the intermediate claim HVopen: open_in (euclidean_space m) (euclidean_topology m) V.
An exact proof term for the current goal is (andER ((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V) Hleft).
We prove the intermediate claim Hhomeo: homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
An exact proof term for the current goal is (andER ((((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V)) (homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) Hpack).
An exact proof term for the current goal is (chart_neighborhood_has_compact_closure X Tx m U V f x HmO HTx (andEL (open_in X Tx U) (x ∈ U) H12) HxU HVsub HVopen Hhomeo).
We will prove locally_metrizable_space X Tx.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃d : set, metric_on N d ∧ subspace_topology X Tx N = metric_topology N d.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
Apply (Hchart x HxX) to the current goal.
Let U be given.
Assume HexV: ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
Apply HexV to the current goal.
Let V be given.
Assume Hexf: ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
Apply Hexf to the current goal.
Let f be given.
Assume Hpack: open_in X Tx U ∧ x ∈ U ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
We prove the intermediate claim H1234: (((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V).
An exact proof term for the current goal is (andEL ((((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V)) (homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) Hpack).
We prove the intermediate claim HhomUV: homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
An exact proof term for the current goal is (andER ((((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V)) (homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) Hpack).
We prove the intermediate claim H123: (open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m).
An exact proof term for the current goal is (andEL ((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V) H1234).
We prove the intermediate claim HVopen: open_in (euclidean_space m) (euclidean_topology m) V.
An exact proof term for the current goal is (andER ((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V) H1234).
We prove the intermediate claim H12: open_in X Tx U ∧ x ∈ U.
An exact proof term for the current goal is (andEL (open_in X Tx U ∧ x ∈ U) (V ⊆ (euclidean_space m)) H123).
We prove the intermediate claim HVsub: V ⊆ (euclidean_space m).
An exact proof term for the current goal is (andER (open_in X Tx U ∧ x ∈ U) (V ⊆ (euclidean_space m)) H123).
We prove the intermediate claim HUopen: open_in X Tx U.
An exact proof term for the current goal is (andEL (open_in X Tx U) (x ∈ U) H12).
We prove the intermediate claim HxinU: x ∈ U.
An exact proof term for the current goal is (andER (open_in X Tx U) (x ∈ U) H12).
We use U 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 (open_in_elem X Tx U HUopen).
An exact proof term for the current goal is HxinU.
We prove the intermediate claim HmetEm: metrizable (euclidean_space m) (euclidean_topology m).
An exact proof term for the current goal is (euclidean_space_metrizable m HmO).
We prove the intermediate claim HVmet: metrizable V (subspace_topology (euclidean_space m) (euclidean_topology m) V).
We prove the intermediate claim HexdE: ∃dE : set, metric_on (euclidean_space m) dE ∧ metric_topology (euclidean_space m) dE = (euclidean_topology m).
An exact proof term for the current goal is HmetEm.
Set dE to be the term Eps_i (λd0 : set ⇒ metric_on (euclidean_space m) d0 ∧ metric_topology (euclidean_space m) d0 = (euclidean_topology m)).
We prove the intermediate claim HdEpair: metric_on (euclidean_space m) dE ∧ metric_topology (euclidean_space m) dE = (euclidean_topology m).
An exact proof term for the current goal is (Eps_i_ex (λd0 : set ⇒ metric_on (euclidean_space m) d0 ∧ metric_topology (euclidean_space m) d0 = (euclidean_topology m)) HexdE).
We prove the intermediate claim HdE: metric_on (euclidean_space m) dE.
An exact proof term for the current goal is (andEL (metric_on (euclidean_space m) dE) (metric_topology (euclidean_space m) dE = (euclidean_topology m)) HdEpair).
Set dV to be the term graph (setprod V V) (λpq : set ⇒ apply_fun dE pq).
We will prove ∃dV0 : set, metric_on V dV0 ∧ metric_topology V dV0 = subspace_topology (euclidean_space m) (euclidean_topology m) V.
We use dV to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hmdef: metric_on V dV = (function_on dV (setprod V V) R ∧ (∀x y : set, x ∈ V → y ∈ V → apply_fun dV (x,y) = apply_fun dV (y,x)) ∧ (∀x : set, x ∈ V → apply_fun dV (x,x) = 0) ∧ (∀x y : set, x ∈ V → y ∈ V → ¬ (Rlt (apply_fun dV (x,y)) 0) ∧ (apply_fun dV (x,y) = 0 → x = y)) ∧ (∀x y z : set, x ∈ V → y ∈ V → z ∈ V → ¬ (Rlt (add_SNo (apply_fun dV (x,y)) (apply_fun dV (y,z))) (apply_fun dV (x,z))))).
Use reflexivity.
rewrite the current goal using Hmdef (from left to right).
Apply and5I to the current goal.
We prove the intermediate claim HtotdV: total_function_on dV (setprod V V) R.
We prove the intermediate claim HdVdef: dV = graph (setprod V V) (λpq : set ⇒ apply_fun dE pq).
Use reflexivity.
rewrite the current goal using HdVdef (from left to right).
Apply (total_function_on_graph (setprod V V) R (λpq : set ⇒ apply_fun dE pq)) to the current goal.
Let pq be given.
Assume Hpq: pq ∈ setprod V V.
We will prove apply_fun dE pq ∈ R.
We prove the intermediate claim HpqE: pq ∈ setprod (euclidean_space m) (euclidean_space m).
An exact proof term for the current goal is ((setprod_Subq V V (euclidean_space m) (euclidean_space m) HVsub HVsub) pq Hpq).
An exact proof term for the current goal is ((metric_on_function_on (euclidean_space m) dE HdE) pq HpqE).
An exact proof term for the current goal is (total_function_on_function_on dV (setprod V V) R HtotdV).
Let x0 and y0 be given.
Assume Hx0V: x0 ∈ V.
Assume Hy0V: y0 ∈ V.
We will prove apply_fun dV (x0,y0) = apply_fun dV (y0,x0).
We prove the intermediate claim Hx0E: x0 ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub x0 Hx0V).
We prove the intermediate claim Hy0E: y0 ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub y0 Hy0V).
We prove the intermediate claim HxyIn: (x0,y0) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V x0 y0 Hx0V Hy0V).
We prove the intermediate claim HyxIn: (y0,x0) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V y0 x0 Hy0V Hx0V).
We prove the intermediate claim HdVdef: dV = graph (setprod V V) (λpq : set ⇒ apply_fun dE pq).
Use reflexivity.
We prove the intermediate claim HxyEq: apply_fun dV (x0,y0) = apply_fun dE (x0,y0).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (x0,y0) HxyIn).
We prove the intermediate claim HyxEq: apply_fun dV (y0,x0) = apply_fun dE (y0,x0).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (y0,x0) HyxIn).
rewrite the current goal using HxyEq (from left to right).
rewrite the current goal using HyxEq (from left to right).
An exact proof term for the current goal is (metric_on_symmetric (euclidean_space m) dE x0 y0 HdE Hx0E Hy0E).
Let x0 be given.
Assume Hx0V: x0 ∈ V.
We will prove apply_fun dV (x0,x0) = 0.
We prove the intermediate claim Hx0E: x0 ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub x0 Hx0V).
We prove the intermediate claim HxxIn: (x0,x0) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V x0 x0 Hx0V Hx0V).
We prove the intermediate claim HdVdef: dV = graph (setprod V V) (λpq : set ⇒ apply_fun dE pq).
Use reflexivity.
We prove the intermediate claim HxxEq: apply_fun dV (x0,x0) = apply_fun dE (x0,x0).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (x0,x0) HxxIn).
rewrite the current goal using HxxEq (from left to right).
An exact proof term for the current goal is (metric_on_diag_zero (euclidean_space m) dE x0 HdE Hx0E).
Let x0 and y0 be given.
Assume Hx0V: x0 ∈ V.
Assume Hy0V: y0 ∈ V.
We will prove ¬ (Rlt (apply_fun dV (x0,y0)) 0) ∧ (apply_fun dV (x0,y0) = 0 → x0 = y0).
We prove the intermediate claim Hx0E: x0 ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub x0 Hx0V).
We prove the intermediate claim Hy0E: y0 ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub y0 Hy0V).
We prove the intermediate claim HxyIn: (x0,y0) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V x0 y0 Hx0V Hy0V).
We prove the intermediate claim HdVdef: dV = graph (setprod V V) (λpq : set ⇒ apply_fun dE pq).
Use reflexivity.
We prove the intermediate claim HxyEq: apply_fun dV (x0,y0) = apply_fun dE (x0,y0).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (x0,y0) HxyIn).
Apply andI to the current goal.
rewrite the current goal using HxyEq (from left to right).
An exact proof term for the current goal is (metric_on_nonneg (euclidean_space m) dE x0 y0 HdE Hx0E Hy0E).
Assume H0: apply_fun dV (x0,y0) = 0.
We prove the intermediate claim H0E: apply_fun dE (x0,y0) = 0.
rewrite the current goal using HxyEq (from right to left).
An exact proof term for the current goal is H0.
An exact proof term for the current goal is (metric_on_zero_eq (euclidean_space m) dE x0 y0 HdE Hx0E Hy0E H0E).
Let x0, y0 and z0 be given.
Assume Hx0V: x0 ∈ V.
Assume Hy0V: y0 ∈ V.
Assume Hz0V: z0 ∈ V.
We will prove ¬ (Rlt (add_SNo (apply_fun dV (x0,y0)) (apply_fun dV (y0,z0))) (apply_fun dV (x0,z0))).
We prove the intermediate claim Hx0E: x0 ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub x0 Hx0V).
We prove the intermediate claim Hy0E: y0 ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub y0 Hy0V).
We prove the intermediate claim Hz0E: z0 ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub z0 Hz0V).
We prove the intermediate claim HxyIn: (x0,y0) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V x0 y0 Hx0V Hy0V).
We prove the intermediate claim HyzIn: (y0,z0) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V y0 z0 Hy0V Hz0V).
We prove the intermediate claim HxzIn: (x0,z0) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V x0 z0 Hx0V Hz0V).
We prove the intermediate claim HdVdef: dV = graph (setprod V V) (λpq : set ⇒ apply_fun dE pq).
Use reflexivity.
We prove the intermediate claim HxyEq: apply_fun dV (x0,y0) = apply_fun dE (x0,y0).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (x0,y0) HxyIn).
We prove the intermediate claim HyzEq: apply_fun dV (y0,z0) = apply_fun dE (y0,z0).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (y0,z0) HyzIn).
We prove the intermediate claim HxzEq: apply_fun dV (x0,z0) = apply_fun dE (x0,z0).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (x0,z0) HxzIn).
rewrite the current goal using HxyEq (from left to right).
rewrite the current goal using HyzEq (from left to right).
rewrite the current goal using HxzEq (from left to right).
An exact proof term for the current goal is (metric_on_triangle (euclidean_space m) dE x0 y0 z0 HdE Hx0E Hy0E Hz0E).
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ metric_topology V dV.
We will prove U ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V.
Set B0 to be the term famunion V (λc0 : set ⇒ {open_ball V dV c0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HdefMT: metric_topology V dV = generated_topology V B0.
Use reflexivity.
We prove the intermediate claim HeqTe: metric_topology (euclidean_space m) dE = euclidean_topology m.
An exact proof term for the current goal is (andER (metric_on (euclidean_space m) dE) (metric_topology (euclidean_space m) dE = euclidean_topology m) HdEpair).
We prove the intermediate claim HtopE: topology_on (euclidean_space m) (euclidean_topology m).
We prove the intermediate claim HtopMT: topology_on (euclidean_space m) (metric_topology (euclidean_space m) dE).
An exact proof term for the current goal is (metric_topology_is_topology (euclidean_space m) dE HdE).
rewrite the current goal using HeqTe (from right to left).
An exact proof term for the current goal is HtopMT.
We prove the intermediate claim HtopSub: topology_on V (subspace_topology (euclidean_space m) (euclidean_topology m) V).
An exact proof term for the current goal is (subspace_topology_is_topology (euclidean_space m) (euclidean_topology m) V HtopE HVsub).
We prove the intermediate claim HallB0: ∀b ∈ B0, b ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V.
Let b be given.
Assume HbB0: b ∈ B0.
We will prove b ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V.
Apply (famunionE_impred V (λc0 : set ⇒ {open_ball V dV c0 r|r ∈ R, Rlt 0 r}) b HbB0 (b ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V)) to the current goal.
Let c0 be given.
Assume Hc0V: c0 ∈ V.
Assume HbIn: b ∈ {open_ball V dV c0 r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball V dV c0 r0) b HbIn (b ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hbeq: b = open_ball V dV c0 r0.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hc0E: c0 ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub c0 Hc0V).
We prove the intermediate claim HballE: open_ball (euclidean_space m) dE c0 r0 ∈ euclidean_topology m.
We prove the intermediate claim HballMT: open_ball (euclidean_space m) dE c0 r0 ∈ metric_topology (euclidean_space m) dE.
An exact proof term for the current goal is (open_ball_in_metric_topology (euclidean_space m) dE c0 r0 HdE Hc0E Hr0pos).
An exact proof term for the current goal is (mem_eqR (open_ball (euclidean_space m) dE c0 r0) (metric_topology (euclidean_space m) dE) (euclidean_topology m) HeqTe HballMT).
We prove the intermediate claim HballEq: open_ball V dV c0 r0 = open_ball (euclidean_space m) dE c0 r0 ∩ V.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ open_ball V dV c0 r0.
We will prove y ∈ open_ball (euclidean_space m) dE c0 r0 ∩ V.
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (open_ballE1 V dV c0 r0 y Hy).
Apply binintersectI to the current goal.
We prove the intermediate claim HyE: y ∈ (euclidean_space m).
An exact proof term for the current goal is (HVsub y HyV).
We prove the intermediate claim HltV: Rlt (apply_fun dV (c0,y)) r0.
An exact proof term for the current goal is (open_ballE2 V dV c0 r0 y Hy).
We prove the intermediate claim HpairIn: (c0,y) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V c0 y Hc0V HyV).
We prove the intermediate claim HdVdef: dV = graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0).
Use reflexivity.
We prove the intermediate claim Heq: apply_fun dV (c0,y) = apply_fun dE (c0,y).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (c0,y) HpairIn).
We prove the intermediate claim HltE: Rlt (apply_fun dE (c0,y)) r0.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HltV.
An exact proof term for the current goal is (open_ballI (euclidean_space m) dE c0 r0 y HyE HltE).
An exact proof term for the current goal is HyV.
Let y be given.
Assume Hy: y ∈ open_ball (euclidean_space m) dE c0 r0 ∩ V.
We will prove y ∈ open_ball V dV c0 r0.
We prove the intermediate claim HyBallE: y ∈ open_ball (euclidean_space m) dE c0 r0.
An exact proof term for the current goal is (binintersectE1 (open_ball (euclidean_space m) dE c0 r0) V y Hy).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (binintersectE2 (open_ball (euclidean_space m) dE c0 r0) V y Hy).
We prove the intermediate claim HltE: Rlt (apply_fun dE (c0,y)) r0.
An exact proof term for the current goal is (open_ballE2 (euclidean_space m) dE c0 r0 y HyBallE).
We prove the intermediate claim HpairIn: (c0,y) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V c0 y Hc0V HyV).
We prove the intermediate claim HdVdef: dV = graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0).
Use reflexivity.
We prove the intermediate claim Heq: apply_fun dV (c0,y) = apply_fun dE (c0,y).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (c0,y) HpairIn).
We prove the intermediate claim HltV: Rlt (apply_fun dV (c0,y)) r0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HltE.
An exact proof term for the current goal is (open_ballI V dV c0 r0 y HyV HltV).
rewrite the current goal using HballEq (from left to right).
An exact proof term for the current goal is (subspace_topologyI (euclidean_space m) (euclidean_topology m) V (open_ball (euclidean_space m) dE c0 r0) HballE).
We prove the intermediate claim Hsub: metric_topology V dV ⊆ subspace_topology (euclidean_space m) (euclidean_topology m) V.
rewrite the current goal using HdefMT (from left to right).
An exact proof term for the current goal is (generated_topology_finer_weak V B0 (subspace_topology (euclidean_space m) (euclidean_topology m) V) HtopSub HallB0).
An exact proof term for the current goal is (Hsub U HU).
Let U be given.
Assume HU: U ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V.
We will prove U ∈ metric_topology V dV.
Set B0 to be the term famunion V (λc0 : set ⇒ {open_ball V dV c0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HdefMT: metric_topology V dV = generated_topology V B0.
Use reflexivity.
rewrite the current goal using HdefMT (from left to right).
We will prove U ∈ generated_topology V B0.
We prove the intermediate claim HUpow: U ∈ 𝒫 V.
An exact proof term for the current goal is (SepE1 (𝒫 V) (λU0 : set ⇒ ∃W ∈ (euclidean_topology m), U0 = W ∩ V) U HU).
We prove the intermediate claim HUsubV: U ⊆ V.
An exact proof term for the current goal is (PowerE V U HUpow).
We prove the intermediate claim HUW: ∃W ∈ (euclidean_topology m), U = W ∩ V.
An exact proof term for the current goal is (subspace_topologyE (euclidean_space m) (euclidean_topology m) V U HU).
Apply HUW to the current goal.
Let W be given.
Assume HWpack.
We prove the intermediate claim HWopen: W ∈ euclidean_topology m.
An exact proof term for the current goal is (andEL (W ∈ euclidean_topology m) (U = W ∩ V) HWpack).
We prove the intermediate claim HUeq: U = W ∩ V.
An exact proof term for the current goal is (andER (W ∈ euclidean_topology m) (U = W ∩ V) HWpack).
We prove the intermediate claim HtopMT: topology_on (euclidean_space m) (metric_topology (euclidean_space m) dE).
An exact proof term for the current goal is (metric_topology_is_topology (euclidean_space m) dE HdE).
We prove the intermediate claim HeqTe: metric_topology (euclidean_space m) dE = euclidean_topology m.
An exact proof term for the current goal is (andER (metric_on (euclidean_space m) dE) (metric_topology (euclidean_space m) dE = euclidean_topology m) HdEpair).
We prove the intermediate claim HWMT: W ∈ metric_topology (euclidean_space m) dE.
An exact proof term for the current goal is (mem_eqL W (metric_topology (euclidean_space m) dE) (euclidean_topology m) HeqTe HWopen).
We prove the intermediate claim HWopenMT: open_in (euclidean_space m) (metric_topology (euclidean_space m) dE) W.
We will prove open_in (euclidean_space m) (metric_topology (euclidean_space m) dE) W.
We will prove topology_on (euclidean_space m) (metric_topology (euclidean_space m) dE) ∧ W ∈ metric_topology (euclidean_space m) dE.
Apply andI to the current goal.
An exact proof term for the current goal is HtopMT.
An exact proof term for the current goal is HWMT.
We prove the intermediate claim HUprop: ∀y ∈ U, ∃b ∈ B0, y ∈ b ∧ b ⊆ U.
Let y be given.
Assume HyU: y ∈ U.
We will prove ∃b ∈ B0, y ∈ b ∧ b ⊆ U.
We prove the intermediate claim HyUV: y ∈ W ∩ V.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HyU.
We prove the intermediate claim HyW: y ∈ W.
An exact proof term for the current goal is (binintersectE1 W V y HyUV).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (binintersectE2 W V y HyUV).
We prove the intermediate claim HyE: y ∈ euclidean_space m.
An exact proof term for the current goal is (HVsub y HyV).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ open_ball (euclidean_space m) dE y (eps_ N) ⊆ W.
An exact proof term for the current goal is (open_in_metric_topology_has_eps_ball_sub (euclidean_space m) dE W y HdE HWopenMT HyW).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (open_ball (euclidean_space m) dE y (eps_ N) ⊆ W) HNpack).
We prove the intermediate claim HballSubW: open_ball (euclidean_space m) dE y (eps_ N) ⊆ W.
An exact proof term for the current goal is (andER (N ∈ ω) (open_ball (euclidean_space m) dE y (eps_ N) ⊆ W) HNpack).
We prove the intermediate claim HepsR: eps_ N ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R (eps_ N) (Subq_SNoS_omega_rational (eps_ N) (SNo_eps_SNoS_omega N HNomega))).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ N).
An exact proof term for the current goal is (RltI 0 (eps_ N) real_0 HepsR (SNo_eps_pos N HNomega)).
Set b to be the term open_ball V dV y (eps_ N).
We prove the intermediate claim HbInC: b ∈ {open_ball V dV y r0|r0 ∈ R, Rlt 0 r0}.
An exact proof term for the current goal is (ReplSepI R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball V dV y r0) (eps_ N) HepsR Hepspos).
We prove the intermediate claim HbB0: b ∈ B0.
An exact proof term for the current goal is (famunionI V (λc0 : set ⇒ {open_ball V dV c0 r0|r0 ∈ R, Rlt 0 r0}) y b HyV HbInC).
We prove the intermediate claim Hby: y ∈ b.
We will prove y ∈ open_ball V dV y (eps_ N).
We prove the intermediate claim HpairIn: (y,y) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V y y HyV HyV).
We prove the intermediate claim HdVdef: dV = graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0).
Use reflexivity.
We prove the intermediate claim HdiagEq: apply_fun dV (y,y) = apply_fun dE (y,y).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (y,y) HpairIn).
We prove the intermediate claim HdEdiag0: apply_fun dE (y,y) = 0.
An exact proof term for the current goal is (metric_on_diag_zero (euclidean_space m) dE y HdE HyE).
We prove the intermediate claim HdVdiag0: apply_fun dV (y,y) = 0.
rewrite the current goal using HdiagEq (from left to right).
An exact proof term for the current goal is HdEdiag0.
We prove the intermediate claim Hlt: Rlt (apply_fun dV (y,y)) (eps_ N).
rewrite the current goal using HdVdiag0 (from left to right).
An exact proof term for the current goal is Hepspos.
An exact proof term for the current goal is (open_ballI V dV y (eps_ N) y HyV Hlt).
We prove the intermediate claim HbsubU: b ⊆ U.
Let z be given.
Assume Hz: z ∈ b.
We will prove z ∈ U.
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (open_ballE1 V dV y (eps_ N) z Hz).
We prove the intermediate claim HzE: z ∈ euclidean_space m.
An exact proof term for the current goal is (HVsub z HzV).
We prove the intermediate claim HltV: Rlt (apply_fun dV (y,z)) (eps_ N).
An exact proof term for the current goal is (open_ballE2 V dV y (eps_ N) z Hz).
We prove the intermediate claim HpairIn: (y,z) ∈ setprod V V.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma V V y z HyV HzV).
We prove the intermediate claim HdVdef: dV = graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0).
Use reflexivity.
We prove the intermediate claim HeqYZ: apply_fun dV (y,z) = apply_fun dE (y,z).
rewrite the current goal using HdVdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod V V) (λpq0 : set ⇒ apply_fun dE pq0) (y,z) HpairIn).
We prove the intermediate claim HltE: Rlt (apply_fun dE (y,z)) (eps_ N).
rewrite the current goal using HeqYZ (from right to left).
An exact proof term for the current goal is HltV.
We prove the intermediate claim HzBallE: z ∈ open_ball (euclidean_space m) dE y (eps_ N).
An exact proof term for the current goal is (open_ballI (euclidean_space m) dE y (eps_ N) z HzE HltE).
We prove the intermediate claim HzW: z ∈ W.
An exact proof term for the current goal is (HballSubW z HzBallE).
We prove the intermediate claim HzUV: z ∈ W ∩ V.
An exact proof term for the current goal is (binintersectI W V z HzW HzV).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HzUV.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB0.
Apply andI to the current goal.
An exact proof term for the current goal is Hby.
An exact proof term for the current goal is HbsubU.
An exact proof term for the current goal is (SepI (𝒫 V) (λU0 : set ⇒ ∀y0 : set, y0 ∈ U0 → ∃b ∈ B0, y0 ∈ b ∧ b ⊆ U0) U HUpow HUprop).
We prove the intermediate claim HmetU: metrizable U (subspace_topology X Tx U).
An exact proof term for the current goal is (homeomorphism_preserves_metrizable U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f HhomUV HVmet).
Apply HmetU to the current goal.
Let d be given.
Assume HdPair: metric_on U d ∧ metric_topology U d = subspace_topology X Tx U.
We use d to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (metric_on U d) (metric_topology U d = subspace_topology X Tx U) HdPair).
rewrite the current goal using (andER (metric_on U d) (metric_topology U d = subspace_topology X Tx U) HdPair) (from right to left).
Use reflexivity.
∎