We will prove (Hausdorff_space R R_standard_topology ∧ T1_space R R_standard_topology) ∧ (Hausdorff_space R R_upper_limit_topology ∧ T1_space R R_upper_limit_topology) ∧ (Hausdorff_space R R_K_topology ∧ T1_space R R_K_topology) ∧ (¬ Hausdorff_space R R_finite_complement_topology ∧ T1_space R R_finite_complement_topology) ∧ (¬ Hausdorff_space R R_ray_topology ∧ ¬ T1_space R R_ray_topology).
Apply andI to the current goal.
Apply andI to the current goal.
We will prove (Hausdorff_space R R_standard_topology ∧ T1_space R R_standard_topology) ∧ (Hausdorff_space R R_upper_limit_topology ∧ T1_space R R_upper_limit_topology) ∧ (Hausdorff_space R R_K_topology ∧ T1_space R R_K_topology).
Apply andI to the current goal.
Apply andI to the current goal.
We will prove Hausdorff_space R R_standard_topology ∧ T1_space R R_standard_topology.
Apply andI to the current goal.
An exact proof term for the current goal is R_standard_topology_Hausdorff.
An exact proof term for the current goal is R_standard_topology_T1.
We will prove Hausdorff_space R R_upper_limit_topology ∧ T1_space R R_upper_limit_topology.
Apply andI to the current goal.
An exact proof term for the current goal is R_upper_limit_topology_Hausdorff.
An exact proof term for the current goal is R_upper_limit_topology_T1.
We will prove Hausdorff_space R R_K_topology ∧ T1_space R R_K_topology.
Apply andI to the current goal.
An exact proof term for the current goal is R_K_topology_Hausdorff.
An exact proof term for the current goal is R_K_topology_T1.
We will prove ¬ Hausdorff_space R R_finite_complement_topology ∧ T1_space R R_finite_complement_topology.
Apply andI to the current goal.
An exact proof term for the current goal is R_finite_complement_not_Hausdorff.
An exact proof term for the current goal is (finite_complement_topology_T1 R).
We will prove ¬ Hausdorff_space R R_ray_topology ∧ ¬ T1_space R R_ray_topology.
Apply andI to the current goal.
An exact proof term for the current goal is ray_topology_not_Hausdorff.
An exact proof term for the current goal is ray_topology_not_T1.
∎