Let a, b and d be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HdR: d ∈ R.
We will prove Sorgenfrey_plane_special_rectangle a b d ∈ Sorgenfrey_plane_topology.
Set U to be the term halfopen_interval_left a b.
Set V to be the term halfopen_interval_left (minus_SNo a) d.
We prove the intermediate claim HTx: topology_on Sorgenfrey_line Sorgenfrey_topology.
An exact proof term for the current goal is R_lower_limit_topology_is_topology.
We prove the intermediate claim HUopen: U ∈ Sorgenfrey_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology a b HaR HbR).
We prove the intermediate claim HmaR: (minus_SNo a) ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
We prove the intermediate claim HVopen: V ∈ Sorgenfrey_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology (minus_SNo a) d HmaR HdR).
We prove the intermediate claim HBasis: basis_on (setprod Sorgenfrey_line Sorgenfrey_line) (product_subbasis Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology).
An exact proof term for the current goal is (product_subbasis_is_basis Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology HTx HTx).
We prove the intermediate claim HrectIn: rectangle_set U V ∈ product_subbasis Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology.
We prove the intermediate claim HVfam: rectangle_set U V ∈ {rectangle_set U V0|V0 ∈ Sorgenfrey_topology}.
An exact proof term for the current goal is (ReplI Sorgenfrey_topology (λV0 : set ⇒ rectangle_set U V0) V HVopen).
An exact proof term for the current goal is (famunionI Sorgenfrey_topology (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Sorgenfrey_topology}) U (rectangle_set U V) HUopen HVfam).
We prove the intermediate claim HdefRect: Sorgenfrey_plane_special_rectangle a b d = rectangle_set U V.
Use reflexivity.
We prove the intermediate claim HdefTop: Sorgenfrey_plane_topology = product_topology Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology.
Use reflexivity.
We prove the intermediate claim HdefProd: product_topology Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology = generated_topology (setprod Sorgenfrey_line Sorgenfrey_line) (product_subbasis Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology).
Use reflexivity.
rewrite the current goal using HdefTop (from left to right).
rewrite the current goal using HdefProd (from left to right).
rewrite the current goal using HdefRect (from left to right).
An exact proof term for the current goal is (generated_topology_contains_basis (setprod Sorgenfrey_line Sorgenfrey_line) (product_subbasis Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology) HBasis (rectangle_set U V) HrectIn).
∎