We will prove first_countable_space Sorgenfrey_line Sorgenfrey_topology ∧ dense_in rational_numbers Sorgenfrey_line Sorgenfrey_topology ∧ Lindelof_space Sorgenfrey_line Sorgenfrey_topology ∧ ¬ second_countable_space Sorgenfrey_line Sorgenfrey_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 Sorgenfrey_line_first_countable.
An exact proof term for the current goal is Sorgenfrey_line_rationals_dense.
An exact proof term for the current goal is Sorgenfrey_line_Lindelof.
An exact proof term for the current goal is Sorgenfrey_line_not_second_countable.
∎