Let X, Tx, Y and n be given.
Assume HdimX: covering_dimension X Tx n.
Assume HYcl: closed_in X Tx Y.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (covering_dimension_topology_on X Tx n HdimX).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (covering_dimension_n_in_omega X Tx n HdimX).
We prove the intermediate claim HYsub: Y ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx Y HYcl).
We prove the intermediate claim HTy: topology_on Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HYsub).
We will prove covering_dimension Y (subspace_topology X Tx Y) n.
Apply (covering_dimensionI Y (subspace_topology X Tx Y) n) to the current goal.
An exact proof term for the current goal is HTy.
An exact proof term for the current goal is HnO.
Let A be given.
Assume HA: open_cover_of Y (subspace_topology X Tx Y) A.
We prove the intermediate claim HYpack: Y ⊆ X ∧ ∃U ∈ Tx, Y = X ∖ U.
An exact proof term for the current goal is (closed_in_package X Tx Y HYcl).
We prove the intermediate claim HexUc: ∃U ∈ Tx, Y = X ∖ U.
An exact proof term for the current goal is (andER (Y ⊆ X) (∃U ∈ Tx, Y = X ∖ U) HYpack).
Apply HexUc to the current goal.
Let Uc be given.
Assume HUcdata.
We prove the intermediate claim HUcTx: Uc ∈ Tx.
An exact proof term for the current goal is (andEL (Uc ∈ Tx) (Y = X ∖ Uc) HUcdata).
We prove the intermediate claim HYeq: Y = X ∖ Uc.
An exact proof term for the current goal is (andER (Uc ∈ Tx) (Y = X ∖ Uc) HUcdata).
We prove the intermediate claim HUcSubX: Uc ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx Uc HTx HUcTx).
We prove the intermediate claim HUcDisjointY: Uc ∩ Y = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ Uc ∩ Y.
We prove the intermediate claim HzUc: z ∈ Uc.
An exact proof term for the current goal is (binintersectE1 Uc Y z Hz).
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (binintersectE2 Uc Y z Hz).
We prove the intermediate claim HzXU: z ∈ X ∖ Uc.
An exact proof term for the current goal is (mem_eqR z Y (X ∖ Uc) HYeq HzY).
We prove the intermediate claim HznotUc: z ∉ Uc.
An exact proof term for the current goal is (setminusE2 X Uc z HzXU).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HznotUc HzUc).
Set Vset to be the term {V ∈ Tx|(V ∩ Y) ∈ A}.
Set A0 to be the term Vset ∪ {Uc}.
We prove the intermediate claim HA0: open_cover_of X Tx A0.
Apply (open_cover_ofI X Tx A0) to the current goal.
An exact proof term for the current goal is HTx.
Let W be given.
Assume HW: W ∈ A0.
Apply (binunionE Vset {Uc} W HW (W ∈ 𝒫 X)) to the current goal.
Assume HWV: W ∈ Vset.
We prove the intermediate claim HWT: W ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λV0 : set ⇒ (V0 ∩ Y) ∈ A) W HWV).
We prove the intermediate claim HWsub: W ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx W HTx HWT).
An exact proof term for the current goal is (PowerI X W HWsub).
Assume HWsing: W ∈ {Uc}.
We prove the intermediate claim HWeq: W = Uc.
An exact proof term for the current goal is (SingE Uc W HWsing).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is ((topology_sub_Power X Tx HTx) Uc HUcTx).
Let x be given.
Assume HxX: x ∈ X.
Apply (xm (x ∈ Y)) to the current goal.
Assume HxY: x ∈ Y.
We prove the intermediate claim HxUA: x ∈ ⋃ A.
An exact proof term for the current goal is (open_cover_of_covers Y (subspace_topology X Tx Y) A HA x HxY).
Apply (UnionE A x HxUA) to the current goal.
Let U be given.
Assume HxUpair: x ∈ U ∧ U ∈ A.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ A) HxUpair).
We prove the intermediate claim HUA: U ∈ A.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ A) HxUpair).
We prove the intermediate claim HUsub: U ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (open_cover_of_members_open Y (subspace_topology X Tx Y) A U HA HUA).
We prove the intermediate claim HexV: ∃V ∈ Tx, U = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HUsub).
Apply HexV to the current goal.
Let V be given.
Assume HVdata.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (U = V ∩ Y) HVdata).
We prove the intermediate claim HUeq: U = V ∩ Y.
An exact proof term for the current goal is (andER (V ∈ Tx) (U = V ∩ Y) HVdata).
We prove the intermediate claim HVin: V ∈ Vset.
Apply (SepI Tx (λV0 : set ⇒ (V0 ∩ Y) ∈ A) V) to the current goal.
An exact proof term for the current goal is HVTx.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HUA.
We prove the intermediate claim HVinA0: V ∈ A0.
An exact proof term for the current goal is (binunionI1 Vset {Uc} V HVin).
We prove the intermediate claim HxV: x ∈ V.
We prove the intermediate claim HxVy: x ∈ V ∩ Y.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (binintersectE1 V Y x HxVy).
An exact proof term for the current goal is (UnionI A0 x V HxV HVinA0).
Assume HxnotY: ¬ (x ∈ Y).
We prove the intermediate claim HxUc: x ∈ Uc.
Apply (xm (x ∈ Uc)) to the current goal.
Assume HxU.
An exact proof term for the current goal is HxU.
Assume HxnotU.
We prove the intermediate claim HxXU: x ∈ X ∖ Uc.
An exact proof term for the current goal is (setminusI X Uc x HxX HxnotU).
We prove the intermediate claim HxY': x ∈ Y.
An exact proof term for the current goal is (mem_eqL x Y (X ∖ Uc) HYeq HxXU).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotY HxY').
We prove the intermediate claim HUcA0: Uc ∈ A0.
An exact proof term for the current goal is (binunionI2 Vset {Uc} Uc (SingI Uc)).
An exact proof term for the current goal is (UnionI A0 x Uc HxUc HUcA0).
Let W be given.
Assume HW: W ∈ A0.
Apply (binunionE Vset {Uc} W HW (W ∈ Tx)) to the current goal.
Assume HWV: W ∈ Vset.
An exact proof term for the current goal is (SepE1 Tx (λV0 : set ⇒ (V0 ∩ Y) ∈ A) W HWV).
Assume HWsing: W ∈ {Uc}.
We prove the intermediate claim HWeq: W = Uc.
An exact proof term for the current goal is (SingE Uc W HWsing).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HUcTx.
We prove the intermediate claim HdimProp: ∀A1 : set, open_cover_of X Tx A1 → ∃B : set, open_cover_of X Tx B ∧ refines_cover B A1 ∧ collection_has_order_at_most_m_plus_one X B n.
Apply HdimX to the current goal.
Assume Hcore Hprop.
An exact proof term for the current goal is Hprop.
Apply (HdimProp A0 HA0) to the current goal.
Let B be given.
Assume HBpack.
We prove the intermediate claim HBcore: open_cover_of X Tx B ∧ refines_cover B A0.
An exact proof term for the current goal is (andEL (open_cover_of X Tx B ∧ refines_cover B A0) (collection_has_order_at_most_m_plus_one X B n) HBpack).
We prove the intermediate claim HBopen: open_cover_of X Tx B.
An exact proof term for the current goal is (andEL (open_cover_of X Tx B) (refines_cover B A0) HBcore).
We prove the intermediate claim HBrest: refines_cover B A0.
An exact proof term for the current goal is (andER (open_cover_of X Tx B) (refines_cover B A0) HBcore).
We prove the intermediate claim HBord: collection_has_order_at_most_m_plus_one X B n.
An exact proof term for the current goal is (andER (open_cover_of X Tx B ∧ refines_cover B A0) (collection_has_order_at_most_m_plus_one X B n) HBpack).
Set Bsub to be the term {V ∩ Y|V ∈ B, ¬ (V ∩ Y = Empty)}.
We use Bsub to witness the existential quantifier.
We will prove open_cover_of Y (subspace_topology X Tx Y) Bsub ∧ refines_cover Bsub A ∧ collection_has_order_at_most_m_plus_one Y Bsub n.
Apply andI to the current goal.
Apply andI to the current goal.
Apply (open_cover_ofI Y (subspace_topology X Tx Y) Bsub) to the current goal.
An exact proof term for the current goal is HTy.
Let W be given.
Assume HW: W ∈ Bsub.
Apply (ReplSepE_impred B (λV : set ⇒ ¬ (V ∩ Y = Empty)) (λV : set ⇒ V ∩ Y) W HW (W ∈ 𝒫 Y)) to the current goal.
Let V be given.
Assume HVB: V ∈ B.
Assume Hnz: ¬ (V ∩ Y = Empty).
Assume HWeq: W = V ∩ Y.
We prove the intermediate claim Hsub: V ∩ Y ⊆ Y.
An exact proof term for the current goal is (binintersect_Subq_2 V Y).
We prove the intermediate claim HWpow: V ∩ Y ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y (V ∩ Y) Hsub).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HWpow.
Let y be given.
Assume HyY: y ∈ Y.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HYsub y HyY).
We prove the intermediate claim HyUB: y ∈ ⋃ B.
An exact proof term for the current goal is (open_cover_of_covers X Tx B HBopen y HyX).
Apply (UnionE B y HyUB) to the current goal.
Let V be given.
Assume HyVpair: y ∈ V ∧ V ∈ B.
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andEL (y ∈ V) (V ∈ B) HyVpair).
We prove the intermediate claim HVB: V ∈ B.
An exact proof term for the current goal is (andER (y ∈ V) (V ∈ B) HyVpair).
We prove the intermediate claim HyVy: y ∈ V ∩ Y.
An exact proof term for the current goal is (binintersectI V Y y HyV HyY).
We prove the intermediate claim Hnz: ¬ (V ∩ Y = Empty).
Assume Heq.
We prove the intermediate claim HyE: y ∈ Empty.
An exact proof term for the current goal is (mem_eqR y (V ∩ Y) Empty Heq HyVy).
An exact proof term for the current goal is (EmptyE y HyE).
We prove the intermediate claim HVinBsub: (V ∩ Y) ∈ Bsub.
An exact proof term for the current goal is (ReplSepI B (λV0 : set ⇒ ¬ (V0 ∩ Y = Empty)) (λV0 : set ⇒ V0 ∩ Y) V HVB Hnz).
An exact proof term for the current goal is (UnionI Bsub y (V ∩ Y) HyVy HVinBsub).
Let W be given.
Assume HW: W ∈ Bsub.
Apply (ReplSepE_impred B (λV : set ⇒ ¬ (V ∩ Y = Empty)) (λV : set ⇒ V ∩ Y) W HW (W ∈ subspace_topology X Tx Y)) to the current goal.
Let V be given.
Assume HVB: V ∈ B.
Assume Hnz: ¬ (V ∩ Y = Empty).
Assume HWeq: W = V ∩ Y.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (open_cover_of_members_open X Tx B V HBopen HVB).
We prove the intermediate claim HWsub: (V ∩ Y) ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (subspace_topologyI X Tx Y V HVTx).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HWsub.
Let W be given.
Assume HW: W ∈ Bsub.
Apply (ReplSepE_impred B (λV : set ⇒ ¬ (V ∩ Y = Empty)) (λV : set ⇒ V ∩ Y) W HW (∃U : set, U ∈ A ∧ W ⊆ U)) to the current goal.
Let V be given.
Assume HVB: V ∈ B.
Assume Hnz: ¬ (V ∩ Y = Empty).
Assume HWeq: W = V ∩ Y.
We prove the intermediate claim HexV0: ∃V0 : set, V0 ∈ A0 ∧ V ⊆ V0.
An exact proof term for the current goal is (HBrest V HVB).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0pair.
We prove the intermediate claim HV0A0: V0 ∈ A0.
An exact proof term for the current goal is (andEL (V0 ∈ A0) (V ⊆ V0) HV0pair).
We prove the intermediate claim HVsubV0: V ⊆ V0.
An exact proof term for the current goal is (andER (V0 ∈ A0) (V ⊆ V0) HV0pair).
We prove the intermediate claim HV0notUc: V0 ≠ Uc.
Assume HV0eq.
We prove the intermediate claim HVsubUc: V ⊆ Uc.
rewrite the current goal using HV0eq (from right to left).
An exact proof term for the current goal is HVsubV0.
We prove the intermediate claim Hempty: V ∩ Y = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ V ∩ Y.
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE1 V Y z Hz).
We prove the intermediate claim HzUc: z ∈ Uc.
An exact proof term for the current goal is (HVsubUc z HzV).
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (binintersectE2 V Y z Hz).
We prove the intermediate claim HzXU: z ∈ X ∖ Uc.
An exact proof term for the current goal is (mem_eqR z Y (X ∖ Uc) HYeq HzY).
We prove the intermediate claim HznotUc: z ∉ Uc.
An exact proof term for the current goal is (setminusE2 X Uc z HzXU).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HznotUc HzUc).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnz Hempty).
We prove the intermediate claim HV0Vset: V0 ∈ Vset.
Apply (binunionE Vset {Uc} V0 HV0A0 (V0 ∈ Vset)) to the current goal.
Assume HV0V.
An exact proof term for the current goal is HV0V.
Assume HV0sing.
We prove the intermediate claim HV0eq: V0 = Uc.
An exact proof term for the current goal is (SingE Uc V0 HV0sing).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HV0notUc HV0eq).
We prove the intermediate claim HV0YinA: (V0 ∩ Y) ∈ A.
An exact proof term for the current goal is (SepE2 Tx (λV1 : set ⇒ (V1 ∩ Y) ∈ A) V0 HV0Vset).
We use (V0 ∩ Y) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV0YinA.
rewrite the current goal using HWeq (from left to right).
Let z be given.
Assume Hz: z ∈ V ∩ Y.
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE1 V Y z Hz).
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (binintersectE2 V Y z Hz).
We prove the intermediate claim HzV0: z ∈ V0.
An exact proof term for the current goal is (HVsubV0 z HzV).
An exact proof term for the current goal is (binintersectI V0 Y z HzV0 HzY).
We prove the intermediate claim HBsub0: Bsub ⊆ restrict_family_to_subspace B Y.
Let W be given.
Assume HW: W ∈ Bsub.
Apply (ReplSepE_impred B (λV : set ⇒ ¬ (V ∩ Y = Empty)) (λV : set ⇒ V ∩ Y) W HW (W ∈ restrict_family_to_subspace B Y)) to the current goal.
Let V be given.
Assume HVB: V ∈ B.
Assume Hnz: ¬ (V ∩ Y = Empty).
Assume HWeq: W = V ∩ Y.
We prove the intermediate claim HVres: (V ∩ Y) ∈ restrict_family_to_subspace B Y.
An exact proof term for the current goal is (ReplI B (λV0 : set ⇒ V0 ∩ Y) V HVB).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HVres.
We prove the intermediate claim HordRestr: collection_has_order_at_most_m_plus_one Y (restrict_family_to_subspace B Y) n.
An exact proof term for the current goal is (collection_has_order_at_most_m_plus_one_restrict_to_subspace X Y B n HnO HYsub HBord).
An exact proof term for the current goal is (collection_has_order_at_most_m_plus_one_mono_family Y Bsub (restrict_family_to_subspace B Y) n HnO HBsub0 HordRestr).
∎