Let X, Tx and A be given.
Assume HL: Lindelof_space X Tx.
Assume Hclosed: closed_in X Tx A.
We will prove Lindelof_space A (subspace_topology X Tx A).
We will prove topology_on A (subspace_topology X Tx A) ∧ ∀U : set, open_cover A (subspace_topology X Tx A) U → ∃V : set, countable_subcollection V U ∧ covers A V.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V) HL).
We prove the intermediate claim HLprop: ∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V) HL).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A Hclosed).
We prove the intermediate claim HexUc: ∃Uc : set, Uc ∈ Tx ∧ A = X ∖ Uc.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx A Hclosed).
Set Uc to be the term Eps_i (λU0 : set ⇒ U0 ∈ Tx ∧ A = X ∖ U0).
We prove the intermediate claim HUc: Uc ∈ Tx ∧ A = X ∖ Uc.
An exact proof term for the current goal is (Eps_i_ex (λU0 : set ⇒ U0 ∈ Tx ∧ A = X ∖ U0) HexUc).
We prove the intermediate claim HUcTx: Uc ∈ Tx.
An exact proof term for the current goal is (andEL (Uc ∈ Tx) (A = X ∖ Uc) HUc).
We prove the intermediate claim HAeq: A = X ∖ Uc.
An exact proof term for the current goal is (andER (Uc ∈ Tx) (A = X ∖ Uc) HUc).
We prove the intermediate claim HUcsubX: Uc ⊆ X.
We prove the intermediate claim HUcPow: Uc ∈ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx Uc HUcTx).
An exact proof term for the current goal is (PowerE X Uc HUcPow).
We prove the intermediate claim HXminusAeq: X ∖ A = Uc.
rewrite the current goal using HAeq (from left to right) at position 1.
An exact proof term for the current goal is (setminus_setminus_eq X Uc HUcsubX).
We prove the intermediate claim HXminusAinTx: X ∖ A ∈ Tx.
rewrite the current goal using HXminusAeq (from left to right).
An exact proof term for the current goal is HUcTx.
Apply andI to the current goal.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HAsubX).
Let U be given.
Assume HcoverA: open_cover A (subspace_topology X Tx A) U.
We will prove ∃V : set, countable_subcollection V U ∧ covers A V.
We prove the intermediate claim HUmem: ∀u : set, u ∈ U → u ∈ subspace_topology X Tx A.
An exact proof term for the current goal is (andEL (∀u : set, u ∈ U → u ∈ subspace_topology X Tx A) (covers A U) HcoverA).
We prove the intermediate claim HUAcover: covers A U.
An exact proof term for the current goal is (andER (∀u : set, u ∈ U → u ∈ subspace_topology X Tx A) (covers A U) HcoverA).
Set Wfam to be the term {V ∈ Tx|V ∩ A ∈ U}.
Set Uext to be the term Wfam ∪ {X ∖ A}.
We prove the intermediate claim HUext: open_cover X Tx Uext.
We will prove (∀u : set, u ∈ Uext → u ∈ Tx) ∧ covers X Uext.
Apply andI to the current goal.
Let u be given.
Assume Hu: u ∈ Uext.
We will prove u ∈ Tx.
Apply (binunionE Wfam {X ∖ A} u Hu) to the current goal.
Assume HuW: u ∈ Wfam.
An exact proof term for the current goal is (SepE1 Tx (λV0 : set ⇒ V0 ∩ A ∈ U) u HuW).
Assume HuSing: u ∈ {X ∖ A}.
We prove the intermediate claim Hueq: u = X ∖ A.
An exact proof term for the current goal is (SingE (X ∖ A) u HuSing).
rewrite the current goal using Hueq (from left to right).
An exact proof term for the current goal is HXminusAinTx.
We will prove covers X Uext.
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃u : set, u ∈ Uext ∧ x ∈ u.
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ x ∈ u.
An exact proof term for the current goal is (HUAcover x HxA).
Apply Hexu to the current goal.
Let u be given.
Assume Hupair: 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) Hupair).
We prove the intermediate claim Hxu: x ∈ u.
An exact proof term for the current goal is (andER (u ∈ U) (x ∈ u) Hupair).
We prove the intermediate claim HuSub: u ∈ subspace_topology X Tx A.
An exact proof term for the current goal is (HUmem u HuU).
We prove the intermediate claim HexV: ∃V ∈ Tx, u = V ∩ A.
An exact proof term for the current goal is (subspace_topologyE X Tx A u HuSub).
Apply HexV to the current goal.
Let V be given.
Assume HVpair: V ∈ Tx ∧ u = V ∩ A.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (u = V ∩ A) HVpair).
We prove the intermediate claim Hueq: u = V ∩ A.
An exact proof term for the current goal is (andER (V ∈ Tx) (u = V ∩ A) HVpair).
We use V to witness the existential quantifier.
We will prove V ∈ Uext ∧ x ∈ V.
Apply andI to the current goal.
We will prove V ∈ Uext.
Apply binunionI1 to the current goal.
We will prove V ∈ Wfam.
Apply SepI to the current goal.
An exact proof term for the current goal is HVTx.
We prove the intermediate claim HsubstU: ∀S T : set, S = T → S ∈ U → T ∈ U.
Let S and T be given.
Assume HeqST: S = T.
Assume HS: S ∈ U.
We will prove T ∈ U.
rewrite the current goal using HeqST (from right to left) at position 1.
An exact proof term for the current goal is HS.
An exact proof term for the current goal is (HsubstU u (V ∩ A) Hueq HuU).
We prove the intermediate claim HxVA: x ∈ V ∩ A.
We prove the intermediate claim Hsubstx: ∀S T : set, S = T → x ∈ S → x ∈ T.
Let S and T be given.
Assume HeqST: S = T.
Assume HxS: x ∈ S.
We will prove x ∈ T.
rewrite the current goal using HeqST (from right to left) at position 1.
An exact proof term for the current goal is HxS.
An exact proof term for the current goal is (Hsubstx u (V ∩ A) Hueq Hxu).
An exact proof term for the current goal is (binintersectE1 V A x HxVA).
Assume HxnotA: ¬ (x ∈ A).
We use (X ∖ A) to witness the existential quantifier.
Apply andI to the current goal.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (SingI (X ∖ A)).
An exact proof term for the current goal is (setminusI X A x HxX HxnotA).
We prove the intermediate claim HexV0: ∃V0 : set, countable_subcollection V0 Uext ∧ covers X V0.
An exact proof term for the current goal is (HLprop Uext HUext).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0: countable_subcollection V0 Uext ∧ covers X V0.
We prove the intermediate claim HV0subcoll: countable_subcollection V0 Uext.
An exact proof term for the current goal is (andEL (countable_subcollection V0 Uext) (covers X V0) HV0).
We prove the intermediate claim HV0coversX: covers X V0.
An exact proof term for the current goal is (andER (countable_subcollection V0 Uext) (covers X V0) HV0).
We prove the intermediate claim HV0sub: V0 ⊆ Uext.
An exact proof term for the current goal is (andEL (V0 ⊆ Uext) (countable_set V0) HV0subcoll).
We prove the intermediate claim HV0count: countable_set V0.
An exact proof term for the current goal is (andER (V0 ⊆ Uext) (countable_set V0) HV0subcoll).
Set V1 to be the term {V ∈ V0|V ≠ X ∖ A}.
We prove the intermediate claim HV1subV0: V1 ⊆ V0.
Let V be given.
Assume HV: V ∈ V1.
An exact proof term for the current goal is (SepE1 V0 (λV0 : set ⇒ V0 ≠ X ∖ A) V HV).
We prove the intermediate claim HV1count: countable_set V1.
We will prove countable_set V1.
An exact proof term for the current goal is (Subq_countable V1 V0 HV0count HV1subV0).
Set V to be the term {(W ∩ A)|W ∈ V1}.
We use V to witness the existential quantifier.
We will prove countable_subcollection V U ∧ covers A V.
Apply andI to the current goal.
We will prove countable_subcollection V U.
We will prove V ⊆ U ∧ countable_set V.
Apply andI to the current goal.
We will prove V ⊆ U.
Let u be given.
Assume Hu: u ∈ V.
We will prove u ∈ U.
Apply (ReplE V1 (λW : set ⇒ W ∩ A) u Hu) to the current goal.
Let W be given.
Assume HWpair: W ∈ V1 ∧ u = W ∩ A.
We prove the intermediate claim HW: W ∈ V1.
An exact proof term for the current goal is (andEL (W ∈ V1) (u = W ∩ A) HWpair).
We prove the intermediate claim Hueq: u = W ∩ A.
An exact proof term for the current goal is (andER (W ∈ V1) (u = W ∩ A) HWpair).
We prove the intermediate claim HWV0: W ∈ V0.
An exact proof term for the current goal is (HV1subV0 W HW).
We prove the intermediate claim HWUext: W ∈ Uext.
An exact proof term for the current goal is (HV0sub W HWV0).
We prove the intermediate claim HWneq: W ≠ X ∖ A.
An exact proof term for the current goal is (SepE2 V0 (λV0 : set ⇒ V0 ≠ X ∖ A) W HW).
We prove the intermediate claim HWWfam: W ∈ Wfam.
We will prove W ∈ Wfam.
Apply (binunionE' Wfam {X ∖ A} W (W ∈ Wfam)) to the current goal.
Assume HWf: W ∈ Wfam.
An exact proof term for the current goal is HWf.
Assume HWsing: W ∈ {X ∖ A}.
We prove the intermediate claim HWa: W = X ∖ A.
An exact proof term for the current goal is (SingE (X ∖ A) W HWsing).
An exact proof term for the current goal is (FalseE (HWneq HWa) (W ∈ Wfam)).
An exact proof term for the current goal is HWUext.
We prove the intermediate claim HWintU: W ∩ A ∈ U.
An exact proof term for the current goal is (SepE2 Tx (λV0 : set ⇒ V0 ∩ A ∈ U) W HWWfam).
rewrite the current goal using Hueq (from left to right).
An exact proof term for the current goal is HWintU.
An exact proof term for the current goal is (countable_image V1 HV1count (λW : set ⇒ W ∩ A)).
We will prove covers A V.
Let x be given.
Assume HxA: x ∈ A.
We will prove ∃u : set, u ∈ V ∧ x ∈ u.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate claim HexW: ∃W : set, W ∈ V0 ∧ x ∈ W.
An exact proof term for the current goal is (HV0coversX x HxX).
Apply HexW to the current goal.
Let W be given.
Assume HWpair: W ∈ V0 ∧ x ∈ W.
We prove the intermediate claim HWV0: W ∈ V0.
An exact proof term for the current goal is (andEL (W ∈ V0) (x ∈ W) HWpair).
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (andER (W ∈ V0) (x ∈ W) HWpair).
We prove the intermediate claim HWneq: W ≠ X ∖ A.
Assume HWa: W = X ∖ A.
We prove the intermediate claim Hxminus: x ∈ X ∖ A.
rewrite the current goal using HWa (from right to left).
An exact proof term for the current goal is HxW.
We prove the intermediate claim HxnotA: ¬ (x ∈ A).
An exact proof term for the current goal is (setminusE2 X A x Hxminus).
An exact proof term for the current goal is (HxnotA HxA).
We prove the intermediate claim HWV1: W ∈ V1.
Apply SepI to the current goal.
An exact proof term for the current goal is HWV0.
An exact proof term for the current goal is HWneq.
We use (W ∩ A) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI V1 (λW0 : set ⇒ W0 ∩ A) W HWV1).
An exact proof term for the current goal is (binintersectI W A x HxW HxA).
∎