Let X, Tx and W be given.
Assume Hnorm: normal_space X Tx.
Assume Hcov: open_cover X Tx W.
Assume Hlf: locally_finite_family X Tx W.
We will prove ∃P : set, partition_of_unity_family X Tx W P.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We prove the intermediate claim HWTx: ∀w : set, w ∈ W → w ∈ Tx.
An exact proof term for the current goal is (andEL (∀w : set, w ∈ W → w ∈ Tx) (covers X W) Hcov).
We prove the intermediate claim HWcovers: covers X W.
An exact proof term for the current goal is (andER (∀w : set, w ∈ W → w ∈ Tx) (covers X W) Hcov).
We prove the intermediate claim HTsubPow: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HWsubPow: W ⊆ 𝒫 X.
We will prove ∀w : set, w ∈ W → w ∈ 𝒫 X.
Let w be given.
Assume HwW: w ∈ W.
An exact proof term for the current goal is (HTsubPow w (HWTx w HwW)).
We prove the intermediate claim HpointFinite: ∀x : set, x ∈ X → finite {w ∈ W|x ∈ w}.
Let x be given.
Assume HxX: x ∈ X.
Set Wx to be the term {w ∈ W|x ∈ w}.
We will prove finite Wx.
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → x ∈ A → A ∈ S.
An exact proof term for the current goal is (locally_finite_family_point_finite_ex X Tx W Hlf x HxX).
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → x ∈ A → A ∈ S.
We prove the intermediate claim HSleft: finite S ∧ S ⊆ W.
An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ W) (∀A : set, A ∈ W → x ∈ A → A ∈ S) HS).
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ W) HSleft).
We prove the intermediate claim HSprop: ∀A : set, A ∈ W → x ∈ A → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ W) (∀A : set, A ∈ W → x ∈ A → A ∈ S) HS).
We prove the intermediate claim HWxSub: Wx ⊆ S.
Let w be given.
Assume Hw: w ∈ Wx.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (SepE1 W (λA0 : set ⇒ x ∈ A0) w Hw).
We prove the intermediate claim Hxw: x ∈ w.
An exact proof term for the current goal is (SepE2 W (λA0 : set ⇒ x ∈ A0) w Hw).
An exact proof term for the current goal is (HSprop w HwW Hxw).
An exact proof term for the current goal is (Subq_finite S HSfin Wx HWxSub).
We prove the intermediate claim HexV: ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (normal_locally_finite_open_cover_shrinking X Tx W Hnorm Hcov Hlf).
Apply HexV to the current goal.
Let V be given.
Assume HV: open_cover X Tx V ∧ locally_finite_family X Tx V ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
We prove the intermediate claim HVcov: open_cover X Tx V.
We prove the intermediate claim HV1: (open_cover X Tx V ∧ locally_finite_family X Tx V) ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w).
An exact proof term for the current goal is (andEL ((open_cover X Tx V ∧ locally_finite_family X Tx V) ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w)) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV).
We prove the intermediate claim HV12: open_cover X Tx V ∧ locally_finite_family X Tx V.
An exact proof term for the current goal is (andEL (open_cover X Tx V ∧ locally_finite_family X Tx V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) HV1).
An exact proof term for the current goal is (andEL (open_cover X Tx V) (locally_finite_family X Tx V) HV12).
We prove the intermediate claim HVlf: locally_finite_family X Tx V.
We prove the intermediate claim HV1: (open_cover X Tx V ∧ locally_finite_family X Tx V) ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w).
An exact proof term for the current goal is (andEL ((open_cover X Tx V ∧ locally_finite_family X Tx V) ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w)) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV).
We prove the intermediate claim HV12: open_cover X Tx V ∧ locally_finite_family X Tx V.
An exact proof term for the current goal is (andEL (open_cover X Tx V ∧ locally_finite_family X Tx V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) HV1).
An exact proof term for the current goal is (andER (open_cover X Tx V) (locally_finite_family X Tx V) HV12).
We prove the intermediate claim HVclmap: ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (andER ((open_cover X Tx V ∧ locally_finite_family X Tx V) ∧ (∀v0 : set, v0 ∈ V → ∃w : set, w ∈ W ∧ v0 ⊆ w)) (∀v0 : set, v0 ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v0 ⊆ w) HV).
We prove the intermediate claim HexU: ∃U : set, open_cover X Tx U ∧ locally_finite_family X Tx U ∧ (∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ u ⊆ v) ∧ ∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ closure_of X Tx u ⊆ v.
An exact proof term for the current goal is (normal_locally_finite_open_cover_shrinking X Tx V Hnorm HVcov HVlf).
Apply HexU to the current goal.
Let U be given.
Assume HU: open_cover X Tx U ∧ locally_finite_family X Tx U ∧ (∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ u ⊆ v) ∧ ∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ closure_of X Tx u ⊆ v.
We prove the intermediate claim HU1: (open_cover X Tx U ∧ locally_finite_family X Tx U) ∧ (∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ u ⊆ v).
An exact proof term for the current goal is (andEL ((open_cover X Tx U ∧ locally_finite_family X Tx U) ∧ (∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ u ⊆ v)) (∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ closure_of X Tx u ⊆ v) HU).
We prove the intermediate claim HU12: open_cover X Tx U ∧ locally_finite_family X Tx U.
An exact proof term for the current goal is (andEL (open_cover X Tx U ∧ locally_finite_family X Tx U) (∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ u ⊆ v) HU1).
We prove the intermediate claim HUcov: open_cover X Tx U.
An exact proof term for the current goal is (andEL (open_cover X Tx U) (locally_finite_family X Tx U) HU12).
We prove the intermediate claim HUlf: locally_finite_family X Tx U.
An exact proof term for the current goal is (andER (open_cover X Tx U) (locally_finite_family X Tx U) HU12).
We prove the intermediate claim HUmap: ∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ u ⊆ v.
An exact proof term for the current goal is (andER (open_cover X Tx U ∧ locally_finite_family X Tx U) (∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ u ⊆ v) HU1).
We prove the intermediate claim HUclmap: ∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ closure_of X Tx u ⊆ v.
An exact proof term for the current goal is (andER ((open_cover X Tx U ∧ locally_finite_family X Tx U) ∧ (∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ u ⊆ v)) (∀u : set, u ∈ U → ∃v : set, v ∈ V ∧ closure_of X Tx u ⊆ v) HU).
Set pickV to be the term λu : set ⇒ Eps_i (λv : set ⇒ v ∈ V ∧ closure_of X Tx u ⊆ v).
We prove the intermediate claim HpickV: ∀u : set, u ∈ U → pickV u ∈ V ∧ closure_of X Tx u ⊆ pickV u.
Let u be given.
Assume HuU: u ∈ U.
We prove the intermediate claim Hexv: ∃v : set, v ∈ V ∧ closure_of X Tx u ⊆ v.
An exact proof term for the current goal is (HUclmap u HuU).
Apply Hexv to the current goal.
Let v be given.
Assume Hv: v ∈ V ∧ closure_of X Tx u ⊆ v.
We prove the intermediate claim Hax: pickV u ∈ V ∧ closure_of X Tx u ⊆ pickV u.
An exact proof term for the current goal is (Eps_i_ax (λv0 : set ⇒ v0 ∈ V ∧ closure_of X Tx u ⊆ v0) v Hv).
An exact proof term for the current goal is Hax.
Set pickW to be the term λv : set ⇒ Eps_i (λw : set ⇒ w ∈ W ∧ closure_of X Tx v ⊆ w).
We prove the intermediate claim HpickW: ∀v : set, v ∈ V → pickW v ∈ W ∧ closure_of X Tx v ⊆ pickW v.
Let v be given.
Assume HvV: v ∈ V.
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (HVclmap v HvV).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (Eps_i_ax (λw0 : set ⇒ w0 ∈ W ∧ closure_of X Tx v ⊆ w0) w Hw).
Set w_of_u to be the term λu : set ⇒ pickW (pickV u).
We prove the intermediate claim Hw_of_u: ∀u : set, u ∈ U → w_of_u u ∈ W ∧ closure_of X Tx (pickV u) ⊆ w_of_u u.
Let u be given.
Assume HuU: u ∈ U.
We prove the intermediate claim Hvpack: pickV u ∈ V ∧ closure_of X Tx u ⊆ pickV u.
An exact proof term for the current goal is (HpickV u HuU).
We prove the intermediate claim HvV: pickV u ∈ V.
An exact proof term for the current goal is (andEL (pickV u ∈ V) (closure_of X Tx u ⊆ pickV u) Hvpack).
An exact proof term for the current goal is (HpickW (pickV u) HvV).
We prove the intermediate claim HVmemTx: ∀v : set, v ∈ V → v ∈ Tx.
An exact proof term for the current goal is (andEL (∀v : set, v ∈ V → v ∈ Tx) (covers X V) HVcov).
We prove the intermediate claim HUmempow: U ⊆ 𝒫 X.
We will prove ∀u : set, u ∈ U → u ∈ 𝒫 X.
Let u be given.
Assume HuU: u ∈ U.
We prove the intermediate claim HUmemTx: ∀u0 : set, u0 ∈ U → u0 ∈ Tx.
An exact proof term for the current goal is (andEL (∀u0 : set, u0 ∈ U → u0 ∈ Tx) (covers X U) HUcov).
An exact proof term for the current goal is (HTsubPow u (HUmemTx u HuU)).
We prove the intermediate claim HUsubX: ∀u : set, u ∈ U → u ⊆ X.
Let u be given.
Assume HuU: u ∈ U.
An exact proof term for the current goal is (PowerE X u (HUmempow u HuU)).
Set bump to be the term λu : set ⇒ Eps_i (λf : set ⇒ continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ closure_of X Tx u → apply_fun f x = 1) ∧ (∀x : set, x ∈ (X ∖ (pickV u)) → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → apply_fun f x ∈ unit_interval)).
We prove the intermediate claim Hbump: ∀u : set, u ∈ U → continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x : set, x ∈ closure_of X Tx u → apply_fun (bump u) x = 1) ∧ (∀x : set, x ∈ (X ∖ (pickV u)) → apply_fun (bump u) x = 0) ∧ (∀x : set, x ∈ X → apply_fun (bump u) x ∈ unit_interval).
Let u be given.
Assume HuU: u ∈ U.
We prove the intermediate claim Hvpack: pickV u ∈ V ∧ closure_of X Tx u ⊆ pickV u.
An exact proof term for the current goal is (HpickV u HuU).
We prove the intermediate claim HvV: pickV u ∈ V.
An exact proof term for the current goal is (andEL (pickV u ∈ V) (closure_of X Tx u ⊆ pickV u) Hvpack).
We prove the intermediate claim HvTx: pickV u ∈ Tx.
An exact proof term for the current goal is (HVmemTx (pickV u) HvV).
We prove the intermediate claim Hclu_closed: closed_in X Tx (closure_of X Tx u).
An exact proof term for the current goal is (closure_is_closed X Tx u HTx (HUsubX u HuU)).
We prove the intermediate claim Hclu_sub_v: closure_of X Tx u ⊆ pickV u.
An exact proof term for the current goal is (andER (pickV u ∈ V) (closure_of X Tx u ⊆ pickV u) Hvpack).
We prove the intermediate claim Hexf: ∃f : set, continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ closure_of X Tx u → apply_fun f x = 1) ∧ (∀x : set, x ∈ (X ∖ (pickV u)) → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → apply_fun f x ∈ unit_interval).
An exact proof term for the current goal is (Urysohn_bump_closed_in_open X Tx (closure_of X Tx u) (pickV u) Hnorm Hclu_closed HvTx Hclu_sub_v).
Apply Hexf to the current goal.
Let f be given.
Assume Hf: continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ closure_of X Tx u → apply_fun f x = 1) ∧ (∀x : set, x ∈ (X ∖ (pickV u)) → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → apply_fun f x ∈ unit_interval).
An exact proof term for the current goal is (Eps_i_ax (λf0 : set ⇒ continuous_map X Tx R R_standard_topology f0 ∧ (∀x : set, x ∈ closure_of X Tx u → apply_fun f0 x = 1) ∧ (∀x : set, x ∈ (X ∖ (pickV u)) → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ X → apply_fun f0 x ∈ unit_interval)) f Hf).
Set bump0 to be the term λu : set ⇒ graph X (λx : set ⇒ apply_fun (bump u) x).
Set P to be the term {bump0 u|u ∈ U}.
We prove the intermediate claim Hbump0_funspace: ∀u : set, u ∈ U → bump0 u ∈ function_space X R.
Let u be given.
Assume HuU: u ∈ U.
Set g to be the term (λx : set ⇒ apply_fun (bump u) x).
We prove the intermediate claim Hb0eq: bump0 u = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
Apply (graph_in_function_space X R g) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hui: apply_fun (bump u) x ∈ unit_interval.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ (pickV u)) → apply_fun (bump u) x0 = 0)) (∀x0 : set, x0 ∈ X → apply_fun (bump u) x0 ∈ unit_interval) (Hbump u HuU) x HxX).
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (apply_fun (bump u) x) Hui).
We prove the intermediate claim Hbump0_cont: ∀u : set, u ∈ U → continuous_map X Tx R R_standard_topology (bump0 u).
Let u be given.
Assume HuU: u ∈ U.
We prove the intermediate claim Hc: continuous_map X Tx R R_standard_topology (bump u).
We prove the intermediate claim Hleft: (continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1)) ∧ (∀x0 : set, x0 ∈ (X ∖ (pickV u)) → apply_fun (bump u) x0 = 0).
An exact proof term for the current goal is (andEL ((continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1)) ∧ (∀x0 : set, x0 ∈ (X ∖ (pickV u)) → apply_fun (bump u) x0 = 0)) (∀x0 : set, x0 ∈ X → apply_fun (bump u) x0 ∈ unit_interval) (Hbump u HuU)).
We prove the intermediate claim Hab: continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1)) (∀x0 : set, x0 ∈ (X ∖ (pickV u)) → apply_fun (bump u) x0 = 0) Hleft).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology (bump u)) (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1) Hab).
We prove the intermediate claim Hfun: function_on (bump0 u) X R.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hui: apply_fun (bump0 u) x ∈ unit_interval.
Set g to be the term (λx0 : set ⇒ apply_fun (bump u) x0).
We prove the intermediate claim Hb0eq: bump0 u = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ (pickV u)) → apply_fun (bump u) x0 = 0)) (∀x0 : set, x0 ∈ X → apply_fun (bump u) x0 ∈ unit_interval) (Hbump u HuU) x HxX).
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (apply_fun (bump0 u) x) Hui).
We prove the intermediate claim Heq: ∀x : set, x ∈ X → apply_fun (bump u) x = apply_fun (bump0 u) x.
Let x be given.
Assume HxX: x ∈ X.
Set g to be the term (λx0 : set ⇒ apply_fun (bump u) x0).
We prove the intermediate claim Hb0eq: bump0 u = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (continuous_map_congr_on X Tx R R_standard_topology (bump u) (bump0 u) Hc Hfun Heq).
We prove the intermediate claim Hbump0_unit_interval: ∀u x : set, u ∈ U → x ∈ X → apply_fun (bump0 u) x ∈ unit_interval.
Let u and x be given.
Assume HuU: u ∈ U.
Assume HxX: x ∈ X.
Set g to be the term (λx0 : set ⇒ apply_fun (bump u) x0).
We prove the intermediate claim Hb0eq: bump0 u = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ (pickV u)) → apply_fun (bump u) x0 = 0)) (∀x0 : set, x0 ∈ X → apply_fun (bump u) x0 ∈ unit_interval) (Hbump u HuU) x HxX).
We prove the intermediate claim Hbump0_domW: ∀u : set, u ∈ U → support_of X Tx (bump0 u) ⊆ w_of_u u.
Let u be given.
Assume HuU: u ∈ U.
We prove the intermediate claim Hwpack: w_of_u u ∈ W ∧ closure_of X Tx (pickV u) ⊆ w_of_u u.
An exact proof term for the current goal is (Hw_of_u u HuU).
We prove the intermediate claim Hclvsubw: closure_of X Tx (pickV u) ⊆ w_of_u u.
An exact proof term for the current goal is (andER (w_of_u u ∈ W) (closure_of X Tx (pickV u) ⊆ w_of_u u) Hwpack).
We prove the intermediate claim Hvpack: pickV u ∈ V ∧ closure_of X Tx u ⊆ pickV u.
An exact proof term for the current goal is (HpickV u HuU).
We prove the intermediate claim HvV: pickV u ∈ V.
An exact proof term for the current goal is (andEL (pickV u ∈ V) (closure_of X Tx u ⊆ pickV u) Hvpack).
We prove the intermediate claim HvTx: pickV u ∈ Tx.
An exact proof term for the current goal is (HVmemTx (pickV u) HvV).
We prove the intermediate claim Hz: ∀x : set, x ∈ (X ∖ (pickV u)) → apply_fun (bump0 u) x = 0.
Let x be given.
Assume Hxout: x ∈ (X ∖ (pickV u)).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (pickV u) x Hxout).
Set g to be the term (λx0 : set ⇒ apply_fun (bump u) x0).
We prove the intermediate claim Hb0eq: bump0 u = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1)) (∀x0 : set, x0 ∈ (X ∖ (pickV u)) → apply_fun (bump u) x0 = 0) (andEL (continuous_map X Tx R R_standard_topology (bump u) ∧ (∀x0 : set, x0 ∈ closure_of X Tx u → apply_fun (bump u) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ (pickV u)) → apply_fun (bump u) x0 = 0)) (∀x0 : set, x0 ∈ X → apply_fun (bump u) x0 ∈ unit_interval) (Hbump u HuU)) x Hxout).
We prove the intermediate claim Hsuppsubclv: support_of X Tx (bump0 u) ⊆ closure_of X Tx (pickV u).
An exact proof term for the current goal is (support_of_zero_outside_open_sub_closure X Tx (bump0 u) (pickV u) HTx HvTx Hz).
An exact proof term for the current goal is (Subq_tra (support_of X Tx (bump0 u)) (closure_of X Tx (pickV u)) (w_of_u u) Hsuppsubclv Hclvsubw).
Set Ufiber to be the term λv : set ⇒ {u ∈ U|pickV u = v}.
Set u_big to be the term λv : set ⇒ ⋃ (Ufiber v).
Set bumpV to be the term λv : set ⇒ Eps_i (λf : set ⇒ continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ closure_of X Tx (u_big v) → apply_fun f x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → apply_fun f x ∈ unit_interval)).
Set bumpV0 to be the term λv : set ⇒ graph X (λx : set ⇒ apply_fun (bumpV v) x).
Set PV to be the term {bumpV0 v|v ∈ V}.
We prove the intermediate claim HbumpV: ∀v : set, v ∈ V → continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x : set, x ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun (bumpV v) x = 0) ∧ (∀x : set, x ∈ X → apply_fun (bumpV v) x ∈ unit_interval).
Let v be given.
Assume HvV: v ∈ V.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We prove the intermediate claim HvTx: v ∈ Tx.
An exact proof term for the current goal is (HVmemTx v HvV).
We prove the intermediate claim HLF_Ufiber: locally_finite_family X Tx (Ufiber v).
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ (Ufiber v) ∧ ∀A : set, A ∈ (Ufiber v) → A ∩ N ≠ Empty → A ∈ S.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HUprop: ∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ U ∧ ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ U ∧ ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S) HUlf).
We prove the intermediate claim HexN: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ U ∧ ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (HUprop x HxX).
Apply HexN to the current goal.
Let N be given.
Assume HNpack: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ U ∧ ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HN1: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ U ∧ ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S) HNpack).
We prove the intermediate claim HNTx: N ∈ Tx.
An exact proof term for the current goal is (andEL (N ∈ Tx) (x ∈ N) HN1).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HN1).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ U ∧ ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ U ∧ ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S) HNpack).
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ U ∧ ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ U) (andEL (finite S ∧ S ⊆ U) (∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S) HS)).
We prove the intermediate claim HSsubU: S ⊆ U.
An exact proof term for the current goal is (andER (finite S) (S ⊆ U) (andEL (finite S ∧ S ⊆ U) (∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S) HS)).
We prove the intermediate claim HSprop: ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ U) (∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S) HS).
Set S0 to be the term {u ∈ S|pickV u = v}.
We use N 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 HNTx.
An exact proof term for the current goal is HxN.
We use S0 to witness the existential quantifier.
We will prove (finite S0 ∧ S0 ⊆ Ufiber v) ∧ ∀A : set, A ∈ Ufiber v → A ∩ N ≠ Empty → A ∈ S0.
Apply andI to the current goal.
We will prove finite S0 ∧ S0 ⊆ Ufiber v.
Apply andI to the current goal.
We prove the intermediate claim HS0subS: S0 ⊆ S.
Let u be given.
Assume Hu: u ∈ S0.
An exact proof term for the current goal is (SepE1 S (λu0 : set ⇒ pickV u0 = v) u Hu).
An exact proof term for the current goal is (Subq_finite S HSfin S0 HS0subS).
Let u be given.
Assume Hu0: u ∈ S0.
We prove the intermediate claim HuS: u ∈ S.
An exact proof term for the current goal is (SepE1 S (λu0 : set ⇒ pickV u0 = v) u Hu0).
We prove the intermediate claim HuEq: pickV u = v.
An exact proof term for the current goal is (SepE2 S (λu0 : set ⇒ pickV u0 = v) u Hu0).
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (HSsubU u HuS).
An exact proof term for the current goal is (SepI U (λu0 : set ⇒ pickV u0 = v) u HuU HuEq).
Let A be given.
Assume HA: A ∈ Ufiber v.
Assume HAnN: A ∩ N ≠ Empty.
We will prove A ∈ S0.
We prove the intermediate claim HAU: A ∈ U.
An exact proof term for the current goal is (SepE1 U (λu0 : set ⇒ pickV u0 = v) A HA).
We prove the intermediate claim HAeq: pickV A = v.
An exact proof term for the current goal is (SepE2 U (λu0 : set ⇒ pickV u0 = v) A HA).
We prove the intermediate claim HAinS: A ∈ S.
An exact proof term for the current goal is (HSprop A HAU HAnN).
An exact proof term for the current goal is (SepI S (λu0 : set ⇒ pickV u0 = v) A HAinS HAeq).
We prove the intermediate claim Hu_big_sub_v: u_big v ⊆ v.
Let x be given.
Assume Hx: x ∈ u_big v.
Apply (UnionE_impred (Ufiber v) x Hx) to the current goal.
Let u be given.
Assume Hxu: x ∈ u.
Assume HuFib: u ∈ Ufiber v.
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (SepE1 U (λu0 : set ⇒ pickV u0 = v) u HuFib).
We prove the intermediate claim Hclu_sub_v: closure_of X Tx u ⊆ pickV u.
An exact proof term for the current goal is (andER (pickV u ∈ V) (closure_of X Tx u ⊆ pickV u) (HpickV u HuU)).
We prove the intermediate claim Hu_sub_clu: u ⊆ closure_of X Tx u.
An exact proof term for the current goal is (subset_of_closure X Tx u HTx (HUsubX u HuU)).
We prove the intermediate claim Hu_sub_v': u ⊆ pickV u.
An exact proof term for the current goal is (Subq_tra u (closure_of X Tx u) (pickV u) Hu_sub_clu Hclu_sub_v).
We prove the intermediate claim HuEq: pickV u = v.
An exact proof term for the current goal is (SepE2 U (λu0 : set ⇒ pickV u0 = v) u HuFib).
We prove the intermediate claim Hu_sub_v: u ⊆ v.
We will prove u ⊆ v.
rewrite the current goal using HuEq (from right to left).
An exact proof term for the current goal is Hu_sub_v'.
An exact proof term for the current goal is (Hu_sub_v x Hxu).
We prove the intermediate claim Hu_big_subX: u_big v ⊆ X.
Let x be given.
Assume Hx: x ∈ u_big v.
We prove the intermediate claim HvPow: v ∈ 𝒫 X.
An exact proof term for the current goal is (HTsubPow v (HVmemTx v HvV)).
We prove the intermediate claim HvSubX: v ⊆ X.
An exact proof term for the current goal is (PowerE X v HvPow).
An exact proof term for the current goal is (HvSubX x (Hu_big_sub_v x Hx)).
We prove the intermediate claim Hcl_u_big_sub_v: closure_of X Tx (u_big v) ⊆ v.
Set Fam to be the term Ufiber v.
Set ClFam to be the term {closure_of X Tx A|A ∈ Fam}.
We prove the intermediate claim HuBigDef: u_big v = ⋃ Fam.
Use reflexivity.
rewrite the current goal using HuBigDef (from left to right).
We prove the intermediate claim HFamSubX: ∀A : set, A ∈ Fam → A ⊆ X.
Let A be given.
Assume HA: A ∈ Fam.
We prove the intermediate claim HAU: A ∈ U.
An exact proof term for the current goal is (SepE1 U (λu0 : set ⇒ pickV u0 = v) A HA).
An exact proof term for the current goal is (HUsubX A HAU).
We prove the intermediate claim HLF: locally_finite_family X Tx Fam.
An exact proof term for the current goal is HLF_Ufiber.
We prove the intermediate claim HclSubUnionCl: closure_of X Tx (⋃ Fam) ⊆ ⋃ ClFam.
Let x be given.
Assume Hxcl: x ∈ closure_of X Tx (⋃ Fam).
We will prove x ∈ ⋃ ClFam.
Apply (xm (x ∈ ⋃ ClFam)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hnot: x ∉ ⋃ ClFam.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → U0 ∩ (⋃ Fam) ≠ Empty) x Hxcl).
We prove the intermediate claim HxNbhd: ∀U0 : set, U0 ∈ Tx → x ∈ U0 → U0 ∩ (⋃ Fam) ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → U0 ∩ (⋃ Fam) ≠ Empty) x Hxcl).
We prove the intermediate claim HexLF: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃N0 : set, N0 ∈ Tx ∧ x0 ∈ N0 ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N0 ≠ Empty → A ∈ S) HLF x HxX).
Apply HexLF to the current goal.
Let N be given.
Assume HN: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HN1: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HN).
We prove the intermediate claim HNTx: N ∈ Tx.
An exact proof term for the current goal is (andEL (N ∈ Tx) (x ∈ N) HN1).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HN1).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HN).
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HS1: finite S ∧ S ⊆ Fam.
An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ Fam) (∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HS).
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ Fam) HS1).
We prove the intermediate claim HSsubFam: S ⊆ Fam.
An exact proof term for the current goal is (andER (finite S) (S ⊆ Fam) HS1).
We prove the intermediate claim HSprop: ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ Fam) (∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HS).
Set sep_open to be the term λA : set ⇒ Eps_i (λU0 : set ⇒ U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ∩ A = Empty).
Set UFam to be the term {sep_open A|A ∈ S}.
We prove the intermediate claim HUFamFin: finite UFam.
An exact proof term for the current goal is (Repl_finite (λA : set ⇒ sep_open A) S HSfin).
We prove the intermediate claim HUFamSubTx: UFam ⊆ Tx.
Let U0 be given.
Assume HU0: U0 ∈ UFam.
Apply (ReplE_impred S (λA : set ⇒ sep_open A) U0 HU0 (U0 ∈ Tx)) to the current goal.
Let A be given.
Assume HA: A ∈ S.
Assume HUeq: U0 = sep_open A.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (HSsubFam A HA).
We prove the intermediate claim HxNotClA: x ∉ closure_of X Tx A.
Assume HxClA: x ∈ closure_of X Tx A.
We prove the intermediate claim HclAin: closure_of X Tx A ∈ ClFam.
An exact proof term for the current goal is (ReplI Fam (λA0 : set ⇒ closure_of X Tx A0) A HAFam).
We prove the intermediate claim HxInUnion: x ∈ ⋃ ClFam.
An exact proof term for the current goal is (UnionI ClFam x (closure_of X Tx A) HxClA HclAin).
An exact proof term for the current goal is (Hnot HxInUnion).
We prove the intermediate claim HAX: A ⊆ X.
An exact proof term for the current goal is (HFamSubX A HAFam).
We prove the intermediate claim HexU: ∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ∩ A = Empty.
An exact proof term for the current goal is (not_in_closure_has_disjoint_open X Tx A x HTx HAX HxX HxNotClA).
We prove the intermediate claim Hsep: (sep_open A) ∈ Tx ∧ x ∈ (sep_open A) ∧ (sep_open A) ∩ A = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU1 : set ⇒ U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ∩ A = Empty) HexU).
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HsepAB: (sep_open A) ∈ Tx ∧ x ∈ (sep_open A).
An exact proof term for the current goal is (andEL ((sep_open A) ∈ Tx ∧ x ∈ (sep_open A)) ((sep_open A) ∩ A = Empty) Hsep).
An exact proof term for the current goal is (andEL ((sep_open A) ∈ Tx) (x ∈ (sep_open A)) HsepAB).
We prove the intermediate claim HUFamPow: UFam ∈ 𝒫 Tx.
Apply PowerI to the current goal.
An exact proof term for the current goal is HUFamSubTx.
Set Uinter to be the term intersection_of_family X UFam.
We prove the intermediate claim HUinterTx: Uinter ∈ Tx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx UFam HTx HUFamPow HUFamFin).
Set M to be the term N ∩ Uinter.
We prove the intermediate claim HMTx: M ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx N Uinter HTx HNTx HUinterTx).
We prove the intermediate claim HxUinter: x ∈ Uinter.
We prove the intermediate claim HallUFam: ∀U0 : set, U0 ∈ UFam → x ∈ U0.
Let U0 be given.
Assume HU0: U0 ∈ UFam.
Apply (ReplE_impred S (λA : set ⇒ sep_open A) U0 HU0 (x ∈ U0)) to the current goal.
Let A be given.
Assume HA: A ∈ S.
Assume HUeq: U0 = sep_open A.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (HSsubFam A HA).
We prove the intermediate claim HxNotClA: x ∉ closure_of X Tx A.
Assume HxClA: x ∈ closure_of X Tx A.
We prove the intermediate claim HclAin: closure_of X Tx A ∈ ClFam.
An exact proof term for the current goal is (ReplI Fam (λA0 : set ⇒ closure_of X Tx A0) A HAFam).
We prove the intermediate claim HxInUnion: x ∈ ⋃ ClFam.
An exact proof term for the current goal is (UnionI ClFam x (closure_of X Tx A) HxClA HclAin).
An exact proof term for the current goal is (Hnot HxInUnion).
We prove the intermediate claim HAX: A ⊆ X.
An exact proof term for the current goal is (HFamSubX A HAFam).
We prove the intermediate claim HexU: ∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ∩ A = Empty.
An exact proof term for the current goal is (not_in_closure_has_disjoint_open X Tx A x HTx HAX HxX HxNotClA).
We prove the intermediate claim Hsep: (sep_open A) ∈ Tx ∧ x ∈ (sep_open A) ∧ (sep_open A) ∩ A = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU1 : set ⇒ U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ∩ A = Empty) HexU).
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HsepAB: (sep_open A) ∈ Tx ∧ x ∈ (sep_open A).
An exact proof term for the current goal is (andEL ((sep_open A) ∈ Tx ∧ x ∈ (sep_open A)) ((sep_open A) ∩ A = Empty) Hsep).
An exact proof term for the current goal is (andER ((sep_open A) ∈ Tx) (x ∈ (sep_open A)) HsepAB).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀U0 : set, U0 ∈ UFam → x0 ∈ U0) x HxX HallUFam).
We prove the intermediate claim HxM: x ∈ M.
An exact proof term for the current goal is (binintersectI N Uinter x HxN HxUinter).
We prove the intermediate claim HMEmpty: M ∩ (⋃ Fam) = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ M ∩ (⋃ Fam).
We will prove z ∈ Empty.
We prove the intermediate claim HzM: z ∈ M.
An exact proof term for the current goal is (binintersectE1 M (⋃ Fam) z Hz).
We prove the intermediate claim HzUF: z ∈ ⋃ Fam.
An exact proof term for the current goal is (binintersectE2 M (⋃ Fam) z Hz).
We prove the intermediate claim HzN: z ∈ N.
An exact proof term for the current goal is (binintersectE1 N Uinter z HzM).
We prove the intermediate claim HzUinter: z ∈ Uinter.
An exact proof term for the current goal is (binintersectE2 N Uinter z HzM).
Apply (UnionE_impred Fam z HzUF) to the current goal.
Let A0 be given.
Assume HzA0: z ∈ A0.
Assume HA0Fam: A0 ∈ Fam.
We prove the intermediate claim HA0Nnon: A0 ∩ N ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (A0 ∩ N) z (binintersectI A0 N z HzA0 HzN)).
We prove the intermediate claim HA0S: A0 ∈ S.
An exact proof term for the current goal is (HSprop A0 HA0Fam HA0Nnon).
We prove the intermediate claim HUA0: (sep_open A0) ∈ UFam.
An exact proof term for the current goal is (ReplI S (λA : set ⇒ sep_open A) A0 HA0S).
We prove the intermediate claim HzInSep: z ∈ sep_open A0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ UFam → x0 ∈ U0) z HzUinter (sep_open A0) HUA0).
We prove the intermediate claim HxNotClA0: x ∉ closure_of X Tx A0.
Assume HxClA0: x ∈ closure_of X Tx A0.
We prove the intermediate claim HclAin: closure_of X Tx A0 ∈ ClFam.
An exact proof term for the current goal is (ReplI Fam (λA1 : set ⇒ closure_of X Tx A1) A0 HA0Fam).
We prove the intermediate claim HxInUnion: x ∈ ⋃ ClFam.
An exact proof term for the current goal is (UnionI ClFam x (closure_of X Tx A0) HxClA0 HclAin).
An exact proof term for the current goal is (Hnot HxInUnion).
We prove the intermediate claim HA0X: A0 ⊆ X.
An exact proof term for the current goal is (HFamSubX A0 HA0Fam).
We prove the intermediate claim HexU: ∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ∩ A0 = Empty.
An exact proof term for the current goal is (not_in_closure_has_disjoint_open X Tx A0 x HTx HA0X HxX HxNotClA0).
We prove the intermediate claim Hsep: (sep_open A0) ∈ Tx ∧ x ∈ (sep_open A0) ∧ (sep_open A0) ∩ A0 = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU1 : set ⇒ U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ∩ A0 = Empty) HexU).
We prove the intermediate claim HsepEq: (sep_open A0) ∩ A0 = Empty.
An exact proof term for the current goal is (andER ((sep_open A0) ∈ Tx ∧ x ∈ (sep_open A0)) ((sep_open A0) ∩ A0 = Empty) Hsep).
We prove the intermediate claim HzInInt: z ∈ (sep_open A0) ∩ A0.
An exact proof term for the current goal is (binintersectI (sep_open A0) A0 z HzInSep HzA0).
rewrite the current goal using HsepEq (from right to left).
An exact proof term for the current goal is HzInInt.
We prove the intermediate claim Hcontra: M ∩ (⋃ Fam) ≠ Empty.
An exact proof term for the current goal is (HxNbhd M HMTx HxM).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hcontra HMEmpty).
We prove the intermediate claim HUnionClSubV: ⋃ ClFam ⊆ v.
Let x be given.
Assume HxU: x ∈ ⋃ ClFam.
Apply (UnionE_impred ClFam x HxU) to the current goal.
Let C be given.
Assume HxC: x ∈ C.
Assume HC: C ∈ ClFam.
Apply (ReplE_impred Fam (λA : set ⇒ closure_of X Tx A) C HC (x ∈ v)) to the current goal.
Let u be given.
Assume HuFam: u ∈ Fam.
Assume HCeq: C = closure_of X Tx u.
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (SepE1 U (λu0 : set ⇒ pickV u0 = v) u HuFam).
We prove the intermediate claim HuPick: pickV u ∈ V ∧ closure_of X Tx u ⊆ pickV u.
An exact proof term for the current goal is (HpickV u HuU).
We prove the intermediate claim HuClSubPick: closure_of X Tx u ⊆ pickV u.
An exact proof term for the current goal is (andER (pickV u ∈ V) (closure_of X Tx u ⊆ pickV u) HuPick).
We prove the intermediate claim HuEq: pickV u = v.
An exact proof term for the current goal is (SepE2 U (λu0 : set ⇒ pickV u0 = v) u HuFam).
We prove the intermediate claim HxClu: x ∈ closure_of X Tx u.
We will prove x ∈ closure_of X Tx u.
rewrite the current goal using HCeq (from right to left).
An exact proof term for the current goal is HxC.
rewrite the current goal using HuEq (from right to left).
An exact proof term for the current goal is (HuClSubPick x HxClu).
An exact proof term for the current goal is (Subq_tra (closure_of X Tx (⋃ Fam)) (⋃ ClFam) v HclSubUnionCl HUnionClSubV).
We prove the intermediate claim Hcl_u_big_closed: closed_in X Tx (closure_of X Tx (u_big v)).
An exact proof term for the current goal is (closure_is_closed X Tx (u_big v) HTx Hu_big_subX).
We prove the intermediate claim Hexf: ∃f : set, continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ closure_of X Tx (u_big v) → apply_fun f x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → apply_fun f x ∈ unit_interval).
An exact proof term for the current goal is (Urysohn_bump_closed_in_open X Tx (closure_of X Tx (u_big v)) v Hnorm Hcl_u_big_closed HvTx Hcl_u_big_sub_v).
Apply Hexf to the current goal.
Let f be given.
Assume Hf: continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ closure_of X Tx (u_big v) → apply_fun f x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → apply_fun f x ∈ unit_interval).
An exact proof term for the current goal is (Eps_i_ax (λf0 : set ⇒ continuous_map X Tx R R_standard_topology f0 ∧ (∀x : set, x ∈ closure_of X Tx (u_big v) → apply_fun f0 x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ X → apply_fun f0 x ∈ unit_interval)) f Hf).
We prove the intermediate claim HbumpV0_funspace: ∀v : set, v ∈ V → bumpV0 v ∈ function_space X R.
Let v be given.
Assume HvV: v ∈ V.
Set g to be the term (λx : set ⇒ apply_fun (bumpV v) x).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
Apply (graph_in_function_space X R g) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hui: apply_fun (bumpV v) x ∈ unit_interval.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0)) (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval) (HbumpV v HvV) x HxX).
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (apply_fun (bumpV v) x) Hui).
We prove the intermediate claim HbumpV0_cont: ∀v : set, v ∈ V → continuous_map X Tx R R_standard_topology (bumpV0 v).
Let v be given.
Assume HvV: v ∈ V.
We prove the intermediate claim Hc: continuous_map X Tx R R_standard_topology (bumpV v).
We prove the intermediate claim Hleft: (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1)) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0).
An exact proof term for the current goal is (andEL ((continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1)) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0)) (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval) (HbumpV v HvV)).
We prove the intermediate claim Hab: continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1)) (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0) Hleft).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology (bumpV v)) (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1) Hab).
We prove the intermediate claim Hfun: function_on (bumpV0 v) X R.
An exact proof term for the current goal is (function_on_of_function_space (bumpV0 v) X R (HbumpV0_funspace v HvV)).
We prove the intermediate claim Heq: ∀x : set, x ∈ X → apply_fun (bumpV v) x = apply_fun (bumpV0 v) x.
Let x be given.
Assume HxX: x ∈ X.
Set g to be the term (λx0 : set ⇒ apply_fun (bumpV v) x0).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (continuous_map_congr_on X Tx R R_standard_topology (bumpV v) (bumpV0 v) Hc Hfun Heq).
We prove the intermediate claim HbumpV0_unit_interval: ∀v x : set, v ∈ V → x ∈ X → apply_fun (bumpV0 v) x ∈ unit_interval.
Let v and x be given.
Assume HvV: v ∈ V.
Assume HxX: x ∈ X.
Set g to be the term (λx0 : set ⇒ apply_fun (bumpV v) x0).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0)) (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval) (HbumpV v HvV) x HxX).
We prove the intermediate claim HbumpV0_domW: ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ support_of X Tx (bumpV0 v) ⊆ w.
Let v be given.
Assume HvV: v ∈ V.
We prove the intermediate claim Hwpack: pickW v ∈ W ∧ closure_of X Tx v ⊆ pickW v.
An exact proof term for the current goal is (HpickW v HvV).
We prove the intermediate claim HwW: pickW v ∈ W.
An exact proof term for the current goal is (andEL (pickW v ∈ W) (closure_of X Tx v ⊆ pickW v) Hwpack).
We prove the intermediate claim Hclvsubw: closure_of X Tx v ⊆ pickW v.
An exact proof term for the current goal is (andER (pickW v ∈ W) (closure_of X Tx v ⊆ pickW v) Hwpack).
We prove the intermediate claim HvTx: v ∈ Tx.
An exact proof term for the current goal is (HVmemTx v HvV).
We prove the intermediate claim Hz: ∀x : set, x ∈ (X ∖ v) → apply_fun (bumpV0 v) x = 0.
Let x be given.
Assume Hxout: x ∈ (X ∖ v).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X v x Hxout).
Set g to be the term (λx0 : set ⇒ apply_fun (bumpV v) x0).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1)) (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0) (andEL (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0)) (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval) (HbumpV v HvV)) x Hxout).
We prove the intermediate claim Hsuppsubclv: support_of X Tx (bumpV0 v) ⊆ closure_of X Tx v.
An exact proof term for the current goal is (support_of_zero_outside_open_sub_closure X Tx (bumpV0 v) v HTx HvTx Hz).
We use (pickW v) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HwW.
An exact proof term for the current goal is (Subq_tra (support_of X Tx (bumpV0 v)) (closure_of X Tx v) (pickW v) Hsuppsubclv Hclvsubw).
We prove the intermediate claim HA: PV ⊆ function_space X R.
Let f be given.
Assume Hf: f ∈ PV.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f Hf) to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Assume Hfeq: f = bumpV0 v.
rewrite the current goal using Hfeq (from left to right).
An exact proof term for the current goal is (HbumpV0_funspace v HvV).
We prove the intermediate claim HB: ∀f : set, f ∈ PV → continuous_map X Tx R R_standard_topology f.
Let f be given.
Assume Hf: f ∈ PV.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f Hf) to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Assume Hfeq: f = bumpV0 v.
rewrite the current goal using Hfeq (from left to right).
An exact proof term for the current goal is (HbumpV0_cont v HvV).
We prove the intermediate claim HC: ∀f x : set, f ∈ PV → x ∈ X → apply_fun f x ∈ unit_interval.
Let f and x be given.
Assume Hf: f ∈ PV.
Assume HxX: x ∈ X.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f Hf) to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Assume Hfeq: f = bumpV0 v.
rewrite the current goal using Hfeq (from left to right).
An exact proof term for the current goal is (HbumpV0_unit_interval v x HvV HxX).
We prove the intermediate claim HD: ∀f : set, f ∈ PV → ∃w : set, w ∈ W ∧ support_of X Tx f ⊆ w.
Let f be given.
Assume Hf: f ∈ PV.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f Hf) to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Assume Hfeq: f = bumpV0 v.
rewrite the current goal using Hfeq (from left to right).
An exact proof term for the current goal is (HbumpV0_domW v HvV).
We prove the intermediate claim HE: ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ PV ∧ ∀f : set, f ∈ PV → support_of X Tx f ∩ N ≠ Empty → f ∈ F0.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HVprop: ∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S) HVlf).
We prove the intermediate claim HVx: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (HVprop x HxX).
Apply HVx to the current goal.
Let N be given.
Assume HNpack: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HN1: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S) HNpack).
We prove the intermediate claim HNTx: N ∈ Tx.
An exact proof term for the current goal is (andEL (N ∈ Tx) (x ∈ N) HN1).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HN1).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S) HNpack).
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HS1: finite S ∧ S ⊆ V.
An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ V) (∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S) HS).
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ V) HS1).
We prove the intermediate claim HSsubV: S ⊆ V.
An exact proof term for the current goal is (andER (finite S) (S ⊆ V) HS1).
We prove the intermediate claim HSprop: ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ V) (∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S) HS).
Set F0 to be the term {bumpV0 v|v ∈ S}.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1.
We use F0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (Repl_finite (λv0 : set ⇒ bumpV0 v0) S HSfin).
Let f be given.
Assume Hf0: f ∈ F0.
Apply (ReplE_impred S (λv0 : set ⇒ bumpV0 v0) f Hf0) to the current goal.
Let v be given.
Assume HvS: v ∈ S.
Assume Hfeq: f = bumpV0 v.
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (HSsubV v HvS).
rewrite the current goal using Hfeq (from left to right).
An exact proof term for the current goal is (ReplI V (λv0 : set ⇒ bumpV0 v0) v HvV).
Let f be given.
Assume HfPV: f ∈ PV.
Assume HsuppMeet: support_of X Tx f ∩ N ≠ Empty.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f HfPV) to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Assume Hfeq: f = bumpV0 v.
We prove the intermediate claim HsuppMeetV: support_of X Tx (bumpV0 v) ∩ N ≠ Empty.
We will prove support_of X Tx (bumpV0 v) ∩ N ≠ Empty.
rewrite the current goal using Hfeq (from right to left).
An exact proof term for the current goal is HsuppMeet.
We prove the intermediate claim HvTx: v ∈ Tx.
An exact proof term for the current goal is (HVmemTx v HvV).
We prove the intermediate claim Hz: ∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV0 v) x0 = 0.
Let x0 be given.
Assume Hx0out: x0 ∈ (X ∖ v).
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (setminusE1 X v x0 Hx0out).
Set g to be the term (λt : set ⇒ apply_fun (bumpV v) t).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x0 Hx0X) (from left to right).
We prove the intermediate claim Habcd: continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x : set, x ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun (bumpV v) x = 0) ∧ (∀x : set, x ∈ X → apply_fun (bumpV v) x ∈ unit_interval).
An exact proof term for the current goal is (HbumpV v HvV).
We prove the intermediate claim Habc: (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x : set, x ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun (bumpV v) x = 0)).
An exact proof term for the current goal is (andEL ((continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x : set, x ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun (bumpV v) x = 0))) (∀x : set, x ∈ X → apply_fun (bumpV v) x ∈ unit_interval) Habcd).
We prove the intermediate claim Hzero: ∀x : set, x ∈ (X ∖ v) → apply_fun (bumpV v) x = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x : set, x ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x = 1)) (∀x : set, x ∈ (X ∖ v) → apply_fun (bumpV v) x = 0) Habc).
An exact proof term for the current goal is (Hzero x0 Hx0out).
We prove the intermediate claim Hsuppsubclv: support_of X Tx (bumpV0 v) ⊆ closure_of X Tx v.
An exact proof term for the current goal is (support_of_zero_outside_open_sub_closure X Tx (bumpV0 v) v HTx HvTx Hz).
We prove the intermediate claim HvMeet: v ∩ N ≠ Empty.
We prove the intermediate claim Hexy: ∃y : set, y ∈ (support_of X Tx (bumpV0 v) ∩ N).
Apply (nonempty_has_element (support_of X Tx (bumpV0 v) ∩ N)) to the current goal.
An exact proof term for the current goal is HsuppMeetV.
Apply Hexy to the current goal.
Let y be given.
Assume Hy: y ∈ (support_of X Tx (bumpV0 v) ∩ N).
We prove the intermediate claim HySupp: y ∈ support_of X Tx (bumpV0 v).
An exact proof term for the current goal is (binintersectE1 (support_of X Tx (bumpV0 v)) N y Hy).
We prove the intermediate claim HyN: y ∈ N.
An exact proof term for the current goal is (binintersectE2 (support_of X Tx (bumpV0 v)) N y Hy).
We prove the intermediate claim Hyclv: y ∈ closure_of X Tx v.
An exact proof term for the current goal is (Hsuppsubclv y HySupp).
We prove the intermediate claim HyProp: ∀U0 : set, U0 ∈ Tx → y ∈ U0 → U0 ∩ v ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ ∀U0 : set, U0 ∈ Tx → y0 ∈ U0 → U0 ∩ v ≠ Empty) y Hyclv).
We prove the intermediate claim HNv: N ∩ v ≠ Empty.
An exact proof term for the current goal is (HyProp N HNTx HyN).
rewrite the current goal using (binintersect_com v N) (from left to right).
An exact proof term for the current goal is HNv.
We prove the intermediate claim HvS: v ∈ S.
An exact proof term for the current goal is (HSprop v HvV HvMeet).
rewrite the current goal using Hfeq (from left to right).
An exact proof term for the current goal is (ReplI S (λv0 : set ⇒ bumpV0 v0) v HvS).
We prove the intermediate claim HFone: ∀x : set, x ∈ X → ∃f : set, f ∈ PV ∧ apply_fun f x = 1.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HUcovers: covers X U.
An exact proof term for the current goal is (andER (∀u0 : set, u0 ∈ U → u0 ∈ Tx) (covers X U) HUcov).
Apply (HUcovers x HxX) to the current goal.
Let u be given.
Assume Hux: u ∈ U ∧ x ∈ u.
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (andEL (u ∈ U) (x ∈ u) Hux).
We prove the intermediate claim Hxu: x ∈ u.
An exact proof term for the current goal is (andER (u ∈ U) (x ∈ u) Hux).
Set v to be the term pickV u.
We prove the intermediate claim Hvpack: v ∈ V ∧ closure_of X Tx u ⊆ v.
An exact proof term for the current goal is (HpickV u HuU).
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (andEL (v ∈ V) (closure_of X Tx u ⊆ v) Hvpack).
We prove the intermediate claim HuSubX: u ⊆ X.
An exact proof term for the current goal is (HUsubX u HuU).
We prove the intermediate claim HuFib: u ∈ Ufiber v.
We prove the intermediate claim HUfiberDef: Ufiber v = {u0 ∈ U|pickV u0 = v}.
Use reflexivity.
rewrite the current goal using HUfiberDef (from left to right).
We prove the intermediate claim Hpu: pickV u = v.
Use reflexivity.
An exact proof term for the current goal is (SepI U (λu0 : set ⇒ pickV u0 = v) u HuU Hpu).
We prove the intermediate claim HxUb: x ∈ u_big v.
An exact proof term for the current goal is (UnionI (Ufiber v) x u Hxu HuFib).
We prove the intermediate claim HUfibPow: Ufiber v ⊆ 𝒫 X.
Let u0 be given.
Assume Hu0: u0 ∈ Ufiber v.
We prove the intermediate claim Hu0U: u0 ∈ U.
An exact proof term for the current goal is (SepE1 U (λu1 : set ⇒ pickV u1 = v) u0 Hu0).
We prove the intermediate claim Hu0subX: u0 ⊆ X.
An exact proof term for the current goal is (HUsubX u0 Hu0U).
An exact proof term for the current goal is (PowerI X u0 Hu0subX).
We prove the intermediate claim HubsubX: u_big v ⊆ X.
An exact proof term for the current goal is (Union_Power X (Ufiber v) HUfibPow).
We prove the intermediate claim HxClBig: x ∈ closure_of X Tx (u_big v).
An exact proof term for the current goal is ((closure_contains_set X Tx (u_big v) HTx HubsubX) x HxUb).
We prove the intermediate claim Habcd: continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0) ∧ (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval).
An exact proof term for the current goal is (HbumpV v HvV).
We prove the intermediate claim Habc: (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0)).
An exact proof term for the current goal is (andEL ((continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0))) (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval) Habcd).
We prove the intermediate claim Hab: continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1)) (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0) Habc).
We prove the intermediate claim Hbv: ∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology (bumpV v)) (∀x0 : set, x0 ∈ closure_of X Tx (u_big v) → apply_fun (bumpV v) x0 = 1) Hab).
We use (bumpV0 v) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI V (λv0 : set ⇒ bumpV0 v0) v HvV).
We prove the intermediate claim Hb0def: bumpV0 v = graph X (λx0 : set ⇒ apply_fun (bumpV v) x0).
Use reflexivity.
rewrite the current goal using Hb0def (from left to right).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun (bumpV v) x0) x HxX) (from left to right).
An exact proof term for the current goal is (Hbv x HxClBig).
We prove the intermediate claim HVsubW: ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w.
We prove the intermediate claim HV1: (open_cover X Tx V ∧ locally_finite_family X Tx V) ∧ (∀v0 : set, v0 ∈ V → ∃w : set, w ∈ W ∧ v0 ⊆ w).
An exact proof term for the current goal is (andEL ((open_cover X Tx V ∧ locally_finite_family X Tx V) ∧ (∀v0 : set, v0 ∈ V → ∃w : set, w ∈ W ∧ v0 ⊆ w)) (∀v0 : set, v0 ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v0 ⊆ w) HV).
An exact proof term for the current goal is (andER (open_cover X Tx V ∧ locally_finite_family X Tx V) (∀v0 : set, v0 ∈ V → ∃w : set, w ∈ W ∧ v0 ⊆ w) HV1).
We prove the intermediate claim HVref: refine_of V W.
An exact proof term for the current goal is HVsubW.
We prove the intermediate claim HPpack: PV ⊆ function_space X R ∧ (∀f : set, f ∈ PV → continuous_map X Tx R R_standard_topology f) ∧ (∀f x : set, f ∈ PV → x ∈ X → apply_fun f x ∈ unit_interval) ∧ (∀f : set, f ∈ PV → ∃w : set, w ∈ W ∧ support_of X Tx f ⊆ w) ∧ (∀x : set, x ∈ X → ∃f : set, f ∈ PV ∧ apply_fun f x = 1) ∧ (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ PV ∧ ∀f : set, f ∈ PV → support_of X Tx f ∩ N ≠ Empty → f ∈ F0).
Apply and6I to the current goal.
An exact proof term for the current goal is HA.
An exact proof term for the current goal is HB.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is HD.
An exact proof term for the current goal is HFone.
An exact proof term for the current goal is HE.
We prove the intermediate claim HPdom: partition_of_unity_dominated X Tx W.
An exact proof term for the current goal is (locally_finite_bump_cover_normalizes_to_partition_of_unity_dominated X Tx W V PV HTx Hcov HVcov HVlf HVref HPpack).
An exact proof term for the current goal is (andER (topology_on X Tx ∧ open_cover X Tx W) (∃P : set, partition_of_unity_family X Tx W P) HPdom).
∎