(def-language language-for-ms-subspace
    (embedded-languages metric-spaces-language)
    (sorts (aa pp)))
            

(def-theory ms-subspace 
    (component-theories metric-spaces)
    (language language-for-ms-subspace))

(def-theorem () 
    "forall(x,y,z:aa,dist(x,z)<=dist(y,z)+dist(x,y))" 
    lemma
    (theory ms-subspace)
    (proof
      (
        (apply-macete-with-minor-premises commutative-law-for-addition)
        (apply-macete-with-minor-premises triangle-inequality-for-distance)
        )))

(def-theory-ensemble-instances
    metric-spaces
    force-under-quick-load
    (target-theories ms-subspace ms-subspace)
    (multiples 1 2)
    (theory-interpretation-check using-simplification)
    (sorts (pp aa aa))
    (constants (dist "lambda(x,y:aa, dist(x,y))" "lambda(x,y:aa, dist(x,y))"))
    (special-renamings 
      (ball sub%ball)
      (open%ball sub%open%ball)
      (lipschitz%bound sub%lipschitz%bound)
      (lipschitz%bound%on sub%lipschitz%bound%on)
      (complete sub%complete)
      (cauchy sub%cauchy)
      (lim sub%lim)))

(def-theorem cauchy-extends 
    "forall(s:[zz,aa],cauchy(s) iff sub%cauchy(s))"
    (proof (unfold-defined-constants))
    (usages transportable-macete)
    (theory ms-subspace))

(def-constant subspace%closed 
    "forall(s:[zz,aa], #(lim(s)) implies #(lim(s),aa))"
    (theory ms-subspace))

(def-theorem limit-definedness-extends 
    "forall(s:[zz,aa],subspace%closed implies lim(s) == sub%lim(s))"
    reverse
    (usages transportable-macete)
    (proof
      ((unfold-single-defined-constant (0) subspace%closed)
        insistent-direct-inference-strategy
        (antecedent-inference "with(s:[zz,aa],#(lim(s)) or #(sub%lim(s)));")
        (force-substitution "lim(s)=sub%lim(s)" "sub%lim(s)=lim(s)" (0))
        (cut-with-single-formula "forsome(x:aa, lim(s)=x)")
        (antecedent-inference "with(s:[zz,aa],forsome(x:aa,lim(s)=x));")
        (backchain "with(x:aa,s:[zz,aa],lim(s)=x);")
        (apply-macete-with-minor-premises tr%characterization-of-limit)
        beta-reduce-repeatedly
        (backchain-backwards "with(x:aa,s:[zz,aa],lim(s)=x);")
        (cut-with-single-formula "lim(s)=lim(s)")
        (incorporate-antecedent "with(s:[zz,aa],lim(s)=lim(s));")
        (apply-macete-with-minor-premises characterization-of-limit)
        (instantiate-existential ("lim(s)"))
        simplify
        (apply-macete-with-minor-premises characterization-of-limit)
        (cut-with-single-formula "sub%lim(s)=sub%lim(s)")
        (incorporate-antecedent "with(s:[zz,aa],sub%lim(s)=sub%lim(s));")
        (apply-macete-with-minor-premises tr%characterization-of-limit)
        beta-reduce-repeatedly))
    (theory ms-subspace))

(def-theorem completeness-extends 
    "complete implies subspace%closed iff sub%complete"
    reverse
    (proof
      (
        (unfold-single-defined-constant (0) complete)
        (unfold-single-defined-constant (0) sub%complete)
        (force-substitution "sub%cauchy(s)" "cauchy(s)" (0))
        direct-and-antecedent-inference-strategy
        (force-substitution "sub%lim(s)" "lim(s)" (0))
        (backchain "forall(s:[zz,pp],cauchy(s) implies #(lim(s)));")
        (apply-macete-with-minor-premises limit-definedness-extends)
        (unfold-single-defined-constant (0) subspace%closed)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "forall(s:[zz,aa],cauchy(s) implies #(sub%lim(s)));" ("s"))
        (contrapose "with(s:[zz,aa],not(cauchy(s)));")
        (apply-macete-with-minor-premises convergent-implies-cauchy)
        (cut-with-single-formula "forsome(x:aa, lim(s)=x)")
        (antecedent-inference "with(s:[zz,aa],forsome(x:aa,lim(s)=x));")
        (instantiate-existential ("sub%lim(s)"))
        (apply-macete-with-minor-premises characterization-of-limit)
        (cut-with-single-formula "sub%lim(s)=sub%lim(s)")
        (incorporate-antecedent "with(s:[zz,aa],sub%lim(s)=sub%lim(s));")
        (apply-macete-with-minor-premises tr%characterization-of-limit)
        beta-reduce-repeatedly
        (apply-macete-with-minor-premises cauchy-extends)
        ))
    
    (usages transportable-macete)
    (theory ms-subspace))

(def-constant subspace%dense 
    "forall(x:pp, forsome(s:[zz,aa], lim(s)=x))"
    (theory ms-subspace))