We will prove continuous_map R R_lower_limit_topology R R_standard_topology {(x,x)|x ∈ R}.
We prove the intermediate claim Hstd: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim Hlower: topology_on R R_lower_limit_topology.
An exact proof term for the current goal is R_lower_limit_topology_is_topology.
Set idR to be the term {(x,x)|x ∈ R}.
We prove the intermediate claim HidStd: continuous_map R R_standard_topology R R_standard_topology idR.
An exact proof term for the current goal is (identity_continuous R R_standard_topology Hstd).
We prove the intermediate claim Hinc: R_standard_topology ⊆ R_lower_limit_topology.
An exact proof term for the current goal is R_lower_limit_finer_than_R_standard.
An exact proof term for the current goal is (continuous_map_domain_finer R R_standard_topology R_lower_limit_topology R R_standard_topology idR HidStd Hlower Hinc).
∎