Set j to be the term {(t,t)|t ∈ unit_interval}.
We will prove continuous_map unit_interval unit_interval_topology R R_standard_topology j.
We will prove topology_on unit_interval unit_interval_topology ∧ topology_on R R_standard_topology ∧ function_on j unit_interval R ∧ ∀V : set, V ∈ R_standard_topology → preimage_of unit_interval j V ∈ unit_interval_topology.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is unit_interval_topology_on.
An exact proof term for the current goal is R_standard_topology_is_topology.
Let a be given.
Assume HaI: a ∈ unit_interval.
We will prove apply_fun j a ∈ R.
rewrite the current goal using (identity_function_apply unit_interval a HaI) (from left to right).
An exact proof term for the current goal is (unit_interval_sub_R a HaI).
Let V be given.
Assume HV: V ∈ R_standard_topology.
We will prove preimage_of unit_interval j V ∈ unit_interval_topology.
We prove the intermediate claim Heq: preimage_of unit_interval j V = V ∩ unit_interval.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ preimage_of unit_interval j V.
We will prove a ∈ V ∩ unit_interval.
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λu : set ⇒ apply_fun j u ∈ V) a Ha).
We prove the intermediate claim HaV: a ∈ V.
rewrite the current goal using (identity_function_apply unit_interval a HaI) (from right to left).
An exact proof term for the current goal is (SepE2 unit_interval (λu : set ⇒ apply_fun j u ∈ V) a Ha).
An exact proof term for the current goal is (binintersectI V unit_interval a HaV HaI).
Let a be given.
Assume Ha: a ∈ V ∩ unit_interval.
We will prove a ∈ preimage_of unit_interval j V.
We prove the intermediate claim HaV: a ∈ V.
An exact proof term for the current goal is (binintersectE1 V unit_interval a Ha).
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (binintersectE2 V unit_interval a Ha).
We prove the intermediate claim Hpredef: preimage_of unit_interval j V = {u ∈ unit_interval|apply_fun j u ∈ V}.
Use reflexivity.
rewrite the current goal using Hpredef (from left to right).
Apply (SepI unit_interval (λu : set ⇒ apply_fun j u ∈ V) a HaI) to the current goal.
rewrite the current goal using (identity_function_apply unit_interval a HaI) (from left to right).
An exact proof term for the current goal is HaV.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hut: unit_interval_topology = subspace_topology R R_standard_topology unit_interval.
Use reflexivity.
rewrite the current goal using Hut (from left to right).
An exact proof term for the current goal is (subspace_topologyI R R_standard_topology unit_interval V HV).
∎