Let Y be given.

Assume HYsub: Y ⊆ X.

Assume HcrX: completely_regular_space X Tx.

We will prove completely_regular_space Y (subspace_topology X Tx Y).

We prove the intermediate claim HTsub: 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 prove the intermediate claim HT1X: one_point_sets_closed X Tx.

An exact proof term for the current goal is (completely_regular_space_one_point_sets_closed X Tx HcrX).

We prove the intermediate claim HsingX: ∀x0 : set, x0 ∈ X → closed_in X Tx {x0}.

An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → closed_in X Tx {x0}) HT1X).

We will prove topology_on Y (subspace_topology X Tx Y) ∧ (one_point_sets_closed Y (subspace_topology X Tx Y) ∧ ∀y : set, y ∈ Y → ∀F : set, closed_in Y (subspace_topology X Tx Y) F → y ∉ F → ∃f : set, continuous_map Y (subspace_topology X Tx Y) R R_standard_topology f ∧ apply_fun f y = 0 ∧ ∀z : set, z ∈ F → apply_fun f z = 1).

Apply andI to the current goal.

An exact proof term for the current goal is HTsub.

Apply andI to the current goal.

We will prove topology_on Y (subspace_topology X Tx Y) ∧ ∀y0 : set, y0 ∈ Y → closed_in Y (subspace_topology X Tx Y) {y0}.

Apply andI to the current goal.

An exact proof term for the current goal is HTsub.

Let y0 be given.

Assume Hy0Y: y0 ∈ Y.

We will prove closed_in Y (subspace_topology X Tx Y) {y0}.

We prove the intermediate claim Hy0X: y0 ∈ X.

An exact proof term for the current goal is (HYsub y0 Hy0Y).

Apply (iffER (closed_in Y (subspace_topology X Tx Y) {y0}) (∃C : set, closed_in X Tx C ∧ {y0} = C ∩ Y) (closed_in_subspace_iff_intersection X Tx Y {y0} HTx HYsub)) to the current goal.

We use {y0} to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (HsingX y0 Hy0X).

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ {y0}.

We will prove z ∈ {y0} ∩ Y.

We prove the intermediate claim HzEq: z = y0.

An exact proof term for the current goal is (SingE y0 z Hz).

rewrite the current goal using HzEq (from left to right).

An exact proof term for the current goal is (binintersectI {y0} Y y0 (SingI y0) Hy0Y).

Let z be given.

Assume Hz: z ∈ {y0} ∩ Y.

We will prove z ∈ {y0}.

An exact proof term for the current goal is (binintersectE1 {y0} Y z Hz).

Let y be given.

Assume HyY: y ∈ Y.

Let F be given.

Assume HFcl: closed_in Y (subspace_topology X Tx Y) F.

Assume HynotF: y ∉ F.

We will prove ∃f : set, continuous_map Y (subspace_topology X Tx Y) R R_standard_topology f ∧ apply_fun f y = 0 ∧ ∀z : set, z ∈ F → apply_fun f z = 1.

We prove the intermediate claim HexC: ∃C : set, closed_in X Tx C ∧ F = C ∩ Y.

An exact proof term for the current goal is (iffEL (closed_in Y (subspace_topology X Tx Y) F) (∃C : set, closed_in X Tx C ∧ F = C ∩ Y) (closed_in_subspace_iff_intersection X Tx Y F HTx HYsub) HFcl).

Apply HexC to the current goal.

Let C be given.

Assume HCpair.

We prove the intermediate claim HCcl: closed_in X Tx C.

An exact proof term for the current goal is (andEL (closed_in X Tx C) (F = C ∩ Y) HCpair).

We prove the intermediate claim HFeq: F = C ∩ Y.

An exact proof term for the current goal is (andER (closed_in X Tx C) (F = C ∩ Y) HCpair).

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 HyNotC: y ∉ C.

Assume HyC: y ∈ C.

We prove the intermediate claim HyCY: y ∈ C ∩ Y.

An exact proof term for the current goal is (binintersectI C Y y HyC HyY).

We prove the intermediate claim HyF: y ∈ F.

rewrite the current goal using HFeq (from left to right).

An exact proof term for the current goal is HyCY.

An exact proof term for the current goal is (HynotF HyF).

We prove the intermediate claim Hexf: ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f y = 0 ∧ ∀z : set, z ∈ C → apply_fun f z = 1.

An exact proof term for the current goal is (completely_regular_space_separation X Tx y C HcrX HyX HCcl HyNotC).

Apply Hexf to the current goal.

Let f be given.

Assume Hfprop.

We use f to witness the existential quantifier.

We prove the intermediate claim Hfleft: continuous_map X Tx R R_standard_topology f ∧ apply_fun f y = 0.

An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f ∧ apply_fun f y = 0) (∀z : set, z ∈ C → apply_fun f z = 1) Hfprop).

We prove the intermediate claim Hfcont: continuous_map X Tx R R_standard_topology f.

An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f) (apply_fun f y = 0) Hfleft).

We prove the intermediate claim Hfy0: apply_fun f y = 0.

An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology f) (apply_fun f y = 0) Hfleft).

We prove the intermediate claim HfC: ∀z : set, z ∈ C → apply_fun f z = 1.

An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology f ∧ apply_fun f y = 0) (∀z : set, z ∈ C → apply_fun f z = 1) Hfprop).

Apply andI to the current goal.

We will prove continuous_map Y (subspace_topology X Tx Y) R R_standard_topology f ∧ apply_fun f y = 0.

Apply andI to the current goal.

An exact proof term for the current goal is (continuous_on_subspace X Tx R R_standard_topology f Y HTx HYsub Hfcont).

An exact proof term for the current goal is Hfy0.

Let z be given.

Assume HzF: z ∈ F.

We will prove apply_fun f z = 1.

We prove the intermediate claim HzCY: z ∈ C ∩ Y.

rewrite the current goal using HFeq (from right to left).

An exact proof term for the current goal is HzF.

We prove the intermediate claim HzC: z ∈ C.

An exact proof term for the current goal is (binintersectE1 C Y z HzCY).

An exact proof term for the current goal is (HfC z HzC).

Let I and Xi be given.

Assume Hfam: completely_regular_spaces_family I Xi.

We will prove completely_regular_space (product_space I Xi) (product_topology_full I Xi).

Apply (xm (I = Empty)) to the current goal.

Assume HIeq: I = Empty.

rewrite the current goal using HIeq (from left to right).

We prove the intermediate claim HXpeq: product_space Empty Xi = {Empty}.

An exact proof term for the current goal is (product_space_empty_index Xi).

We prove the intermediate claim HTp: topology_on (product_space Empty Xi) (product_topology_full Empty Xi).

An exact proof term for the current goal is (product_topology_full_empty_is_topology Xi).

We will prove topology_on (product_space Empty Xi) (product_topology_full Empty Xi) ∧ (one_point_sets_closed (product_space Empty Xi) (product_topology_full Empty Xi) ∧ ∀x : set, x ∈ product_space Empty Xi → ∀F : set, closed_in (product_space Empty Xi) (product_topology_full Empty Xi) F → x ∉ F → ∃f : set, continuous_map (product_space Empty Xi) (product_topology_full Empty Xi) R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1).

Apply andI to the current goal.

An exact proof term for the current goal is HTp.

Apply andI to the current goal.

We will prove topology_on (product_space Empty Xi) (product_topology_full Empty Xi) ∧ ∀x0 : set, x0 ∈ product_space Empty Xi → closed_in (product_space Empty Xi) (product_topology_full Empty Xi) {x0}.

Apply andI to the current goal.

An exact proof term for the current goal is HTp.

Let x0 be given.

Assume Hx0Xp: x0 ∈ product_space Empty Xi.

We prove the intermediate claim Hx0Sing: x0 ∈ {Empty}.

rewrite the current goal using HXpeq (from right to left).

An exact proof term for the current goal is Hx0Xp.

We prove the intermediate claim Hx0Eq: x0 = Empty.

An exact proof term for the current goal is (SingE Empty x0 Hx0Sing).

rewrite the current goal using Hx0Eq (from left to right).

We will prove closed_in (product_space Empty Xi) (product_topology_full Empty Xi) {Empty}.

Apply (closed_inI (product_space Empty Xi) (product_topology_full Empty Xi) {Empty} HTp) to the current goal.

We prove the intermediate claim Hem: Empty ∈ product_space Empty Xi.

rewrite the current goal using HXpeq (from left to right).

An exact proof term for the current goal is (SingI Empty).

An exact proof term for the current goal is (singleton_subset Empty (product_space Empty Xi) Hem).

We will prove ∃U ∈ product_topology_full Empty Xi, {Empty} = product_space Empty Xi ∖ U.

We use Empty to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (topology_has_empty (product_space Empty Xi) (product_topology_full Empty Xi) HTp).

rewrite the current goal using HXpeq (from left to right).

rewrite the current goal using (setminus_Empty_eq {Empty}) (from left to right).

Use reflexivity.

Let x be given.

Assume HxXp: x ∈ product_space Empty Xi.

Let F be given.

Assume HFcl: closed_in (product_space Empty Xi) (product_topology_full Empty Xi) F.

Assume HxnotF: x ∉ F.

We will prove ∃f : set, continuous_map (product_space Empty Xi) (product_topology_full Empty Xi) R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.

We use (const_fun (product_space Empty Xi) 0) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (const_fun_continuous (product_space Empty Xi) (product_topology_full Empty Xi) R R_standard_topology 0 HTp R_standard_topology_is_topology_local real_0).

We prove the intermediate claim Hfx: apply_fun (const_fun (product_space Empty Xi) 0) x = 0.

An exact proof term for the current goal is (const_fun_apply (product_space Empty Xi) 0 x HxXp).

An exact proof term for the current goal is Hfx.

Let y be given.

Assume HyF: y ∈ F.

We will prove apply_fun (const_fun (product_space Empty Xi) 0) y = 1.

We prove the intermediate claim HFsub: F ⊆ product_space Empty Xi.

An exact proof term for the current goal is (closed_in_subset (product_space Empty Xi) (product_topology_full Empty Xi) F HFcl).

We prove the intermediate claim HyXp: y ∈ product_space Empty Xi.

An exact proof term for the current goal is (HFsub y HyF).

We prove the intermediate claim HxEq: x = Empty.

We prove the intermediate claim HxSing: x ∈ {Empty}.

rewrite the current goal using HXpeq (from right to left).

An exact proof term for the current goal is HxXp.

An exact proof term for the current goal is (SingE Empty x HxSing).

We prove the intermediate claim HyEq: y = Empty.

We prove the intermediate claim HySing: y ∈ {Empty}.

rewrite the current goal using HXpeq (from right to left).

An exact proof term for the current goal is HyXp.

An exact proof term for the current goal is (SingE Empty y HySing).

We prove the intermediate claim Hyx: y = x.

rewrite the current goal using HyEq (from left to right).

rewrite the current goal using HxEq (from right to left).

Use reflexivity.

We prove the intermediate claim HxF: x ∈ F.

rewrite the current goal using Hyx (from right to left).

An exact proof term for the current goal is HyF.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HxnotF HxF).

Assume HIne: ¬ (I = Empty).

Set Xp to be the term product_space I Xi.

Set Tp to be the term product_topology_full I Xi.

We prove the intermediate claim HIne': I ≠ Empty.

Assume HI0: I = Empty.

An exact proof term for the current goal is (HIne HI0).

We prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).

Let i be given.

Assume HiI: i ∈ I.

We prove the intermediate claim Hcri: completely_regular_space (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (Hfam i HiI).

We prove the intermediate claim HsetEq: space_family_set Xi i = product_component Xi i.

Use reflexivity.

We prove the intermediate claim HtopEq: space_family_topology Xi i = product_component_topology Xi i.

Use reflexivity.

rewrite the current goal using HsetEq (from left to right).

rewrite the current goal using HtopEq (from left to right).

An exact proof term for the current goal is (completely_regular_space_topology_on (product_component Xi i) (product_component_topology Xi i) Hcri).

We prove the intermediate claim HSsub: subbasis_on Xp (product_subbasis_full I Xi).

An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIne' HcompTop).

We prove the intermediate claim HTp: topology_on Xp Tp.

An exact proof term for the current goal is (topology_from_subbasis_is_topology Xp (product_subbasis_full I Xi) HSsub).

We will prove topology_on Xp Tp ∧ (one_point_sets_closed Xp Tp ∧ ∀x : set, x ∈ Xp → ∀F : set, closed_in Xp Tp F → x ∉ F → ∃f : set, continuous_map Xp Tp R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1).

Apply andI to the current goal.

An exact proof term for the current goal is HTp.

Apply andI to the current goal.

We prove the intermediate claim HregFam: regular_spaces_family I Xi.

Let i be given.

Assume HiI: i ∈ I.

An exact proof term for the current goal is (completely_regular_space_implies_regular (product_component Xi i) (product_component_topology Xi i) (Hfam i HiI)).

We prove the intermediate claim HregProd: regular_space (product_space I Xi) (product_topology_full I Xi).

An exact proof term for the current goal is (product_topology_full_regular_axiom I Xi HregFam).

An exact proof term for the current goal is (andEL (one_point_sets_closed (product_space I Xi) (product_topology_full I Xi)) (∀x0 : set, x0 ∈ product_space I Xi → ∀F0 : set, closed_in (product_space I Xi) (product_topology_full I Xi) F0 → x0 ∉ F0 → ∃U V : set, U ∈ product_topology_full I Xi ∧ V ∈ product_topology_full I Xi ∧ x0 ∈ U ∧ F0 ⊆ V ∧ U ∩ V = Empty) HregProd).

Let x be given.

Assume HxXp: x ∈ Xp.

Let F be given.

Assume HFcl: closed_in Xp Tp F.

Assume HxnotF: x ∉ F.

We will prove ∃f : set, continuous_map Xp Tp R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.

Set U to be the term Xp ∖ F.

We prove the intermediate claim HUopen: open_in Xp Tp U.

An exact proof term for the current goal is (open_of_closed_complement Xp Tp F HFcl).

We prove the intermediate claim HUinTp: U ∈ Tp.

An exact proof term for the current goal is (andER (topology_on Xp Tp) (U ∈ Tp) HUopen).

We prove the intermediate claim HxU: x ∈ U.

Apply setminusI to the current goal.

An exact proof term for the current goal is HxXp.

An exact proof term for the current goal is HxnotF.

We prove the intermediate claim HexFin: ∃F0 : set, F0 ∈ finite_subcollections (product_subbasis_full I Xi) ∧ x ∈ intersection_of_family Xp F0 ∧ intersection_of_family Xp F0 ⊆ U.

An exact proof term for the current goal is (generated_topology_from_subbasis_finite_neighborhood Xp (product_subbasis_full I Xi) U x HSsub HUinTp HxU).

Apply HexFin to the current goal.

Let F0 be given.

Assume HF0pack.

We prove the intermediate claim HF0AB: F0 ∈ finite_subcollections (product_subbasis_full I Xi) ∧ x ∈ intersection_of_family Xp F0.

An exact proof term for the current goal is (andEL (F0 ∈ finite_subcollections (product_subbasis_full I Xi) ∧ x ∈ intersection_of_family Xp F0) (intersection_of_family Xp F0 ⊆ U) HF0pack).

We prove the intermediate claim HF0fin: F0 ∈ finite_subcollections (product_subbasis_full I Xi).

An exact proof term for the current goal is (andEL (F0 ∈ finite_subcollections (product_subbasis_full I Xi)) (x ∈ intersection_of_family Xp F0) HF0AB).

We prove the intermediate claim HxW: x ∈ intersection_of_family Xp F0.

An exact proof term for the current goal is (andER (F0 ∈ finite_subcollections (product_subbasis_full I Xi)) (x ∈ intersection_of_family Xp F0) HF0AB).

We prove the intermediate claim HWsubU: intersection_of_family Xp F0 ⊆ U.

An exact proof term for the current goal is (andER (F0 ∈ finite_subcollections (product_subbasis_full I Xi) ∧ x ∈ intersection_of_family Xp F0) (intersection_of_family Xp F0 ⊆ U) HF0pack).

We prove the intermediate claim Hexf: ∃f : set, continuous_map Xp Tp R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ Xp → (∃s : set, s ∈ F0 ∧ y ∉ s) → apply_fun f y = 1.

An exact proof term for the current goal is (product_finite_subbasis_intersection_separator I Xi F0 x HIne' Hfam HF0fin HxW).

Apply Hexf to the current goal.

Let f be given.

Assume Hfpack.

We use f to witness the existential quantifier.

We prove the intermediate claim Hfleft: continuous_map Xp Tp R R_standard_topology f ∧ apply_fun f x = 0.

An exact proof term for the current goal is (andEL (continuous_map Xp Tp R R_standard_topology f ∧ apply_fun f x = 0) (∀y : set, y ∈ Xp → (∃s : set, s ∈ F0 ∧ y ∉ s) → apply_fun f y = 1) Hfpack).

We prove the intermediate claim Hfsep: ∀y : set, y ∈ Xp → (∃s : set, s ∈ F0 ∧ y ∉ s) → apply_fun f y = 1.

An exact proof term for the current goal is (andER (continuous_map Xp Tp R R_standard_topology f ∧ apply_fun f x = 0) (∀y : set, y ∈ Xp → (∃s : set, s ∈ F0 ∧ y ∉ s) → apply_fun f y = 1) Hfpack).

Apply andI to the current goal.

An exact proof term for the current goal is Hfleft.

Let y be given.

Assume HyF: y ∈ F.

We will prove apply_fun f y = 1.

We prove the intermediate claim HyXp: y ∈ Xp.

An exact proof term for the current goal is (closed_in_subset Xp Tp F HFcl y HyF).

We prove the intermediate claim HyNotU: y ∉ U.

Assume HyU: y ∈ U.

We prove the intermediate claim HyNotF': y ∉ F.

An exact proof term for the current goal is (setminusE2 Xp F y HyU).

An exact proof term for the current goal is (HyNotF' HyF).

We prove the intermediate claim HyNotW: y ∉ intersection_of_family Xp F0.

Assume HyW: y ∈ intersection_of_family Xp F0.

We prove the intermediate claim HyU: y ∈ U.

An exact proof term for the current goal is (HWsubU y HyW).

An exact proof term for the current goal is (HyNotU HyU).

We prove the intermediate claim Hexs: ∃s : set, s ∈ F0 ∧ y ∉ s.

Apply (xm (∃s : set, s ∈ F0 ∧ y ∉ s)) to the current goal.

Assume Hex: ∃s : set, s ∈ F0 ∧ y ∉ s.

An exact proof term for the current goal is Hex.

Assume Hno: ¬ (∃s : set, s ∈ F0 ∧ y ∉ s).

We prove the intermediate claim Hall: ∀s : set, s ∈ F0 → y ∈ s.

Let s be given.

Assume HsF0: s ∈ F0.

Apply (xm (y ∈ s)) to the current goal.

Assume HyS: y ∈ s.

An exact proof term for the current goal is HyS.

Assume HyNotS: y ∉ s.

We prove the intermediate claim Hex0: ∃s0 : set, s0 ∈ F0 ∧ y ∉ s0.

We use s to witness the existential quantifier.

An exact proof term for the current goal is (andI (s ∈ F0) (y ∉ s) HsF0 HyNotS).

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hno Hex0).

We prove the intermediate claim HyW: y ∈ intersection_of_family Xp F0.

An exact proof term for the current goal is (intersection_of_familyI Xp F0 y HyXp Hall).

Apply FalseE to the current goal.

An exact proof term for the current goal is (HyNotW HyW).

An exact proof term for the current goal is (Hfsep y HyXp Hexs).