Let X, Tx, Y and dY be given.
Assume HTx: topology_on X Tx.
Assume HdY: metric_on Y dY.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ compact_open_topology_C X Tx Y (metric_topology Y dY).
We will prove U ∈ compact_convergence_topology_metric_C X Tx Y dY.
An exact proof term for the current goal is (compact_open_topology_C_sub_compact_convergence_metric_C X Tx Y dY HTx HdY U HU).
Let U be given.
Assume HU: U ∈ compact_convergence_topology_metric_C X Tx Y dY.
We will prove U ∈ compact_open_topology_C X Tx Y (metric_topology Y dY).
An exact proof term for the current goal is (compact_convergence_metric_C_sub_compact_open_topology_C X Tx Y dY HTx HdY U HU).
∎