Let J be given.
Assume HJ: uncountable_set J.
We will prove ¬ paracompact_space (product_space J (const_space_family J R R_standard_topology)) (product_topology_full J (const_space_family J R R_standard_topology)).
Assume Hpara: paracompact_space (product_space J (const_space_family J R R_standard_topology)) (product_topology_full J (const_space_family J R R_standard_topology)).
We will prove False.
We prove the intermediate claim HHfam: Hausdorff_spaces_family J (const_space_family J R R_standard_topology).
Let i be given.
Assume Hi: i ∈ J.
We will prove Hausdorff_space (product_component (const_space_family J R R_standard_topology) i) (product_component_topology (const_space_family J R R_standard_topology) i).
rewrite the current goal using (product_component_def (const_space_family J R R_standard_topology) i) (from left to right).
rewrite the current goal using (product_component_topology_def (const_space_family J R R_standard_topology) i) (from left to right).
rewrite the current goal using (const_space_family_apply J R R_standard_topology i Hi) (from left to right).
rewrite the current goal using (tuple_2_0_eq R R_standard_topology) (from left to right).
rewrite the current goal using (tuple_2_1_eq R R_standard_topology) (from left to right).
An exact proof term for the current goal is R_standard_topology_Hausdorff.
We prove the intermediate claim HHprod: Hausdorff_space (product_space J (const_space_family J R R_standard_topology)) (product_topology_full J (const_space_family J R R_standard_topology)).
An exact proof term for the current goal is (product_topology_full_Hausdorff_axiom J (const_space_family J R R_standard_topology) HHfam).
We prove the intermediate claim Hnorm: normal_space (product_space J (const_space_family J R R_standard_topology)) (product_topology_full J (const_space_family J R R_standard_topology)).
An exact proof term for the current goal is (paracompact_Hausdorff_normal (product_space J (const_space_family J R R_standard_topology)) (product_topology_full J (const_space_family J R R_standard_topology)) Hpara HHprod).
We prove the intermediate claim Hnotnorm: ¬ normal_space (product_space J (const_space_family J R R_standard_topology)) (product_topology_full J (const_space_family J R R_standard_topology)).
An exact proof term for the current goal is (uncountable_product_R_not_normal J HJ).
An exact proof term for the current goal is (Hnotnorm Hnorm).
∎