We will prove ¬ metrizable R R_lower_limit_topology.
Assume Hmet: metrizable R R_lower_limit_topology.
We will prove False.
We prove the intermediate claim HL: Lindelof_space R R_lower_limit_topology.
We will prove Lindelof_space R R_lower_limit_topology.
We prove the intermediate claim Hline: Sorgenfrey_line = R.
Use reflexivity.
We prove the intermediate claim Htop: Sorgenfrey_topology = R_lower_limit_topology.
Use reflexivity.
rewrite the current goal using Hline (from right to left).
rewrite the current goal using Htop (from right to left).
An exact proof term for the current goal is Sorgenfrey_line_Lindelof.
We prove the intermediate claim Hsc: second_countable_space R R_lower_limit_topology.
An exact proof term for the current goal is (ex30_5b_metrizable_Lindelof_second_countable R R_lower_limit_topology Hmet HL).
We prove the intermediate claim HscS: second_countable_space Sorgenfrey_line Sorgenfrey_topology.
We prove the intermediate claim Hline: Sorgenfrey_line = R.
Use reflexivity.
We prove the intermediate claim Htop: Sorgenfrey_topology = R_lower_limit_topology.
Use reflexivity.
rewrite the current goal using Hline (from left to right).
rewrite the current goal using Htop (from left to right).
An exact proof term for the current goal is Hsc.
An exact proof term for the current goal is (Sorgenfrey_line_not_second_countable HscS).
∎