We will prove second_countable_space R R_standard_topology.
We will prove topology_on R R_standard_topology ∧ ∃B : set, basis_on R B ∧ countable_set B ∧ basis_generates R B R_standard_topology.
Apply andI to the current goal.
An exact proof term for the current goal is R_standard_topology_is_topology.
We use rational_open_intervals_basis to witness the existential quantifier.
We will prove basis_on R rational_open_intervals_basis ∧ countable_set rational_open_intervals_basis ∧ basis_generates R rational_open_intervals_basis R_standard_topology.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HBgenerates: basis_on R rational_open_intervals_basis ∧ generated_topology R rational_open_intervals_basis = R_standard_topology.
An exact proof term for the current goal is ex13_8a_rational_intervals_basis_standard.
An exact proof term for the current goal is (andEL (basis_on R rational_open_intervals_basis) (generated_topology R rational_open_intervals_basis = R_standard_topology) HBgenerates).
An exact proof term for the current goal is rational_open_intervals_basis_countable.
We will prove basis_generates R rational_open_intervals_basis R_standard_topology.
An exact proof term for the current goal is ex13_8a_rational_intervals_basis_standard.
∎