Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Set B to be the term famunion R (λx0 : set ⇒ {open_ball R R_bounded_metric x0 r0|r0 ∈ R, Rlt 0 r0}).
We will prove open_interval a b ∈ generated_topology R B.
We prove the intermediate claim HdefGT: generated_topology R B = {U ∈ 𝒫 R|∀x ∈ U, ∃b0 ∈ B, x ∈ b0 ∧ b0 ⊆ U}.
Use reflexivity.
rewrite the current goal using HdefGT (from left to right).
Apply SepI to the current goal.
Apply PowerI to the current goal.
Let x be given.
Assume Hx: x ∈ open_interval a b.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x Hx).
Let x be given.
Assume Hx: x ∈ open_interval a b.
We will prove ∃b0 ∈ B, x ∈ b0 ∧ b0 ⊆ open_interval a 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 Hx).
We prove the intermediate claim Hxab: 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 Hx).
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) Hxab).
We prove the intermediate claim Hxb: Rlt x b.
An exact proof term for the current goal is (andER (Rlt a x) (Rlt x b) Hxab).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HaxS: a < x.
An exact proof term for the current goal is (RltE_lt a x Hax).
We prove the intermediate claim HxbS: x < b.
An exact proof term for the current goal is (RltE_lt x b Hxb).
Set dx to be the term add_SNo x (minus_SNo a).
Set dy to be the term add_SNo b (minus_SNo x).
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 HmxR: minus_SNo x ∈ R.
An exact proof term for the current goal is (real_minus_SNo x HxR).
We prove the intermediate claim HdxR: dx ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR (minus_SNo a) HmaR).
We prove the intermediate claim HdyR: dy ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo x) HmxR).
We prove the intermediate claim HdxS: SNo dx.
An exact proof term for the current goal is (real_SNo dx HdxR).
We prove the intermediate claim HdyS: SNo dy.
An exact proof term for the current goal is (real_SNo dy HdyR).
We prove the intermediate claim HdxPosS: 0 < dx.
We prove the intermediate claim H0aLt: add_SNo 0 a < x.
rewrite the current goal using (add_SNo_0L a HaS) (from left to right).
An exact proof term for the current goal is HaxS.
An exact proof term for the current goal is (add_SNo_minus_Lt2b x a 0 HxS HaS SNo_0 H0aLt).
We prove the intermediate claim HdyPosS: 0 < dy.
We prove the intermediate claim H0xLt: add_SNo 0 x < b.
rewrite the current goal using (add_SNo_0L x HxS) (from left to right).
An exact proof term for the current goal is HxbS.
An exact proof term for the current goal is (add_SNo_minus_Lt2b b x 0 HbS HxS SNo_0 H0xLt).
We prove the intermediate claim HdxPos: Rlt 0 dx.
An exact proof term for the current goal is (RltI 0 dx real_0 HdxR HdxPosS).
We prove the intermediate claim HdyPos: Rlt 0 dy.
An exact proof term for the current goal is (RltI 0 dy real_0 HdyR HdyPosS).
We prove the intermediate claim Hexr: ∃r3 : set, r3 ∈ R ∧ Rlt 0 r3 ∧ Rlt r3 dx ∧ Rlt r3 dy ∧ Rlt r3 1 ∧ Rlt r3 1.
An exact proof term for the current goal is (exists_eps_lt_four_pos_Euclid dx dy 1 1 HdxR HdyR real_1 real_1 HdxPos HdyPos Rlt_0_1 Rlt_0_1).
Apply Hexr to the current goal.
Let r3 be given.
Assume Hr3: r3 ∈ R ∧ Rlt 0 r3 ∧ Rlt r3 dx ∧ Rlt r3 dy ∧ Rlt r3 1 ∧ Rlt r3 1.
We prove the intermediate claim Hr3_ABCDE: ((((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 dx) ∧ Rlt r3 dy) ∧ Rlt r3 1).
An exact proof term for the current goal is (andEL ((((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 dx) ∧ Rlt r3 dy) ∧ Rlt r3 1) (Rlt r3 1) Hr3).
We prove the intermediate claim Hr3_ABCD: (((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 dx) ∧ Rlt r3 dy).
An exact proof term for the current goal is (andEL (((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 dx) ∧ Rlt r3 dy) (Rlt r3 1) Hr3_ABCDE).
We prove the intermediate claim Hr3_E: Rlt r3 1.
An exact proof term for the current goal is (andER (((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 dx) ∧ Rlt r3 dy) (Rlt r3 1) Hr3_ABCDE).
We prove the intermediate claim Hr3_ABC: ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 dx).
An exact proof term for the current goal is (andEL ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 dx) (Rlt r3 dy) Hr3_ABCD).
We prove the intermediate claim Hr3_D: Rlt r3 dy.
An exact proof term for the current goal is (andER ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 dx) (Rlt r3 dy) Hr3_ABCD).
We prove the intermediate claim Hr3_AB: r3 ∈ R ∧ Rlt 0 r3.
An exact proof term for the current goal is (andEL (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 dx) Hr3_ABC).
We prove the intermediate claim Hr3_C: Rlt r3 dx.
An exact proof term for the current goal is (andER (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 dx) Hr3_ABC).
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (andEL (r3 ∈ R) (Rlt 0 r3) Hr3_AB).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (andER (r3 ∈ R) (Rlt 0 r3) Hr3_AB).
We prove the intermediate claim Hr3ltDx: Rlt r3 dx.
An exact proof term for the current goal is Hr3_C.
We prove the intermediate claim Hr3ltDy: Rlt r3 dy.
An exact proof term for the current goal is Hr3_D.
We prove the intermediate claim Hr3lt1: Rlt r3 1.
An exact proof term for the current goal is Hr3_E.
Set ball to be the term open_ball R R_bounded_metric x r3.
We use ball to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HballIn: ball ∈ {open_ball R R_bounded_metric x rr|rr ∈ R, Rlt 0 rr}.
An exact proof term for the current goal is (ReplSepI R (λrr : set ⇒ Rlt 0 rr) (λrr : set ⇒ open_ball R R_bounded_metric x rr) r3 Hr3R Hr3pos).
An exact proof term for the current goal is (famunionI R (λx0 : set ⇒ {open_ball R R_bounded_metric x0 rr|rr ∈ R, Rlt 0 rr}) x ball HxR HballIn).
Apply andI to the current goal.
An exact proof term for the current goal is (center_in_open_ball R R_bounded_metric x r3 R_bounded_metric_is_metric_on_early HxR Hr3pos).
rewrite the current goal using (open_ball_R_bounded_metric_eq_open_interval_early x r3 HxR Hr3R Hr3pos Hr3lt1) (from left to right).
Let y be given.
Assume HyB: y ∈ open_interval (add_SNo x (minus_SNo r3)) (add_SNo x r3).
We will prove y ∈ open_interval a b.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λy0 : set ⇒ Rlt (add_SNo x (minus_SNo r3)) y0 ∧ Rlt y0 (add_SNo x r3)) y HyB).
We prove the intermediate claim HyConj: Rlt (add_SNo x (minus_SNo r3)) y ∧ Rlt y (add_SNo x r3).
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ Rlt (add_SNo x (minus_SNo r3)) y0 ∧ Rlt y0 (add_SNo x r3)) y HyB).
We prove the intermediate claim HyLeft: Rlt (add_SNo x (minus_SNo r3)) y.
An exact proof term for the current goal is (andEL (Rlt (add_SNo x (minus_SNo r3)) y) (Rlt y (add_SNo x r3)) HyConj).
We prove the intermediate claim HyRight: Rlt y (add_SNo x r3).
An exact proof term for the current goal is (andER (Rlt (add_SNo x (minus_SNo r3)) y) (Rlt y (add_SNo x r3)) HyConj).
We prove the intermediate claim Hxmr3R: add_SNo x (minus_SNo r3) ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR (minus_SNo r3) (real_minus_SNo r3 Hr3R)).
We prove the intermediate claim Hxpr3R: add_SNo x r3 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR r3 Hr3R).
We prove the intermediate claim Haxmr3S: a < add_SNo x (minus_SNo r3).
We prove the intermediate claim Hr3dxS: r3 < dx.
An exact proof term for the current goal is (RltE_lt r3 dx Hr3ltDx).
We prove the intermediate claim Hr3plusA_lt_x: add_SNo r3 a < x.
An exact proof term for the current goal is (add_SNo_minus_Lt2 x a r3 HxS HaS (real_SNo r3 Hr3R) Hr3dxS).
We prove the intermediate claim Ha_plus_r3_lt_x: add_SNo a r3 < x.
rewrite the current goal using (add_SNo_com r3 a (real_SNo r3 Hr3R) HaS) (from right to left).
An exact proof term for the current goal is Hr3plusA_lt_x.
An exact proof term for the current goal is (add_SNo_minus_Lt2b x r3 a HxS (real_SNo r3 Hr3R) HaS Ha_plus_r3_lt_x).
We prove the intermediate claim Hxpr3ltbS: add_SNo x r3 < b.
We prove the intermediate claim Hr3dyS: r3 < dy.
An exact proof term for the current goal is (RltE_lt r3 dy Hr3ltDy).
We prove the intermediate claim Hr3plusX_lt_b: add_SNo r3 x < b.
An exact proof term for the current goal is (add_SNo_minus_Lt2 b x r3 HbS HxS (real_SNo r3 Hr3R) Hr3dyS).
rewrite the current goal using (add_SNo_com r3 x (real_SNo r3 Hr3R) HxS) (from right to left) at position 1.
An exact proof term for the current goal is Hr3plusX_lt_b.
We prove the intermediate claim Haxmr3: Rlt a (add_SNo x (minus_SNo r3)).
An exact proof term for the current goal is (RltI a (add_SNo x (minus_SNo r3)) HaR Hxmr3R Haxmr3S).
We prove the intermediate claim Hxpr3ltb: Rlt (add_SNo x r3) b.
An exact proof term for the current goal is (RltI (add_SNo x r3) b Hxpr3R HbR Hxpr3ltbS).
We prove the intermediate claim Hay: Rlt a y.
An exact proof term for the current goal is (Rlt_tra a (add_SNo x (minus_SNo r3)) y Haxmr3 HyLeft).
We prove the intermediate claim Hyb: Rlt y b.
An exact proof term for the current goal is (Rlt_tra y (add_SNo x r3) b HyRight Hxpr3ltb).
An exact proof term for the current goal is (SepI R (λy0 : set ⇒ Rlt a y0 ∧ Rlt y0 b) y HyR (andI (Rlt a y) (Rlt y b) Hay Hyb)).
∎