We will prove SOmega_topology = subspace_topology Sbar_Omega SbarOmega_topology S_Omega.
We prove the intermediate claim HinhEq: order_topology_inherited Sbar_Omega S_Omega = order_topology S_Omega.
We prove the intermediate claim HdefInh: order_topology_inherited Sbar_Omega S_Omega = generated_topology S_Omega (order_topology_basis_inherited Sbar_Omega S_Omega).
Use reflexivity.
We prove the intermediate claim HdefOrd: order_topology S_Omega = generated_topology S_Omega (order_topology_basis S_Omega).
Use reflexivity.
rewrite the current goal using HdefInh (from left to right).
rewrite the current goal using HdefOrd (from left to right).
rewrite the current goal using (SOmega_order_topology_basis_inherited_eq) (from left to right).
Use reflexivity.
rewrite the current goal using HinhEq (from right to left).
We prove the intermediate claim Hso: simply_ordered_set Sbar_Omega.
An exact proof term for the current goal is simply_ordered_set_Sbar_Omega.
We prove the intermediate claim Hconv: convex_in Sbar_Omega S_Omega.
An exact proof term for the current goal is convex_in_Sbar_Omega_S_Omega.
An exact proof term for the current goal is (convex_subspace_order_topology Sbar_Omega S_Omega Hso Hconv).
∎