Let X, Tx and W be given.
Assume Hnorm: normal_space X Tx.
Assume HWcov: open_cover X Tx W.
Assume HWfin: finite W.
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) HWcov).
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) HWcov).
Set p to be the term λF : set ⇒ ∀A : set, closed_in X Tx A → A ⊆ ⋃ F → (∀w : set, w ∈ F → w ∈ Tx) → ∃V : set, finite V ∧ (∀v : set, v ∈ V → v ∈ Tx) ∧ A ⊆ ⋃ V ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ F ∧ closure_of X Tx v ⊆ w.
We prove the intermediate claim HpEmpty: p Empty.
Let A be given.
Assume HAcl: closed_in X Tx A.
Assume HAU: A ⊆ ⋃ Empty.
Assume HATx: ∀w : set, w ∈ Empty → w ∈ Tx.
We use Empty to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is finite_Empty.
Let v be given.
Assume Hv: v ∈ Empty.
An exact proof term for the current goal is (EmptyE v Hv (v ∈ Tx)).
An exact proof term for the current goal is HAU.
Let v be given.
Assume Hv: v ∈ Empty.
An exact proof term for the current goal is (EmptyE v Hv (∃w : set, w ∈ Empty ∧ closure_of X Tx v ⊆ w)).
We prove the intermediate claim HpStep: ∀F y : set, finite F → y ∉ F → p F → p (F ∪ {y}).
Let F and y be given.
Assume HFfin: finite F.
Assume HyNot: y ∉ F.
Assume HpF: p F.
Let A be given.
Assume HAcl: closed_in X Tx A.
Assume HAU: A ⊆ ⋃ (F ∪ {y}).
Assume HFTx: ∀w : set, w ∈ (F ∪ {y}) → w ∈ Tx.
We prove the intermediate claim HFtx: ∀w : set, w ∈ F → w ∈ Tx.
Let w be given.
Assume HwF: w ∈ F.
An exact proof term for the current goal is (HFTx w (binunionI1 F {y} w HwF)).
We prove the intermediate claim HyTx: y ∈ Tx.
An exact proof term for the current goal is (HFTx y (binunionI2 F {y} y (SingI y))).
Set A1 to be the term A ∖ y.
We prove the intermediate claim HA1cl: closed_in X Tx A1.
We prove the intermediate claim HcY: closed_in X Tx (X ∖ y).
An exact proof term for the current goal is (closed_of_open_complement X Tx y HTx HyTx).
We prove the intermediate claim HA1eq: A1 = A ∩ (X ∖ y).
Apply set_ext to the current goal.
Let x be given.
Assume HxA1: x ∈ A1.
We will prove x ∈ A ∩ (X ∖ y).
We prove the intermediate claim Hxpair: x ∈ A ∧ x ∉ y.
An exact proof term for the current goal is (setminusE A y x HxA1).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (andEL (x ∈ A) (x ∉ y) Hxpair).
We prove the intermediate claim Hxny: x ∉ y.
An exact proof term for the current goal is (andER (x ∈ A) (x ∉ y) Hxpair).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (A ⊆ X) (∃U ∈ Tx, A = X ∖ U) (closed_in_package X Tx A HAcl) x HxA).
An exact proof term for the current goal is (binintersectI A (X ∖ y) x HxA (setminusI X y x HxX Hxny)).
Let x be given.
Assume Hx: x ∈ A ∩ (X ∖ y).
We will prove x ∈ A1.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A (X ∖ y) x Hx).
We prove the intermediate claim HxXny: x ∈ X ∖ y.
An exact proof term for the current goal is (binintersectE2 A (X ∖ y) x Hx).
We prove the intermediate claim Hxny: x ∉ y.
An exact proof term for the current goal is (setminusE2 X y x HxXny).
An exact proof term for the current goal is (setminusI A y x HxA Hxny).
rewrite the current goal using HA1eq (from left to right).
An exact proof term for the current goal is (closed_binintersect X Tx A (X ∖ y) HAcl HcY).
We prove the intermediate claim HA1sub: A1 ⊆ ⋃ F.
Let x be given.
Assume HxA1: x ∈ A1.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (setminusE1 A y x HxA1).
We prove the intermediate claim Hxny: x ∉ y.
An exact proof term for the current goal is (setminusE2 A y x HxA1).
We prove the intermediate claim HxUFy: x ∈ ⋃ (F ∪ {y}).
An exact proof term for the current goal is (HAU x HxA).
Apply (UnionE_impred (F ∪ {y}) x HxUFy (x ∈ ⋃ F)) to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HU: U ∈ (F ∪ {y}).
Apply (binunionE F {y} U HU (x ∈ ⋃ F)) to the current goal.
Assume HUF: U ∈ F.
An exact proof term for the current goal is (UnionI F x U HxU HUF).
Assume HUy: U ∈ {y}.
We prove the intermediate claim HUeq: U = y.
An exact proof term for the current goal is (SingE y U HUy).
Apply FalseE to the current goal.
We prove the intermediate claim Hxy: x ∈ 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 (Hxny Hxy).
We prove the intermediate claim HexV1: ∃V1 : set, finite V1 ∧ (∀v : set, v ∈ V1 → v ∈ Tx) ∧ A1 ⊆ ⋃ V1 ∧ ∀v : set, v ∈ V1 → ∃w : set, w ∈ F ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (HpF A1 HA1cl HA1sub HFtx).
Apply HexV1 to the current goal.
Let V1 be given.
Assume HV1: finite V1 ∧ (∀v : set, v ∈ V1 → v ∈ Tx) ∧ A1 ⊆ ⋃ V1 ∧ ∀v : set, v ∈ V1 → ∃w : set, w ∈ F ∧ closure_of X Tx v ⊆ w.
We prove the intermediate claim HV1Tx: ∀v : set, v ∈ V1 → v ∈ Tx.
Apply (and4E (finite V1) (∀v : set, v ∈ V1 → v ∈ Tx) (A1 ⊆ ⋃ V1) (∀v : set, v ∈ V1 → ∃w : set, w ∈ F ∧ closure_of X Tx v ⊆ w) HV1) to the current goal.
Assume Hfin Htx Hsub Hmap.
An exact proof term for the current goal is Htx.
We prove the intermediate claim HA1V1: A1 ⊆ ⋃ V1.
Apply (and4E (finite V1) (∀v : set, v ∈ V1 → v ∈ Tx) (A1 ⊆ ⋃ V1) (∀v : set, v ∈ V1 → ∃w : set, w ∈ F ∧ closure_of X Tx v ⊆ w) HV1) to the current goal.
Assume Hfin Htx Hsub Hmap.
An exact proof term for the current goal is Hsub.
We prove the intermediate claim HV1clmap: ∀v : set, v ∈ V1 → ∃w : set, w ∈ F ∧ closure_of X Tx v ⊆ w.
Apply (and4E (finite V1) (∀v : set, v ∈ V1 → v ∈ Tx) (A1 ⊆ ⋃ V1) (∀v : set, v ∈ V1 → ∃w : set, w ∈ F ∧ closure_of X Tx v ⊆ w) HV1) to the current goal.
Assume Hfin Htx Hsub Hmap.
An exact proof term for the current goal is Hmap.
We prove the intermediate claim HV1fin: finite V1.
Apply (and4E (finite V1) (∀v : set, v ∈ V1 → v ∈ Tx) (A1 ⊆ ⋃ V1) (∀v : set, v ∈ V1 → ∃w : set, w ∈ F ∧ closure_of X Tx v ⊆ w) HV1) to the current goal.
Assume Hfin Htx Hsub Hmap.
An exact proof term for the current goal is Hfin.
We prove the intermediate claim HUnionV1Tx: ⋃ V1 ∈ Tx.
We prove the intermediate claim HV1subTx: V1 ⊆ Tx.
Let v be given.
Assume Hv: v ∈ V1.
An exact proof term for the current goal is (HV1Tx v Hv).
An exact proof term for the current goal is (topology_union_closed X Tx V1 HTx HV1subTx).
Set B to be the term A ∖ ⋃ V1.
We prove the intermediate claim HBcl: closed_in X Tx B.
We prove the intermediate claim HcComp: closed_in X Tx (X ∖ ⋃ V1).
An exact proof term for the current goal is (closed_of_open_complement X Tx (⋃ V1) HTx HUnionV1Tx).
We prove the intermediate claim HBeq: B = A ∩ (X ∖ ⋃ V1).
Apply set_ext to the current goal.
Let x be given.
Assume HxB: x ∈ B.
We will prove x ∈ A ∩ (X ∖ ⋃ V1).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (setminusE1 A (⋃ V1) x HxB).
We prove the intermediate claim HxNotUV1: x ∉ ⋃ V1.
An exact proof term for the current goal is (setminusE2 A (⋃ V1) x HxB).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (andEL (A ⊆ X) (∃U ∈ Tx, A = X ∖ U) (closed_in_package X Tx A HAcl)).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
An exact proof term for the current goal is (binintersectI A (X ∖ ⋃ V1) x HxA (setminusI X (⋃ V1) x HxX HxNotUV1)).
Let x be given.
Assume Hx: x ∈ A ∩ (X ∖ ⋃ V1).
We will prove x ∈ B.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A (X ∖ ⋃ V1) x Hx).
We prove the intermediate claim HxXc: x ∈ X ∖ ⋃ V1.
An exact proof term for the current goal is (binintersectE2 A (X ∖ ⋃ V1) x Hx).
We prove the intermediate claim HxNotUV1: x ∉ ⋃ V1.
An exact proof term for the current goal is (setminusE2 X (⋃ V1) x HxXc).
An exact proof term for the current goal is (setminusI A (⋃ V1) x HxA HxNotUV1).
rewrite the current goal using HBeq (from left to right).
An exact proof term for the current goal is (closed_binintersect X Tx A (X ∖ ⋃ V1) HAcl HcComp).
We prove the intermediate claim HBsuby: B ⊆ y.
Let x be given.
Assume HxB: x ∈ B.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (setminusE1 A (⋃ V1) x HxB).
We prove the intermediate claim HxNotUV1: x ∉ ⋃ V1.
An exact proof term for the current goal is (setminusE2 A (⋃ V1) x HxB).
Apply (xm (x ∈ y)) to the current goal.
Assume Hxy: x ∈ y.
An exact proof term for the current goal is Hxy.
Assume Hxny: x ∉ y.
We prove the intermediate claim HxA1: x ∈ A1.
An exact proof term for the current goal is (setminusI A y x HxA Hxny).
We prove the intermediate claim HxUV1: x ∈ ⋃ V1.
An exact proof term for the current goal is (HA1V1 x HxA1).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxNotUV1 HxUV1).
We prove the intermediate claim HexV2: ∃V2 : set, V2 ∈ Tx ∧ B ⊆ V2 ∧ closure_of X Tx V2 ⊆ y.
An exact proof term for the current goal is (normal_space_shrink_closed X Tx B y Hnorm HBcl HyTx HBsuby).
Apply HexV2 to the current goal.
Let V2 be given.
Assume HV2: V2 ∈ Tx ∧ B ⊆ V2 ∧ closure_of X Tx V2 ⊆ y.
We prove the intermediate claim HV2Tx: V2 ∈ Tx.
Apply (and3E (V2 ∈ Tx) (B ⊆ V2) (closure_of X Tx V2 ⊆ y) HV2) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H1.
We prove the intermediate claim HBV2: B ⊆ V2.
Apply (and3E (V2 ∈ Tx) (B ⊆ V2) (closure_of X Tx V2 ⊆ y) HV2) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H2.
We prove the intermediate claim HV2clsub: closure_of X Tx V2 ⊆ y.
Apply (and3E (V2 ∈ Tx) (B ⊆ V2) (closure_of X Tx V2 ⊆ y) HV2) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H3.
Set V to be the term V1 ∪ {V2}.
We use V to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is (binunion_finite V1 HV1fin {V2} (Sing_finite V2)).
Let v be given.
Assume Hv: v ∈ V.
Apply (binunionE V1 {V2} v Hv) to the current goal.
Assume Hv1: v ∈ V1.
An exact proof term for the current goal is (HV1Tx v Hv1).
Assume Hv2: v ∈ {V2}.
We prove the intermediate claim Heq: v = V2.
An exact proof term for the current goal is (SingE V2 v Hv2).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HV2Tx.
Let x be given.
Assume HxA: x ∈ A.
We will prove x ∈ ⋃ V.
We prove the intermediate claim HUnionEq: ⋃ V = (⋃ V1) ∪ V2.
An exact proof term for the current goal is (Union_binunion_singleton_eq V1 V2).
rewrite the current goal using HUnionEq (from left to right).
Apply (xm (x ∈ ⋃ V1)) to the current goal.
Assume HxUV1: x ∈ ⋃ V1.
An exact proof term for the current goal is (binunionI1 (⋃ V1) V2 x HxUV1).
Assume HxNotUV1: ¬ (x ∈ ⋃ V1).
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (setminusI A (⋃ V1) x HxA HxNotUV1).
We prove the intermediate claim HxV2: x ∈ V2.
An exact proof term for the current goal is (HBV2 x HxB).
An exact proof term for the current goal is (binunionI2 (⋃ V1) V2 x HxV2).
Let v be given.
Assume Hv: v ∈ V.
Apply (binunionE V1 {V2} v Hv) to the current goal.
Assume Hv1: v ∈ V1.
We prove the intermediate claim Hexw: ∃w : set, w ∈ F ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (HV1clmap v Hv1).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ F ∧ closure_of X Tx v ⊆ w.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 F {y} w (andEL (w ∈ F) (closure_of X Tx v ⊆ w) Hw)).
An exact proof term for the current goal is (andER (w ∈ F) (closure_of X Tx v ⊆ w) Hw).
Assume Hv2: v ∈ {V2}.
We prove the intermediate claim Heq: v = V2.
An exact proof term for the current goal is (SingE V2 v Hv2).
rewrite the current goal using Heq (from left to right).
We use y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI2 F {y} y (SingI y)).
An exact proof term for the current goal is HV2clsub.
We prove the intermediate claim HpW: p W.
An exact proof term for the current goal is (finite_ind p HpEmpty HpStep W HWfin).
We prove the intermediate claim HXcl: closed_in X Tx X.
An exact proof term for the current goal is (X_is_closed X Tx HTx).
We prove the intermediate claim HXsubUnionW: X ⊆ ⋃ W.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ x ∈ w.
An exact proof term for the current goal is (HWcovers x HxX).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ x ∈ w.
An exact proof term for the current goal is (UnionI W x w (andER (w ∈ W) (x ∈ w) Hw) (andEL (w ∈ W) (x ∈ w) Hw)).
We prove the intermediate claim HexV: ∃V : set, finite V ∧ (∀v : set, v ∈ V → v ∈ Tx) ∧ X ⊆ ⋃ V ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (HpW X HXcl HXsubUnionW HWTx).
Apply HexV to the current goal.
Let V be given.
Assume HV: finite V ∧ (∀v : set, v ∈ V → v ∈ Tx) ∧ X ⊆ ⋃ V ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
We prove the intermediate claim HVfin: finite V.
Apply (and4E (finite V) (∀v : set, v ∈ V → v ∈ Tx) (X ⊆ ⋃ V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hfin Htx Hsub Hmap.
An exact proof term for the current goal is Hfin.
We prove the intermediate claim HVTx: ∀v : set, v ∈ V → v ∈ Tx.
Apply (and4E (finite V) (∀v : set, v ∈ V → v ∈ Tx) (X ⊆ ⋃ V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hfin Htx Hsub Hmap.
An exact proof term for the current goal is Htx.
We prove the intermediate claim HXUnionV: X ⊆ ⋃ V.
Apply (and4E (finite V) (∀v : set, v ∈ V → v ∈ Tx) (X ⊆ ⋃ V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hfin Htx Hsub Hmap.
An exact proof term for the current goal is Hsub.
We prove the intermediate claim HVclmap: ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
Apply (and4E (finite V) (∀v : set, v ∈ V → v ∈ Tx) (X ⊆ ⋃ V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hfin Htx Hsub Hmap.
An exact proof term for the current goal is Hmap.
We use V to witness the existential quantifier.
Apply and4I to the current goal.
We will prove (∀v : set, v ∈ V → v ∈ Tx) ∧ covers X V.
Apply andI to the current goal.
An exact proof term for the current goal is HVTx.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HxUV: x ∈ ⋃ V.
An exact proof term for the current goal is (HXUnionV x HxX).
Apply (UnionE V x HxUV) to the current goal.
Let U be given.
Assume HU: x ∈ U ∧ U ∈ V.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ V) HU).
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ V) HU).
An exact proof term for the current goal is HVfin.
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.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (w ∈ W) (closure_of X Tx v ⊆ w) Hw).
Let x be given.
Assume Hxv: x ∈ v.
We prove the intermediate claim HvsubX: v ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx v HTx (HVTx v HvV)).
We prove the intermediate claim Hxcl: x ∈ closure_of X Tx v.
An exact proof term for the current goal is (subset_of_closure X Tx v HTx HvsubX x Hxv).
An exact proof term for the current goal is ((andER (w ∈ W) (closure_of X Tx v ⊆ w) Hw) x Hxcl).
Let v be given.
Assume HvV: v ∈ V.
Apply (HVclmap v HvV) to the current goal.
∎