We will prove closure_of R R_standard_topology K_set = K_set ∪ {0} ∧ closure_of R R_K_topology K_set = K_set ∧ closure_of R R_finite_complement_topology K_set = R ∧ closure_of R R_upper_limit_topology K_set = K_set ∧ closure_of R R_ray_topology K_set = R_nonneg_set.
Apply andI to the current goal.
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 closure_of_K_in_R_standard_topology.
An exact proof term for the current goal is closure_of_K_in_R_K_topology.
We prove the intermediate claim HKinf: infinite K_set.
An exact proof term for the current goal is K_set_infinite.
We prove the intermediate claim HKsub: K_set ⊆ R.
An exact proof term for the current goal is K_set_Subq_R.
We prove the intermediate claim HTdef: R_finite_complement_topology = finite_complement_topology R.
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
An exact proof term for the current goal is (closure_infinite_finite_complement R K_set HKsub HKinf).
An exact proof term for the current goal is closure_of_K_in_R_upper_limit_topology.
An exact proof term for the current goal is closure_of_K_in_R_ray_topology.
∎