Let X, dX, Y, dY and f be given.
Assume HdX: metric_on X dX.
Assume HdY: metric_on Y dY.
Assume Hf: function_on f X Y.
We will prove continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f ↔ (∀x0 : set, x0 ∈ X → ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps)).
Apply iffI to the current goal.
Assume Hcont: continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f.
Let x0 be given.
Assume Hx0: x0 ∈ X.
Let eps be given.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim Hepspos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim Hfx0Y: apply_fun f x0 ∈ Y.
An exact proof term for the current goal is (Hf x0 Hx0).
Set V to be the term open_ball Y dY (apply_fun f x0) eps.
We prove the intermediate claim HVtop: V ∈ metric_topology Y dY.
An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun f x0) eps HdY Hfx0Y Hepspos).
Set U to be the term preimage_of X f V.
We prove the intermediate claim HUtop: U ∈ metric_topology X dX.
An exact proof term for the current goal is (continuous_map_preimage X (metric_topology X dX) Y (metric_topology Y dY) f Hcont V HVtop).
Set Bx to be the term famunion X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HUgen: U ∈ generated_topology X Bx.
An exact proof term for the current goal is HUtop.
We prove the intermediate claim Hx0ball: apply_fun f x0 ∈ V.
An exact proof term for the current goal is (center_in_open_ball Y dY (apply_fun f x0) eps HdY Hfx0Y Hepspos).
We prove the intermediate claim Hx0U: x0 ∈ U.
An exact proof term for the current goal is (SepI X (λx : set ⇒ apply_fun f x ∈ V) x0 Hx0 Hx0ball).
We prove the intermediate claim HUlocal: ∀z ∈ U, ∃b ∈ Bx, z ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ Bx, x0 ∈ b ∧ b ⊆ U0) U HUgen).
Apply (HUlocal x0 Hx0U) to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbBx: b ∈ Bx.
An exact proof term for the current goal is (andEL (b ∈ Bx) (x0 ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hbprop: x0 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ Bx) (x0 ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hx0b: x0 ∈ b.
An exact proof term for the current goal is (andEL (x0 ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (x0 ∈ b) (b ⊆ U) Hbprop).
Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}) b HbBx (∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps))) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume HbIn: b ∈ {open_ball X dX c r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X dX c r0) b HbIn (∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps))) to the current goal.
Let r be given.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume Hbeq: b = open_ball X dX c r.
We prove the intermediate claim Hx0inBall: x0 ∈ open_ball X dX c r.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hx0b.
We prove the intermediate claim Hexdelta: ∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ open_ball X dX x0 delta ⊆ open_ball X dX c r.
An exact proof term for the current goal is (open_ball_refine_center X dX c x0 r HdX HcX Hx0 HrR Hrpos Hx0inBall).
Apply Hexdelta to the current goal.
Let delta be given.
Assume Hdelta.
We prove the intermediate claim Hdelta12: delta ∈ R ∧ Rlt 0 delta.
An exact proof term for the current goal is (andEL (delta ∈ R ∧ Rlt 0 delta) (open_ball X dX x0 delta ⊆ open_ball X dX c r) Hdelta).
We prove the intermediate claim HdeltaR: delta ∈ R.
An exact proof term for the current goal is (andEL (delta ∈ R) (Rlt 0 delta) Hdelta12).
We prove the intermediate claim Hdeltapos: Rlt 0 delta.
An exact proof term for the current goal is (andER (delta ∈ R) (Rlt 0 delta) Hdelta12).
We prove the intermediate claim Hballsub: open_ball X dX x0 delta ⊆ open_ball X dX c r.
An exact proof term for the current goal is (andER (delta ∈ R ∧ Rlt 0 delta) (open_ball X dX x0 delta ⊆ open_ball X dX c r) Hdelta).
We prove the intermediate claim HballsubU: open_ball X dX x0 delta ⊆ U.
We prove the intermediate claim Hsubb: open_ball X dX x0 delta ⊆ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is Hballsub.
An exact proof term for the current goal is (Subq_tra (open_ball X dX x0 delta) b U Hsubb HbsubU).
We use delta to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HdeltaR.
An exact proof term for the current goal is Hdeltapos.
Let x be given.
Assume HxX: x ∈ X.
Assume Hdx: Rlt (apply_fun dX (x,x0)) delta.
We prove the intermediate claim Hsym: apply_fun dX (x0,x) = apply_fun dX (x,x0).
An exact proof term for the current goal is (metric_on_symmetric X dX x0 x HdX Hx0 HxX).
We prove the intermediate claim Hdx': Rlt (apply_fun dX (x0,x)) delta.
rewrite the current goal using Hsym (from left to right).
An exact proof term for the current goal is Hdx.
We prove the intermediate claim HxinBall: x ∈ open_ball X dX x0 delta.
An exact proof term for the current goal is (open_ballI X dX x0 delta x HxX Hdx').
We prove the intermediate claim HxinU: x ∈ U.
An exact proof term for the current goal is (HballsubU x HxinBall).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxinU).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hf x HxX).
We prove the intermediate claim HsymY: apply_fun dY (apply_fun f x,apply_fun f x0) = apply_fun dY (apply_fun f x0,apply_fun f x).
An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun f x) (apply_fun f x0) HdY HfxY Hfx0Y).
rewrite the current goal using HsymY (from left to right).
An exact proof term for the current goal is (open_ballE2 Y dY (apply_fun f x0) eps (apply_fun f x) HfxV).
Assume Hed: ∀x0 : set, x0 ∈ X → ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps).
Set Bx to be the term famunion X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}).
Set By to be the term famunion Y (λy0 : set ⇒ {open_ball Y dY y0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HTx: topology_on X (metric_topology X dX).
An exact proof term for the current goal is (metric_topology_is_topology X dX HdX).
We prove the intermediate claim HTy: topology_on Y (metric_topology Y dY).
An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).
We will prove continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f.
We will prove ((topology_on X (metric_topology X dX) ∧ topology_on Y (metric_topology Y dY)) ∧ function_on f X Y) ∧ (∀V : set, V ∈ metric_topology Y dY → preimage_of X f V ∈ metric_topology X dX).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HTy.
An exact proof term for the current goal is Hf.
Let V be given.
Assume HV: V ∈ metric_topology Y dY.
We will prove preimage_of X f V ∈ metric_topology X dX.
Set U to be the term preimage_of X f V.
We will prove U ∈ generated_topology X Bx.
We prove the intermediate claim HVgen: V ∈ generated_topology Y By.
An exact proof term for the current goal is HV.
We prove the intermediate claim HVinPow: V ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λV0 : set ⇒ ∀y0 ∈ V0, ∃b ∈ By, y0 ∈ b ∧ b ⊆ V0) V HVgen).
We prove the intermediate claim HVsubY: V ⊆ Y.
An exact proof term for the current goal is (PowerE Y V HVinPow).
We prove the intermediate claim HVlocal: ∀y0 ∈ V, ∃b ∈ By, y0 ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λV0 : set ⇒ ∀y0 ∈ V0, ∃b ∈ By, y0 ∈ b ∧ b ⊆ V0) V HVgen).
We prove the intermediate claim HUsubX: U ⊆ X.
Let x0 be given.
Assume Hx0U: x0 ∈ U.
An exact proof term for the current goal is (SepE1 X (λx : set ⇒ apply_fun f x ∈ V) x0 Hx0U).
We prove the intermediate claim HUinPow: U ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X U HUsubX).
We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ Bx, x0 ∈ b ∧ b ⊆ U.
Let x0 be given.
Assume Hx0U: x0 ∈ U.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λx : set ⇒ apply_fun f x ∈ V) x0 Hx0U).
We prove the intermediate claim Hfx0V: apply_fun f x0 ∈ V.
An exact proof term for the current goal is (SepE2 X (λx : set ⇒ apply_fun f x ∈ V) x0 Hx0U).
We prove the intermediate claim Hfx0Y: apply_fun f x0 ∈ Y.
An exact proof term for the current goal is (HVsubY (apply_fun f x0) Hfx0V).
Apply (HVlocal (apply_fun f x0) Hfx0V) to the current goal.
Let bY be given.
Assume HbYpair.
We prove the intermediate claim HbYBy: bY ∈ By.
An exact proof term for the current goal is (andEL (bY ∈ By) (apply_fun f x0 ∈ bY ∧ bY ⊆ V) HbYpair).
We prove the intermediate claim HbYprop: apply_fun f x0 ∈ bY ∧ bY ⊆ V.
An exact proof term for the current goal is (andER (bY ∈ By) (apply_fun f x0 ∈ bY ∧ bY ⊆ V) HbYpair).
We prove the intermediate claim Hfx0bY: apply_fun f x0 ∈ bY.
An exact proof term for the current goal is (andEL (apply_fun f x0 ∈ bY) (bY ⊆ V) HbYprop).
We prove the intermediate claim HbYsubV: bY ⊆ V.
An exact proof term for the current goal is (andER (apply_fun f x0 ∈ bY) (bY ⊆ V) HbYprop).
Apply (famunionE_impred Y (λy0 : set ⇒ {open_ball Y dY y0 r|r ∈ R, Rlt 0 r}) bY HbYBy (∃b ∈ Bx, x0 ∈ b ∧ b ⊆ U)) to the current goal.
Let c be given.
Assume HcY: c ∈ Y.
Assume HbYIn: bY ∈ {open_ball Y dY c r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball Y dY c r0) bY HbYIn (∃b ∈ Bx, x0 ∈ b ∧ b ⊆ U)) to the current goal.
Let r be given.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume HbYeq: bY = open_ball Y dY c r.
We prove the intermediate claim Hfx0inBall: apply_fun f x0 ∈ open_ball Y dY c r.
rewrite the current goal using HbYeq (from right to left).
An exact proof term for the current goal is Hfx0bY.
We prove the intermediate claim Hexeps0: ∃eps0 : set, eps0 ∈ R ∧ Rlt 0 eps0 ∧ open_ball Y dY (apply_fun f x0) eps0 ⊆ open_ball Y dY c r.
An exact proof term for the current goal is (open_ball_refine_center Y dY c (apply_fun f x0) r HdY HcY Hfx0Y HrR Hrpos Hfx0inBall).
Apply Hexeps0 to the current goal.
Let eps0 be given.
Assume Heps0.
We prove the intermediate claim Heps0_12: eps0 ∈ R ∧ Rlt 0 eps0.
An exact proof term for the current goal is (andEL (eps0 ∈ R ∧ Rlt 0 eps0) (open_ball Y dY (apply_fun f x0) eps0 ⊆ open_ball Y dY c r) Heps0).
We prove the intermediate claim Heps0R: eps0 ∈ R.
An exact proof term for the current goal is (andEL (eps0 ∈ R) (Rlt 0 eps0) Heps0_12).
We prove the intermediate claim Heps0pos: Rlt 0 eps0.
An exact proof term for the current goal is (andER (eps0 ∈ R) (Rlt 0 eps0) Heps0_12).
We prove the intermediate claim HballYsub: open_ball Y dY (apply_fun f x0) eps0 ⊆ open_ball Y dY c r.
An exact proof term for the current goal is (andER (eps0 ∈ R ∧ Rlt 0 eps0) (open_ball Y dY (apply_fun f x0) eps0 ⊆ open_ball Y dY c r) Heps0).
We prove the intermediate claim HballYsubV: open_ball Y dY (apply_fun f x0) eps0 ⊆ V.
We prove the intermediate claim HsubbY: open_ball Y dY (apply_fun f x0) eps0 ⊆ bY.
rewrite the current goal using HbYeq (from left to right).
An exact proof term for the current goal is HballYsub.
An exact proof term for the current goal is (Subq_tra (open_ball Y dY (apply_fun f x0) eps0) bY V HsubbY HbYsubV).
Apply (Hed x0 Hx0X eps0 (andI (eps0 ∈ R) (Rlt 0 eps0) Heps0R Heps0pos)) to the current goal.
Let delta be given.
Assume Hdelta.
We prove the intermediate claim Hdelta12: delta ∈ R ∧ Rlt 0 delta.
An exact proof term for the current goal is (andEL (delta ∈ R ∧ Rlt 0 delta) (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps0) Hdelta).
We prove the intermediate claim HdeltaR: delta ∈ R.
An exact proof term for the current goal is (andEL (delta ∈ R) (Rlt 0 delta) Hdelta12).
We prove the intermediate claim Hdeltapos: Rlt 0 delta.
An exact proof term for the current goal is (andER (delta ∈ R) (Rlt 0 delta) Hdelta12).
We prove the intermediate claim HdeltaImp: ∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps0.
An exact proof term for the current goal is (andER (delta ∈ R ∧ Rlt 0 delta) (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps0) Hdelta).
We use (open_ball X dX x0 delta) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HballIn: open_ball X dX x0 delta ∈ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}.
An exact proof term for the current goal is (ReplSepI R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X dX x0 r0) delta HdeltaR Hdeltapos).
An exact proof term for the current goal is (famunionI X (λx1 : set ⇒ {open_ball X dX x1 r|r ∈ R, Rlt 0 r}) x0 (open_ball X dX x0 delta) Hx0X HballIn).
Apply andI to the current goal.
An exact proof term for the current goal is (center_in_open_ball X dX x0 delta HdX Hx0X Hdeltapos).
Let x be given.
Assume Hxin: x ∈ open_ball X dX x0 delta.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (open_ballE1 X dX x0 delta x Hxin).
We prove the intermediate claim HsymX: apply_fun dX (x,x0) = apply_fun dX (x0,x).
An exact proof term for the current goal is (metric_on_symmetric X dX x x0 HdX HxX Hx0X).
We prove the intermediate claim Hdx0x: Rlt (apply_fun dX (x0,x)) delta.
An exact proof term for the current goal is (open_ballE2 X dX x0 delta x Hxin).
We prove the intermediate claim Hdx: Rlt (apply_fun dX (x,x0)) delta.
rewrite the current goal using HsymX (from left to right).
An exact proof term for the current goal is Hdx0x.
We prove the intermediate claim HfyY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hf x HxX).
We prove the intermediate claim Hdy: Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps0.
An exact proof term for the current goal is (HdeltaImp x HxX Hdx).
We prove the intermediate claim HsymY: apply_fun dY (apply_fun f x0,apply_fun f x) = apply_fun dY (apply_fun f x,apply_fun f x0).
An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun f x0) (apply_fun f x) HdY Hfx0Y HfyY).
We prove the intermediate claim Hdy': Rlt (apply_fun dY (apply_fun f x0,apply_fun f x)) eps0.
rewrite the current goal using HsymY (from left to right).
An exact proof term for the current goal is Hdy.
We prove the intermediate claim HfxBall: apply_fun f x ∈ open_ball Y dY (apply_fun f x0) eps0.
An exact proof term for the current goal is (open_ballI Y dY (apply_fun f x0) eps0 (apply_fun f x) HfyY Hdy').
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (HballYsubV (apply_fun f x) HfxBall).
An exact proof term for the current goal is (SepI X (λx1 : set ⇒ apply_fun f x1 ∈ V) x HxX HfxV).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ Bx, x0 ∈ b ∧ b ⊆ U0) U HUinPow HUprop).
∎