Let X and Tx be given.
Assume HT: Tychonoff_space X Tx.
We will prove ∃Ty : set, compact_space (Stone_Cech_compactification X Tx) Ty ∧ Hausdorff_space (Stone_Cech_compactification X Tx) Ty.
Set C to be the term Stone_Cech_index X Tx.
Set Xi to be the term Stone_Cech_ambient_family X Tx.
Set P to be the term Stone_Cech_ambient_space X Tx.
Set Tp to be the term Stone_Cech_ambient_topology X Tx.
Set Img to be the term Stone_Cech_image X Tx.
Set Beta to be the term Stone_Cech_compactification X Tx.
Set Ty to be the term subspace_topology P Tp Beta.
We use Ty to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HcompP: compact_space P Tp.
We prove the intermediate claim HXi: Xi = const_space_family C unit_interval unit_interval_topology.
Use reflexivity.
Apply (Tychonoff_theorem C Xi) to the current goal.
Let i be given.
Assume Hi: i ∈ C.
rewrite the current goal using HXi (from left to right).
rewrite the current goal using (space_family_set_const_space_family C unit_interval unit_interval_topology i Hi) (from left to right).
rewrite the current goal using (space_family_topology_const_space_family C unit_interval unit_interval_topology i Hi) (from left to right).
An exact proof term for the current goal is unit_interval_compact_axiom.
We prove the intermediate claim HTp: topology_on P Tp.
An exact proof term for the current goal is (compact_space_topology P Tp HcompP).
We prove the intermediate claim HImgSub: Img ⊆ P.
Let p be given.
Assume Hp: p ∈ Img.
An exact proof term for the current goal is (SepE1 P (λq : set ⇒ ∃x : set, x ∈ X ∧ q = graph C (λf : set ⇒ apply_fun f x)) p Hp).
We prove the intermediate claim Hclosed: closed_in P Tp Beta.
An exact proof term for the current goal is (closure_is_closed P Tp Img HTp HImgSub).
An exact proof term for the current goal is (closed_subspace_compact P Tp Beta HcompP Hclosed).
We prove the intermediate claim HXi: Xi = const_space_family C unit_interval unit_interval_topology.
Use reflexivity.
We prove the intermediate claim HUIH: Hausdorff_space unit_interval unit_interval_topology.
An exact proof term for the current goal is (ex17_12_subspace_Hausdorff R R_standard_topology unit_interval R_standard_topology_Hausdorff unit_interval_sub_R).
We prove the intermediate claim HHfam: Hausdorff_spaces_family C Xi.
Let i be given.
Assume Hi: i ∈ C.
rewrite the current goal using HXi (from left to right).
rewrite the current goal using (space_family_set_const_space_family C unit_interval unit_interval_topology i Hi) (from left to right).
rewrite the current goal using (space_family_topology_const_space_family C unit_interval unit_interval_topology i Hi) (from left to right).
An exact proof term for the current goal is HUIH.
We prove the intermediate claim HhausP: Hausdorff_space P Tp.
An exact proof term for the current goal is (product_topology_full_Hausdorff_axiom C Xi HHfam).
We prove the intermediate claim HTp: topology_on P Tp.
An exact proof term for the current goal is (Hausdorff_space_topology P Tp HhausP).
We prove the intermediate claim HImgSub: Img ⊆ P.
Let p be given.
Assume Hp: p ∈ Img.
An exact proof term for the current goal is (SepE1 P (λq : set ⇒ ∃x : set, x ∈ X ∧ q = graph C (λf : set ⇒ apply_fun f x)) p Hp).
We prove the intermediate claim Hclosed: closed_in P Tp Beta.
An exact proof term for the current goal is (closure_is_closed P Tp Img HTp HImgSub).
We prove the intermediate claim HBetasub: Beta ⊆ P.
An exact proof term for the current goal is (closed_in_subset P Tp Beta Hclosed).
An exact proof term for the current goal is (ex17_12_subspace_Hausdorff P Tp Beta HhausP HBetasub).
∎