Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Set Fam to be the term {halfopen_interval_left x b|x ∈ open_interval a b}.
We prove the intermediate claim HTlower: topology_on R R_lower_limit_topology.
An exact proof term for the current goal is R_lower_limit_topology_is_topology.
We prove the intermediate claim HFamSub: Fam ⊆ R_lower_limit_topology.
Let U be given.
Assume HU: U ∈ Fam.
We will prove U ∈ R_lower_limit_topology.
Apply (ReplE_impred (open_interval a b) (λx0 : set ⇒ halfopen_interval_left x0 b) U HU (U ∈ R_lower_limit_topology)) to the current goal.
Let x be given.
Assume HxI: x ∈ open_interval a b.
Assume HUeq: U = halfopen_interval_left x b.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x HxI).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x b HxR HbR).
We prove the intermediate claim Heq: open_interval a b = ⋃ Fam.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ open_interval a b.
We will prove y ∈ ⋃ Fam.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) y Hy).
We prove the intermediate claim HyProp: Rlt a y ∧ Rlt y b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) y Hy).
We prove the intermediate claim Hyb: Rlt y b.
An exact proof term for the current goal is (andER (Rlt a y) (Rlt y b) HyProp).
Set U0 to be the term halfopen_interval_left y b.
We prove the intermediate claim HyU0: y ∈ U0.
An exact proof term for the current goal is (halfopen_interval_left_leftmem y b Hyb).
We prove the intermediate claim HU0Fam: U0 ∈ Fam.
An exact proof term for the current goal is (ReplI (open_interval a b) (λx0 : set ⇒ halfopen_interval_left x0 b) y Hy).
An exact proof term for the current goal is (UnionI Fam y U0 HyU0 HU0Fam).
Let y be given.
Assume HyU: y ∈ ⋃ Fam.
We will prove y ∈ open_interval a b.
Apply (UnionE_impred Fam y HyU (y ∈ open_interval a b)) to the current goal.
Let U be given.
Assume HyU0: y ∈ U.
Assume HUFam: U ∈ Fam.
We prove the intermediate claim Hexx: ∃x : set, x ∈ open_interval a b ∧ U = halfopen_interval_left x b.
An exact proof term for the current goal is (ReplE (open_interval a b) (λx0 : set ⇒ halfopen_interval_left x0 b) U HUFam).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxI: x ∈ open_interval a b.
An exact proof term for the current goal is (andEL (x ∈ open_interval a b) (U = halfopen_interval_left x b) Hxpair).
We prove the intermediate claim HUeq: U = halfopen_interval_left x b.
An exact proof term for the current goal is (andER (x ∈ open_interval a b) (U = halfopen_interval_left x b) Hxpair).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x HxI).
We prove the intermediate claim HxProp: Rlt a x ∧ Rlt x b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x HxI).
We prove the intermediate claim Hax: Rlt a x.
An exact proof term for the current goal is (andEL (Rlt a x) (Rlt x b) HxProp).
We prove the intermediate claim HyHx: y ∈ halfopen_interval_left x b.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HyU0.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z b) y HyHx).
We prove the intermediate claim HyProp: ¬ (Rlt y x) ∧ Rlt y b.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z b) y HyHx).
We prove the intermediate claim Hnyx: ¬ (Rlt y x).
An exact proof term for the current goal is (andEL (¬ (Rlt y x)) (Rlt y b) HyProp).
We prove the intermediate claim Hyb: Rlt y b.
An exact proof term for the current goal is (andER (¬ (Rlt y x)) (Rlt y b) HyProp).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Hay: Rlt a y.
Apply (SNoLt_trichotomy_or_impred a y HaS HyS (Rlt a y)) to the current goal.
Assume Halt: a < y.
An exact proof term for the current goal is (RltI a y HaR HyR Halt).
Assume HaEq: a = y.
We prove the intermediate claim Hyx: Rlt y x.
rewrite the current goal using HaEq (from right to left).
An exact proof term for the current goal is Hax.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnyx Hyx).
Assume Hylt: y < a.
We prove the intermediate claim Hya: Rlt y a.
An exact proof term for the current goal is (RltI y a HyR HaR Hylt).
We prove the intermediate claim Hyx: Rlt y x.
An exact proof term for the current goal is (Rlt_tra y a x Hya Hax).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnyx Hyx).
We prove the intermediate claim Hop_def: open_interval a b = {z ∈ R|Rlt a z ∧ Rlt z b}.
Use reflexivity.
rewrite the current goal using Hop_def (from left to right).
Apply (SepI R (λz : set ⇒ Rlt a z ∧ Rlt z b) y HyR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hay.
An exact proof term for the current goal is Hyb.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_union_closed R R_lower_limit_topology Fam HTlower HFamSub).
∎