We will prove paracompact_space (product_space ω (const_space_family ω R R_standard_topology)) (product_topology_full ω (const_space_family ω R R_standard_topology)).
We prove the intermediate claim Hmetr: metrizable (product_space ω (const_space_family ω R R_standard_topology)) (product_topology_full ω (const_space_family ω R R_standard_topology)).
We will prove ∃d : set, metric_on (product_space ω (const_space_family ω R R_standard_topology)) d ∧ metric_topology (product_space ω (const_space_family ω R R_standard_topology)) d = product_topology_full ω (const_space_family ω R R_standard_topology).
We use Romega_D_metric to witness the existential quantifier.
We prove the intermediate claim Hpair: metric_on R_omega_space Romega_D_metric ∧ Romega_D_metric_topology = R_omega_product_topology.
An exact proof term for the current goal is Romega_D_metric_induces_product_topology.
We prove the intermediate claim Hm: metric_on R_omega_space Romega_D_metric.
An exact proof term for the current goal is (andEL (metric_on R_omega_space Romega_D_metric) (Romega_D_metric_topology = R_omega_product_topology) Hpair).
We prove the intermediate claim Heq: Romega_D_metric_topology = R_omega_product_topology.
An exact proof term for the current goal is (andER (metric_on R_omega_space Romega_D_metric) (Romega_D_metric_topology = R_omega_product_topology) Hpair).
Apply andI to the current goal.
An exact proof term for the current goal is Hm.
We prove the intermediate claim Hdef: metric_topology R_omega_space Romega_D_metric = Romega_D_metric_topology.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
An exact proof term for the current goal is (metrizable_paracompact (product_space ω (const_space_family ω R R_standard_topology)) (product_topology_full ω (const_space_family ω R R_standard_topology)) Hmetr).
∎