Let X, d, B and x be given.
Assume Hm: metric_on X d.
Assume HBcl: closed_in X (metric_topology X d) B.
Assume HxX: x ∈ X.
Assume HxnotB: x ∉ B.
Assume HBne: B ≠ Empty.
Set Tx to be the term metric_topology X d.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
We prove the intermediate claim HBpkg: B ⊆ X ∧ ∃U ∈ Tx, B = X ∖ U.
An exact proof term for the current goal is (closed_in_package X Tx B HBcl).
We prove the intermediate claim HBsub: B ⊆ X.
An exact proof term for the current goal is (andEL (B ⊆ X) (∃U ∈ Tx, B = X ∖ U) HBpkg).
We prove the intermediate claim HexU: ∃U ∈ Tx, B = X ∖ U.
An exact proof term for the current goal is (andER (B ⊆ X) (∃U ∈ Tx, B = X ∖ U) HBpkg).
Apply HexU to the current goal.
Let U be given.
Assume HUconj.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (B = X ∖ U) HUconj).
We prove the intermediate claim HBdef: B = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (B = X ∖ U) HUconj).
We prove the intermediate claim HxU: x ∈ U.
Apply (xm (x ∈ U)) to the current goal.
Assume H: x ∈ U.
An exact proof term for the current goal is H.
Assume Hnot: x ∉ U.
We prove the intermediate claim HxBU: x ∈ X ∖ U.
An exact proof term for the current goal is (setminusI X U x HxX Hnot).
We prove the intermediate claim HxB: x ∈ B.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is HxBU.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB HxB).
We prove the intermediate claim HexBall: ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ U).
Set B0 to be the term famunion X (λc : set ⇒ {open_ball X d c r0|r0 ∈ R, Rlt 0 r0}).
We prove the intermediate claim Hdef: Tx = generated_topology X B0.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology X B0.
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUcond: ∀y ∈ U, ∃b0 ∈ B0, y ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀y0 : set, y0 ∈ U0 → ∃b0 ∈ B0, y0 ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb0: ∃b0 ∈ B0, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUcond x HxU).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B0: b0 ∈ B0.
An exact proof term for the current goal is (andEL (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hxinb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) (andER (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair)).
We prove the intermediate claim Hb0sub: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) (andER (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair)).
Apply (famunionE_impred X (λc : set ⇒ {open_ball X d c r0|r0 ∈ R, Rlt 0 r0}) b0 Hb0B0 (∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume Hb0In: b0 ∈ {open_ball X d c r0|r0 ∈ R, Rlt 0 r0}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c r0) b0 Hb0In (∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hb0eq: b0 = open_ball X d c r0.
We prove the intermediate claim HxinBall: x ∈ open_ball X d c r0.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxinb0.
We prove the intermediate claim HballsubU: open_ball X d c r0 ⊆ U.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hb0sub.
We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d x s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (open_ball_refine_center X d c x r0 Hm HcX HxX Hr0R Hr0pos HxinBall).
Apply Hexs to the current goal.
Let s be given.
Assume Hs.
We prove the intermediate claim Hs12: s ∈ R ∧ Rlt 0 s.
An exact proof term for the current goal is (andEL (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hs).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (andEL (s ∈ R) (Rlt 0 s) Hs12).
We prove the intermediate claim Hspos: Rlt 0 s.
An exact proof term for the current goal is (andER (s ∈ R) (Rlt 0 s) Hs12).
We prove the intermediate claim HsubBall: open_ball X d x s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hs).
We prove the intermediate claim HsubU: open_ball X d x s ⊆ U.
An exact proof term for the current goal is (Subq_tra (open_ball X d x s) (open_ball X d c r0) U HsubBall HballsubU).
We use s to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HsR.
Apply andI to the current goal.
An exact proof term for the current goal is Hspos.
An exact proof term for the current goal is HsubU.
Apply HexBall to the current goal.
Let r be given.
Assume Hrpack.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ U) Hrpack).
We prove the intermediate claim Hrprop: Rlt 0 r ∧ open_ball X d x r ⊆ U.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ U) Hrpack).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andEL (Rlt 0 r) (open_ball X d x r ⊆ U) Hrprop).
We prove the intermediate claim HballsubU: open_ball X d x r ⊆ U.
An exact proof term for the current goal is (andER (Rlt 0 r) (open_ball X d x r ⊆ U) Hrprop).
We prove the intermediate claim HdistR: metric_dist_to_set X d x B ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d x B Hm HxX HBsub HBne).
Set l to be the term metric_sup_neg_dists X d x B.
We prove the intermediate claim Hlub: R_lub (metric_neg_dists X d x B) l.
An exact proof term for the current goal is (metric_sup_neg_dists_is_lub X d x B Hm HxX HBsub HBne).
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (R_lub_in_R (metric_neg_dists X d x B) l Hlub).
We prove the intermediate claim HdistDef: metric_dist_to_set X d x B = minus_SNo l.
Use reflexivity.
Set u to be the term minus_SNo r.
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (real_minus_SNo r HrR).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HuDef: u = minus_SNo r.
Use reflexivity.
We prove the intermediate claim HuS: SNo u.
rewrite the current goal using HuDef (from left to right).
An exact proof term for the current goal is (SNo_minus_SNo r HrS).
We prove the intermediate claim Hub: ∀t : set, t ∈ metric_neg_dists X d x B → t ∈ R → Rle t u.
Let t be given.
Assume HtS: t ∈ metric_neg_dists X d x B.
Assume HtR: t ∈ R.
Apply (ReplE_impred B (λb0 : set ⇒ minus_SNo (apply_fun d (x,b0))) t HtS (Rle t u)) to the current goal.
Let b be given.
Assume HbB: b ∈ B.
Assume Hteq: t = minus_SNo (apply_fun d (x,b)).
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsub b HbB).
We prove the intermediate claim HbnotU: b ∉ U.
We prove the intermediate claim HbBU: b ∈ X ∖ U.
rewrite the current goal using HBdef (from right to left).
An exact proof term for the current goal is HbB.
An exact proof term for the current goal is (setminusE2 X U b HbBU).
We prove the intermediate claim HbnotBall: b ∉ open_ball X d x r.
Assume HbBall: b ∈ open_ball X d x r.
We prove the intermediate claim HbU: b ∈ U.
An exact proof term for the current goal is (HballsubU b HbBall).
An exact proof term for the current goal is (HbnotU HbU).
We prove the intermediate claim Hnlt: ¬ (Rlt (apply_fun d (x,b)) r).
Assume Hlt: Rlt (apply_fun d (x,b)) r.
We prove the intermediate claim HbBall: b ∈ open_ball X d x r.
An exact proof term for the current goal is (SepI X (λy0 : set ⇒ Rlt (apply_fun d (x,y0)) r) b HbX Hlt).
An exact proof term for the current goal is (HbnotBall HbBall).
We prove the intermediate claim HdxbR: apply_fun d (x,b) ∈ R.
We prove the intermediate claim Hfun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hm).
We prove the intermediate claim HxbIn: (x,b) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x b HxX HbX).
An exact proof term for the current goal is (Hfun (x,b) HxbIn).
We prove the intermediate claim Hrle: Rle r (apply_fun d (x,b)).
An exact proof term for the current goal is (RleI r (apply_fun d (x,b)) HrR HdxbR Hnlt).
We prove the intermediate claim Hntlt: ¬ (Rlt u t).
Assume Hltut: Rlt u t.
We prove the intermediate claim Hut: u < t.
An exact proof term for the current goal is (RltE_lt u t Hltut).
We prove the intermediate claim Hut2: u < minus_SNo (apply_fun d (x,b)).
rewrite the current goal using Hteq (from right to left).
An exact proof term for the current goal is Hut.
We prove the intermediate claim HdS: SNo (apply_fun d (x,b)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x,b)) HdxbR).
We prove the intermediate claim Hltneg: apply_fun d (x,b) < minus_SNo u.
An exact proof term for the current goal is (minus_SNo_Lt_contra2 u (apply_fun d (x,b)) HuS HdS Hut2).
We prove the intermediate claim Hinv: minus_SNo u = r.
rewrite the current goal using HuDef (from left to right).
An exact proof term for the current goal is (minus_SNo_minus_SNo_real r HrR).
We prove the intermediate claim Hltneg2: apply_fun d (x,b) < r.
rewrite the current goal using Hinv (from right to left).
An exact proof term for the current goal is Hltneg.
We prove the intermediate claim HltR: Rlt (apply_fun d (x,b)) r.
An exact proof term for the current goal is (RltI (apply_fun d (x,b)) r HdxbR HrR Hltneg2).
An exact proof term for the current goal is (Hnlt HltR).
Apply (RleI t u HtR HuR) to the current goal.
Assume Hltut: Rlt u t.
An exact proof term for the current goal is (Hntlt Hltut).
We prove the intermediate claim Hmin: ∀v : set, v ∈ R → (∀t : set, t ∈ metric_neg_dists X d x B → t ∈ R → Rle t v) → Rle l v.
An exact proof term for the current goal is (andER (l ∈ R ∧ ∀t : set, t ∈ metric_neg_dists X d x B → t ∈ R → Rle t l) (∀v : set, v ∈ R → (∀t : set, t ∈ metric_neg_dists X d x B → t ∈ R → Rle t v) → Rle l v) Hlub).
We prove the intermediate claim Hle_l_u: Rle l u.
An exact proof term for the current goal is (Hmin u HuR Hub).
We prove the intermediate claim Hnlt_u_l: ¬ (Rlt u l).
An exact proof term for the current goal is (RleE_nlt l u Hle_l_u).
We prove the intermediate claim Hle_r_dist: Rle r (metric_dist_to_set X d x B).
Apply (RleI r (metric_dist_to_set X d x B) HrR HdistR) to the current goal.
Assume Hlt: Rlt (metric_dist_to_set X d x B) r.
We prove the intermediate claim Hlt2: Rlt (minus_SNo l) r.
rewrite the current goal using HdistDef (from right to left).
An exact proof term for the current goal is Hlt.
We prove the intermediate claim HltS: minus_SNo l < r.
An exact proof term for the current goal is (RltE_lt (minus_SNo l) r Hlt2).
We prove the intermediate claim HlS: SNo l.
An exact proof term for the current goal is (real_SNo l HlR).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim Hneg: minus_SNo r < l.
An exact proof term for the current goal is (minus_SNo_Lt_contra1 l r HlS HrS HltS).
We prove the intermediate claim HnegR: Rlt u l.
An exact proof term for the current goal is (RltI u l HuR HlR Hneg).
An exact proof term for the current goal is (Hnlt_u_l HnegR).
rewrite the current goal using HdistDef (from left to right).
An exact proof term for the current goal is (Rlt_Rle_tra 0 r (minus_SNo l) Hrpos Hle_r_dist).
∎