Loading theory "HOL-Library.Function_Algebras" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Bump_Function" via "Smooth_Manifolds.Smooth" via "Smooth_Manifolds.Analysis_More")
Loading theory "HOL-Library.Quotient_Syntax" (required by "Smooth_Manifolds.Projective_Space" via "HOL-Library.Quotient_Set")
Loading theory "HOL-Types_To_Sets.Prerequisites" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Bump_Function" via "Smooth_Manifolds.Smooth" via "Smooth_Manifolds.Analysis_More" via "HOL-Types_To_Sets.Linear_Algebra_On")
Loading theory "HOL-Types_To_Sets.Types_To_Sets" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Bump_Function" via "Smooth_Manifolds.Smooth" via "Smooth_Manifolds.Analysis_More" via "HOL-Types_To_Sets.Linear_Algebra_On")
### theory "HOL-Library.Quotient_Syntax"
### 0.021s elapsed time, 0.104s cpu time, 0.000s GC time
Loading theory "HOL-Library.Quotient_Set" (required by "Smooth_Manifolds.Projective_Space")
instantiation
  fun :: (type, plus) plus
  plus_fun == plus ::
    ('a \<Rightarrow> 'b)
    \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b
locale local_typedef
  fixes S :: "'b set"
    and s :: "'s itself"
  assumes "local_typedef TYPE('s) S"
instantiation
  fun :: (type, zero) zero
  zero_fun == zero_class.zero :: 'a \<Rightarrow> 'b
instantiation
  fun :: (type, times) times
  times_fun == times ::
    ('a \<Rightarrow> 'b)
    \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b
signature LOCAL_TYPEDEF =
  sig
    val cancel_type_definition: thm -> thm
    val cancel_type_definition_attr: attribute
  end
structure Local_Typedef: LOCAL_TYPEDEF
### ML warning (line 74 of "~~/src/HOL/Types_To_Sets/Examples/Prerequisites.thy"):
### Pattern is not exhaustive.
structure More_Simplifier:
  sig
    val asm_full_var_simplify: Proof.context -> thm -> thm
    val var_simplified:
       Context.generic * Token.T list ->
         attribute * (Context.generic * Token.T list)
    val var_simplify_only: Proof.context -> thm list -> thm -> thm
  end
### theory "HOL-Library.Quotient_Set"
### 0.124s elapsed time, 0.520s cpu time, 0.000s GC time
instantiation
  fun :: (type, one) one
  one_fun == one_class.one :: 'a \<Rightarrow> 'b
### theory "HOL-Types_To_Sets.Prerequisites"
### 0.162s elapsed time, 0.692s cpu time, 0.000s GC time
signature UNOVERLOADING =
  sig
    val unoverload: cterm -> thm -> thm
    val unoverload_attr: cterm -> attribute
  end
structure Unoverloading: UNOVERLOADING
### theory "HOL-Library.Function_Algebras"
### 0.265s elapsed time, 1.096s cpu time, 0.000s GC time
signature INTERNALIZE_SORT =
  sig
    val internalize_sort: ctyp -> thm -> typ * thm
    val internalize_sort_attr: typ -> attribute
  end
structure Internalize_Sort: INTERNALIZE_SORT
### ML warning (line 41 of "~~/src/HOL/Types_To_Sets/unoverload_type.ML"):
### Matches are not exhaustive.
signature UNOVERLOAD_TYPE =
  sig
    val unoverload_type: Context.generic -> indexname list -> thm -> thm
    val unoverload_type_attr: indexname list -> attribute
  end
structure Unoverload_Type: UNOVERLOAD_TYPE
### Metis: Unused theorems: "??.unknown"
### Metis: Unused theorems: "??.unknown"
### Metis: Unused theorems: "??.unknown"
### Metis: Unused theorems: "??.unknown"
### Metis: Unused theorems: "??.unknown"
### Metis: Unused theorems: "??.unknown"
### ML warning (line 36 of "~~/src/HOL/Types_To_Sets/unoverload_def.ML"):
### Pattern is not exhaustive.
### ML warning (line 36 of "~~/src/HOL/Types_To_Sets/unoverload_def.ML"):
### Value identifier (ctxt') has not been referenced.
### ML warning (line 40 of "~~/src/HOL/Types_To_Sets/unoverload_def.ML"):
### Pattern is not exhaustive.
### ML warning (line 66 of "~~/src/HOL/Types_To_Sets/unoverload_def.ML"):
### Pattern is not exhaustive.
structure Unoverload_Def:
  sig
    val unoverload_def: binding option -> thm -> theory -> theory
    val unoverload_def1_cmd:
       binding option * (Facts.ref * Token.src list) -> theory -> theory
  end
### theory "HOL-Types_To_Sets.Types_To_Sets"
### 0.505s elapsed time, 1.868s cpu time, 0.000s GC time
Loading theory "HOL-Types_To_Sets.Group_On_With" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Bump_Function" via "Smooth_Manifolds.Smooth" via "Smooth_Manifolds.Analysis_More" via "HOL-Types_To_Sets.Linear_Algebra_On" via "HOL-Types_To_Sets.Linear_Algebra_On_With")
locale semigroup_add_on_with
  fixes S :: "'a set"
    and pls :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes "semigroup_add_on_with S pls"
locale ab_semigroup_add_on_with
  fixes S :: "'a set"
    and pls :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes "ab_semigroup_add_on_with S pls"
### Metis: Unused theorems: "??.unknown"
locale comm_monoid_add_on_with
  fixes S :: "'a set"
    and pls :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and z :: "'a"
  assumes "comm_monoid_add_on_with S pls z"
locale comm_monoid_add_on_with
  fixes S :: "'a set"
    and pls :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and z :: "'a"
  assumes "comm_monoid_add_on_with S pls z"
locale ab_group_add_on_with
  fixes S :: "'a set"
    and pls :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and z :: "'a"
    and mns :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and um :: "'a \<Rightarrow> 'a"
  assumes "ab_group_add_on_with S pls z mns um"
### Rule already declared as introduction (intro)
### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
### (?A ===> ?B) ?f ?g
locale local_typedef_ab_group_add_on_with
  fixes pls :: "'b \<Rightarrow> 'b \<Rightarrow> 'b"
    and z :: "'b"
    and mns :: "'b \<Rightarrow> 'b \<Rightarrow> 'b"
    and um :: "'b \<Rightarrow> 'b"
    and S :: "'b set"
    and s :: "'s itself"
  assumes "local_typedef_ab_group_add_on_with TYPE('s) pls z mns um S"
### Rule already declared as introduction (intro)
### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
### (?A ===> ?B) ?f ?g
### Rule already declared as introduction (intro)
### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
### (?A ===> ?B) ?f ?g
### Rule already declared as introduction (intro)
### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
### (?A ===> ?B) ?f ?g
### Rule already declared as introduction (intro)
### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
### (?A ===> ?B) ?f ?g
### Rule already declared as introduction (intro)
### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
### (?A ===> ?B) ?f ?g
locale ab_group_add_on_with
  fixes S :: "'a set"
    and pls :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and z :: "'a"
    and mns :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and um :: "'a \<Rightarrow> 'a"
  assumes "ab_group_add_on_with S pls z mns um"
### theory "HOL-Types_To_Sets.Group_On_With"
### 1.299s elapsed time, 4.516s cpu time, 0.208s GC time
Loading theory "HOL-Types_To_Sets.Linear_Algebra_On_With" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Bump_Function" via "Smooth_Manifolds.Smooth" via "Smooth_Manifolds.Analysis_More" via "HOL-Types_To_Sets.Linear_Algebra_On")
locale ab_group_add
  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and zero :: "'a"
    and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and uminus :: "'a \<Rightarrow> 'a"
  assumes "class.ab_group_add plus zero minus uminus"
  notes
    "add.semigroup_axioms" = (\<open>semigroup plus\<close>)
      ["attribute" "<attribute>"]
  notes
    "add.assoc" =
      (\<open>plus (plus ?a ?b) ?c = plus ?a (plus ?b ?c)\<close>)
      ["ac_simps"]
  notes
    "semigroup_add_axioms" = (\<open>class.semigroup_add plus\<close>)
      ["attribute" "<attribute>"]
  notes
    "add_assoc" =
      (\<open>plus (plus ?a ?b) ?c = plus ?a (plus ?b ?c)\<close>)
      ["algebra_simps", "algebra_split_simps", "field_simps",
        "field_split_simps"]
  notes
    "add.abel_semigroup_axioms" = (\<open>abel_semigroup plus\<close>)
      ["attribute" "<attribute>"]
  notes
    "add.commute" = (\<open>plus ?a ?b = plus ?b ?a\<close>) ["ac_simps"]
  notes theorem
    "add.left_commute" =
      (\<open>plus ?b (plus ?a ?c) = plus ?a (plus ?b ?c)\<close>)
      ["ac_simps"]
  notes
    "ab_semigroup_add_axioms" = (\<open>class.ab_semigroup_add plus\<close>)
      ["attribute" "<attribute>"]
  notes
    "add_commute" = (\<open>plus ?a ?b = plus ?b ?a\<close>)
      ["algebra_simps", "algebra_split_simps", "field_simps",
        "field_split_simps"]
  notes
    (\<open>plus ?b (plus ?a ?c) = plus ?a (plus ?b ?c)\<close>)
      ["algebra_simps", "algebra_split_simps", "field_simps",
        "field_split_simps"]
  notes theorem
    "add_ac" = \<open>plus (plus ?a ?b) ?c = plus ?a (plus ?b ?c)\<close>
      \<open>plus ?a ?b = plus ?b ?a\<close>
      \<open>plus ?b (plus ?a ?c) = plus ?a (plus ?b ?c)\<close>
  notes
    "add.monoid_axioms" = (\<open>monoid plus zero\<close>)
      ["attribute" "<attribute>"]
  notes "add.left_neutral" = (\<open>plus zero ?a = ?a\<close>) ["simp"]
  notes "add.right_neutral" = (\<open>plus ?a zero = ?a\<close>) ["simp"]
  notes
    "sum_list.monoid_list_axioms" = (\<open>monoid_list plus zero\<close>)
      ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "sum_list.eq_foldr" =
      (\<open>monoid_add.sum_list plus zero ?xs =
              foldr plus ?xs zero\<close>)
      ["code"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "sum_list.Nil" =
      (\<open>monoid_add.sum_list plus zero [] = zero\<close>) ["simp"]
  notes theorem
    "sum_list.Cons" =
      (\<open>monoid_add.sum_list plus zero (?x # ?xs) =
              plus ?x (monoid_add.sum_list plus zero ?xs)\<close>)
      ["simp"]
  notes theorem
    "sum_list.append" =
      (\<open>monoid_add.sum_list plus zero (?xs @ ?ys) =
              plus (monoid_add.sum_list plus zero ?xs)
               (monoid_add.sum_list plus zero ?ys)\<close>)
      ["simp"]
  notes
    "monoid_add_axioms" = (\<open>class.monoid_add plus zero\<close>)
      ["attribute" "<attribute>"]
  notes "add_0_left" = \<open>plus zero ?a = ?a\<close>
  notes "add_0_right" = \<open>plus ?a zero = ?a\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "sum_list_def" =
      \<open>monoid_add.sum_list plus zero \<equiv>
             monoid_list.F plus zero\<close>
  notes theorem
    "fold_plus_sum_list_rev" =
      \<open>fold plus ?xs =
             plus (monoid_add.sum_list plus zero (rev ?xs))\<close>
  notes theorem
    "size_list_conv_sum_list" =
      \<open>size_list ?f ?xs = sum_list (map ?f ?xs) + length ?xs\<close>
  notes theorem
    "length_concat" =
      \<open>length (concat ?xss) = sum_list (map length ?xss)\<close>
  notes theorem
    "length_product_lists" =
      \<open>length (product_lists ?xss) =
             foldr (*) (map length ?xss) 1\<close>
  notes theorem
    "sum_list_map_filter" =
      \<open>(\<And>x.
                 \<lbrakk>x \<in> set ?xs; \<not> ?P x\<rbrakk>
                 \<Longrightarrow> ?f x = zero) \<Longrightarrow>
             monoid_add.sum_list plus zero (map ?f (filter ?P ?xs)) =
             monoid_add.sum_list plus zero (map ?f ?xs)\<close>
  notes theorem
    "sum_list_triv" =
      \<open>(\<Sum>x\<leftarrow>?xs. ?r) = of_nat (length ?xs) * ?r\<close>
  notes theorem
    "sum_list_0" =
      (\<open>monoid_add.sum_list plus zero (map (\<lambda>x. zero) ?xs) =
              zero\<close>)
      ["simp"]
  notes theorem
    "sum_list_distinct_conv_sum_set" =
      \<open>distinct ?xs \<Longrightarrow>
             sum_list (map ?f ?xs) = sum ?f (set ?xs)\<close>
  notes theorem
    "interv_sum_list_conv_sum_set_nat" =
      \<open>sum_list (map ?f [?m..<?n]) = sum ?f (set [?m..<?n])\<close>
  notes theorem
    "interv_sum_list_conv_sum_set_int" =
      \<open>sum_list (map ?f [?k..?l]) = sum ?f (set [?k..?l])\<close>
  notes theorem
    "sum_list_sum_nth" =
      \<open>sum_list ?xs = sum ((!) ?xs) {0..<length ?xs}\<close>
  notes theorem
    "sum_list_map_filter'" =
      \<open>monoid_add.sum_list plus zero (map ?f (filter ?P ?xs)) =
             monoid_add.sum_list plus zero
              (map (\<lambda>x. if ?P x then ?f x else zero) ?xs)\<close>
  notes
    "add.comm_monoid_axioms" = (\<open>comm_monoid plus zero\<close>)
      ["attribute" "<attribute>"]
  notes "add.comm_neutral" = \<open>plus ?a zero = ?a\<close>
  notes
    "sum.comm_monoid_set_axioms" =
      (\<open>comm_monoid_set plus zero\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "sum.eq_fold" =
      \<open>comm_monoid_add.sum plus zero ?g ?A =
             Finite_Set.fold (plus \<circ> ?g) zero ?A\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "sum.infinite" =
      (\<open>infinite ?A \<Longrightarrow>
              comm_monoid_add.sum plus zero ?g ?A = zero\<close>)
      ["simp"]
  notes theorem
    "sum.empty" =
      (\<open>comm_monoid_add.sum plus zero ?g {} = zero\<close>) ["simp"]
  notes theorem
    "sum.insert" =
      (\<open>\<lbrakk>finite ?A; ?x \<notin> ?A\<rbrakk>
              \<Longrightarrow> comm_monoid_add.sum plus zero ?g
                                 (insert ?x ?A) =
                                plus (?g ?x)
                                 (comm_monoid_add.sum plus zero ?g
                                   ?A)\<close>)
      ["simp"]
  notes theorem
    "sum.remove" =
      \<open>\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?A =
                               plus (?g ?x)
                                (comm_monoid_add.sum plus zero ?g
                                  (?A - {?x}))\<close>
  notes theorem
    "sum.insert_remove" =
      \<open>finite ?A \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g (insert ?x ?A) =
             plus (?g ?x)
              (comm_monoid_add.sum plus zero ?g (?A - {?x}))\<close>
  notes theorem
    "sum.insert_if" =
      \<open>finite ?A \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g (insert ?x ?A) =
             (if ?x \<in> ?A then comm_monoid_add.sum plus zero ?g ?A
              else plus (?g ?x)
                    (comm_monoid_add.sum plus zero ?g ?A))\<close>
  notes theorem
    "sum.neutral" =
      \<open>\<forall>x\<in>?A. ?g x = zero \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g ?A = zero\<close>
  notes theorem
    "sum.neutral_const" =
      (\<open>comm_monoid_add.sum plus zero (\<lambda>_. zero) ?A =
              zero\<close>)
      ["simp"]
  notes theorem
    "sum.union_inter" =
      \<open>\<lbrakk>finite ?A; finite ?B\<rbrakk>
             \<Longrightarrow> plus
                                (comm_monoid_add.sum plus zero ?g
                                  (?A \<union> ?B))
                                (comm_monoid_add.sum plus zero ?g
                                  (?A \<inter> ?B)) =
                               plus (comm_monoid_add.sum plus zero ?g ?A)
                                (comm_monoid_add.sum plus zero ?g
                                  ?B)\<close>
  notes theorem
    "sum.union_inter_neutral" =
      \<open>\<lbrakk>finite ?A; finite ?B;
              \<forall>x\<in>?A \<inter> ?B. ?g x = zero\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g
                                (?A \<union> ?B) =
                               plus (comm_monoid_add.sum plus zero ?g ?A)
                                (comm_monoid_add.sum plus zero ?g
                                  ?B)\<close>
  notes theorem
    "sum.union_disjoint" =
      \<open>\<lbrakk>finite ?A; finite ?B; ?A \<inter> ?B = {}\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g
                                (?A \<union> ?B) =
                               plus (comm_monoid_add.sum plus zero ?g ?A)
                                (comm_monoid_add.sum plus zero ?g
                                  ?B)\<close>
  notes theorem
    "sum.union_diff2" =
      \<open>\<lbrakk>finite ?A; finite ?B\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g
                                (?A \<union> ?B) =
                               plus
                                (plus
                                  (comm_monoid_add.sum plus zero ?g
                                    (?A - ?B))
                                  (comm_monoid_add.sum plus zero ?g
                                    (?B - ?A)))
                                (comm_monoid_add.sum plus zero ?g
                                  (?A \<inter> ?B))\<close>
  notes theorem
    "sum.subset_diff" =
      \<open>\<lbrakk>?B \<subseteq> ?A; finite ?A\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?A =
                               plus
                                (comm_monoid_add.sum plus zero ?g (?A - ?B))
                                (comm_monoid_add.sum plus zero ?g
                                  ?B)\<close>
  notes theorem
    "sum.Int_Diff" =
      \<open>finite ?A \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g ?A =
             plus (comm_monoid_add.sum plus zero ?g (?A \<inter> ?B))
              (comm_monoid_add.sum plus zero ?g (?A - ?B))\<close>
  notes theorem
    "sum.setdiff_irrelevant" =
      \<open>finite ?A \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g (?A - {x. ?g x = zero}) =
             comm_monoid_add.sum plus zero ?g ?A\<close>
  notes theorem
    "sum.not_neutral_contains_not_neutral" =
      (\<open>\<lbrakk>comm_monoid_add.sum plus zero ?g ?A \<noteq> zero;
               \<And>a.
                  \<lbrakk>a \<in> ?A; ?g a \<noteq> zero\<rbrakk>
                  \<Longrightarrow> ?thesis\<rbrakk>
              \<Longrightarrow> ?thesis\<close>)
      ["consumes" - 1, "case_names" "1"]
  notes theorem
    "sum.reindex" =
      \<open>inj_on ?h ?A \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g (?h ` ?A) =
             comm_monoid_add.sum plus zero (?g \<circ> ?h) ?A\<close>
  notes theorem
    "sum.cong" =
      (\<open>\<lbrakk>?A = ?B;
               \<And>x. x \<in> ?B \<Longrightarrow> ?g x = ?h x\<rbrakk>
              \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?A =
                                comm_monoid_add.sum plus zero ?h ?B\<close>)
      ["fundef_cong"]
  notes theorem
    "sum.cong_simp" =
      (\<open>\<lbrakk>?A = ?B;
               \<And>x. x \<in> ?B =simp=> ?g x = ?h x\<rbrakk>
              \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?A =
                                comm_monoid_add.sum plus zero ?h ?B\<close>)
      ["cong"]
  notes theorem
    "sum.reindex_cong" =
      \<open>\<lbrakk>inj_on ?l ?B; ?A = ?l ` ?B;
              \<And>x.
                 x \<in> ?B \<Longrightarrow> ?g (?l x) = ?h x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?A =
                               comm_monoid_add.sum plus zero ?h ?B\<close>
  notes theorem
    "sum.UNION_disjoint" =
      \<open>\<lbrakk>finite ?I; \<forall>i\<in>?I. finite (?A i);
              \<forall>i\<in>?I.
                 \<forall>j\<in>?I.
                    i \<noteq> j \<longrightarrow>
                    ?A i \<inter> ?A j = {}\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g
                                (\<Union> (?A ` ?I)) =
                               comm_monoid_add.sum plus zero
                                (\<lambda>x.
                                    comm_monoid_add.sum plus zero ?g (?A x))
                                ?I\<close>
  notes theorem
    "sum.Union_disjoint" =
      \<open>\<lbrakk>\<forall>A\<in>?C. finite A;
              \<forall>A\<in>?C.
                 \<forall>B\<in>?C.
                    A \<noteq> B \<longrightarrow>
                    A \<inter> B = {}\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g
                                (\<Union> ?C) =
                               (comm_monoid_add.sum plus zero \<circ>
                                comm_monoid_add.sum plus zero)
                                ?g ?C\<close>
  notes theorem
    "sum.distrib" =
      \<open>comm_monoid_add.sum plus zero (\<lambda>x. plus (?g x) (?h x))
              ?A =
             plus (comm_monoid_add.sum plus zero ?g ?A)
              (comm_monoid_add.sum plus zero ?h ?A)\<close>
  notes theorem
    "sum.Sigma" =
      \<open>\<lbrakk>finite ?A; \<forall>x\<in>?A. finite (?B x)\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero
                                (\<lambda>x.
                                    comm_monoid_add.sum plus zero (?g x)
                                     (?B x))
                                ?A =
                               comm_monoid_add.sum plus zero
                                (\<lambda>(x, y). ?g x y)
                                (Sigma ?A ?B)\<close>
  notes theorem
    "sum.related" =
      \<open>\<lbrakk>?R zero zero;
              \<forall>x1 y1 x2 y2.
                 ?R x1 x2 \<and> ?R y1 y2 \<longrightarrow>
                 ?R (plus x1 y1) (plus x2 y2);
              finite ?S; \<forall>x\<in>?S. ?R (?h x) (?g x)\<rbrakk>
             \<Longrightarrow> ?R (comm_monoid_add.sum plus zero ?h ?S)
                                (comm_monoid_add.sum plus zero ?g
                                  ?S)\<close>
  notes theorem
    "sum.mono_neutral_cong_left" =
      \<open>\<lbrakk>finite ?T; ?S \<subseteq> ?T;
              \<forall>i\<in>?T - ?S. ?h i = zero;
              \<And>x. x \<in> ?S \<Longrightarrow> ?g x = ?h x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?S =
                               comm_monoid_add.sum plus zero ?h ?T\<close>
  notes theorem
    "sum.mono_neutral_cong_right" =
      \<open>\<lbrakk>finite ?T; ?S \<subseteq> ?T;
              \<forall>i\<in>?T - ?S. ?g i = zero;
              \<And>x. x \<in> ?S \<Longrightarrow> ?g x = ?h x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?T =
                               comm_monoid_add.sum plus zero ?h ?S\<close>
  notes theorem
    "sum.mono_neutral_left" =
      \<open>\<lbrakk>finite ?T; ?S \<subseteq> ?T;
              \<forall>i\<in>?T - ?S. ?g i = zero\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?S =
                               comm_monoid_add.sum plus zero ?g ?T\<close>
  notes theorem
    "sum.mono_neutral_right" =
      \<open>\<lbrakk>finite ?T; ?S \<subseteq> ?T;
              \<forall>i\<in>?T - ?S. ?g i = zero\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?T =
                               comm_monoid_add.sum plus zero ?g ?S\<close>
  notes theorem
    "sum.mono_neutral_cong" =
      \<open>\<lbrakk>finite ?T; finite ?S;
              \<And>i. i \<in> ?T - ?S \<Longrightarrow> ?h i = zero;
              \<And>i. i \<in> ?S - ?T \<Longrightarrow> ?g i = zero;
              \<And>x.
                 x \<in> ?S \<inter> ?T \<Longrightarrow>
                 ?g x = ?h x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?S =
                               comm_monoid_add.sum plus zero ?h ?T\<close>
  notes theorem
    "sum.reindex_bij_betw" =
      \<open>bij_betw ?h ?S ?T \<Longrightarrow>
             comm_monoid_add.sum plus zero (\<lambda>x. ?g (?h x)) ?S =
             comm_monoid_add.sum plus zero ?g ?T\<close>
  notes theorem
    "sum.reindex_bij_witness" =
      \<open>\<lbrakk>\<And>a. a \<in> ?S \<Longrightarrow> ?i (?j a) = a;
              \<And>a. a \<in> ?S \<Longrightarrow> ?j a \<in> ?T;
              \<And>b. b \<in> ?T \<Longrightarrow> ?j (?i b) = b;
              \<And>b. b \<in> ?T \<Longrightarrow> ?i b \<in> ?S;
              \<And>a.
                 a \<in> ?S \<Longrightarrow> ?h (?j a) = ?g a\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?S =
                               comm_monoid_add.sum plus zero ?h ?T\<close>
  notes theorem
    "sum.reindex_bij_betw_not_neutral" =
      \<open>\<lbrakk>finite ?S'; finite ?T';
              bij_betw ?h (?S - ?S') (?T - ?T');
              \<And>a. a \<in> ?S' \<Longrightarrow> ?g (?h a) = zero;
              \<And>b. b \<in> ?T' \<Longrightarrow> ?g b = zero\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero
                                (\<lambda>x. ?g (?h x)) ?S =
                               comm_monoid_add.sum plus zero ?g ?T\<close>
  notes theorem
    "sum.reindex_nontrivial" =
      \<open>\<lbrakk>finite ?A;
              \<And>x y.
                 \<lbrakk>x \<in> ?A; y \<in> ?A; x \<noteq> y;
                  ?h x = ?h y\<rbrakk>
                 \<Longrightarrow> ?g (?h x) = zero\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g (?h ` ?A) =
                               comm_monoid_add.sum plus zero (?g \<circ> ?h)
                                ?A\<close>
  notes theorem
    "sum.reindex_bij_witness_not_neutral" =
      \<open>\<lbrakk>finite ?S'; finite ?T';
              \<And>a. a \<in> ?S - ?S' \<Longrightarrow> ?i (?j a) = a;
              \<And>a.
                 a \<in> ?S - ?S' \<Longrightarrow> ?j a \<in> ?T - ?T';
              \<And>b. b \<in> ?T - ?T' \<Longrightarrow> ?j (?i b) = b;
              \<And>b.
                 b \<in> ?T - ?T' \<Longrightarrow> ?i b \<in> ?S - ?S';
              \<And>a. a \<in> ?S' \<Longrightarrow> ?g a = zero;
              \<And>b. b \<in> ?T' \<Longrightarrow> ?h b = zero;
              \<And>a.
                 a \<in> ?S \<Longrightarrow> ?h (?j a) = ?g a\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?S =
                               comm_monoid_add.sum plus zero ?h ?T\<close>
  notes theorem
    "sum.delta_remove" =
      \<open>finite ?S \<Longrightarrow>
             comm_monoid_add.sum plus zero
              (\<lambda>k. if k = ?a then ?b k else ?c k) ?S =
             (if ?a \<in> ?S
              then plus (?b ?a)
                    (comm_monoid_add.sum plus zero ?c (?S - {?a}))
              else comm_monoid_add.sum plus zero ?c (?S - {?a}))\<close>
  notes theorem
    "sum.delta" =
      (\<open>finite ?S \<Longrightarrow>
              comm_monoid_add.sum plus zero
               (\<lambda>k. if k = ?a then ?b k else zero) ?S =
              (if ?a \<in> ?S then ?b ?a else zero)\<close>)
      ["simp"]
  notes theorem
    "sum.delta'" =
      (\<open>finite ?S \<Longrightarrow>
              comm_monoid_add.sum plus zero
               (\<lambda>k. if ?a = k then ?b k else zero) ?S =
              (if ?a \<in> ?S then ?b ?a else zero)\<close>)
      ["simp"]
  notes theorem
    "sum.If_cases" =
      \<open>finite ?A \<Longrightarrow>
             comm_monoid_add.sum plus zero
              (\<lambda>x. if ?P x then ?h x else ?g x) ?A =
             plus (comm_monoid_add.sum plus zero ?h (?A \<inter> {x. ?P x}))
              (comm_monoid_add.sum plus zero ?g
                (?A \<inter> - {x. ?P x}))\<close>
  notes theorem
    "sum.cartesian_product" =
      \<open>comm_monoid_add.sum plus zero
              (\<lambda>x. comm_monoid_add.sum plus zero (?g x) ?B) ?A =
             comm_monoid_add.sum plus zero (\<lambda>(x, y). ?g x y)
              (?A \<times> ?B)\<close>
  notes theorem
    "sum.inter_restrict" =
      \<open>finite ?A \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g (?A \<inter> ?B) =
             comm_monoid_add.sum plus zero
              (\<lambda>x. if x \<in> ?B then ?g x else zero) ?A\<close>
  notes theorem
    "sum.inter_filter" =
      \<open>finite ?A \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {x \<in> ?A. ?P x} =
             comm_monoid_add.sum plus zero
              (\<lambda>x. if ?P x then ?g x else zero) ?A\<close>
  notes theorem
    "sum.Union_comp" =
      \<open>\<lbrakk>\<forall>A\<in>?B. finite A;
              \<And>A1 A2 x.
                 \<lbrakk>A1 \<in> ?B; A2 \<in> ?B; A1 \<noteq> A2;
                  x \<in> A1; x \<in> A2\<rbrakk>
                 \<Longrightarrow> ?g x = zero\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g
                                (\<Union> ?B) =
                               (comm_monoid_add.sum plus zero \<circ>
                                comm_monoid_add.sum plus zero)
                                ?g ?B\<close>
  notes theorem
    "sum.swap" =
      \<open>comm_monoid_add.sum plus zero
              (\<lambda>i. comm_monoid_add.sum plus zero (?g i) ?B) ?A =
             comm_monoid_add.sum plus zero
              (\<lambda>j.
                  comm_monoid_add.sum plus zero (\<lambda>i. ?g i j) ?A)
              ?B\<close>
  notes theorem
    "sum.swap_restrict" =
      \<open>\<lbrakk>finite ?A; finite ?B\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero
                                (\<lambda>x.
                                    comm_monoid_add.sum plus zero (?g x)
                                     {y \<in> ?B. ?R x y})
                                ?A =
                               comm_monoid_add.sum plus zero
                                (\<lambda>y.
                                    comm_monoid_add.sum plus zero
                                     (\<lambda>x. ?g x y)
                                     {x \<in> ?A. ?R x y})
                                ?B\<close>
  notes theorem
    "sum.image_gen" =
      \<open>finite ?S \<Longrightarrow>
             comm_monoid_add.sum plus zero ?h ?S =
             comm_monoid_add.sum plus zero
              (\<lambda>y.
                  comm_monoid_add.sum plus zero ?h {x \<in> ?S. ?g x = y})
              (?g ` ?S)\<close>
  notes theorem
    "sum.group" =
      \<open>\<lbrakk>finite ?S; finite ?T; ?g ` ?S \<subseteq> ?T\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero
                                (\<lambda>y.
                                    comm_monoid_add.sum plus zero ?h
                                     {x \<in> ?S. ?g x = y})
                                ?T =
                               comm_monoid_add.sum plus zero ?h ?S\<close>
  notes theorem
    "sum.Plus" =
      \<open>\<lbrakk>finite ?A; finite ?B\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g
                                (?A <+> ?B) =
                               plus
                                (comm_monoid_add.sum plus zero
                                  (?g \<circ> Inl) ?A)
                                (comm_monoid_add.sum plus zero
                                  (?g \<circ> Inr) ?B)\<close>
  notes theorem
    "sum.same_carrier" =
      \<open>\<lbrakk>finite ?C; ?A \<subseteq> ?C; ?B \<subseteq> ?C;
              \<And>a. a \<in> ?C - ?A \<Longrightarrow> ?g a = zero;
              \<And>b.
                 b \<in> ?C - ?B \<Longrightarrow> ?h b = zero\<rbrakk>
             \<Longrightarrow> (comm_monoid_add.sum plus zero ?g ?A =
                                comm_monoid_add.sum plus zero ?h ?B) =
                               (comm_monoid_add.sum plus zero ?g ?C =
                                comm_monoid_add.sum plus zero ?h ?C)\<close>
  notes theorem
    "sum.same_carrierI" =
      \<open>\<lbrakk>finite ?C; ?A \<subseteq> ?C; ?B \<subseteq> ?C;
              \<And>a. a \<in> ?C - ?A \<Longrightarrow> ?g a = zero;
              \<And>b. b \<in> ?C - ?B \<Longrightarrow> ?h b = zero;
              comm_monoid_add.sum plus zero ?g ?C =
              comm_monoid_add.sum plus zero ?h ?C\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g ?A =
                               comm_monoid_add.sum plus zero ?h ?B\<close>
  notes theorem
    "sum.eq_general" =
      \<open>\<lbrakk>\<And>y.
                         y \<in> ?B \<Longrightarrow>
                         \<exists>!x. x \<in> ?A \<and> ?h x = y;
              \<And>x.
                 x \<in> ?A \<Longrightarrow>
                 ?h x \<in> ?B \<and> ?\<gamma> (?h x) = ?\<phi> x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?\<phi> ?A =
                               comm_monoid_add.sum plus zero ?\<gamma>
                                ?B\<close>
  notes theorem
    "sum.eq_general_inverses" =
      \<open>\<lbrakk>\<And>y.
                         y \<in> ?B \<Longrightarrow>
                         ?k y \<in> ?A \<and> ?h (?k y) = y;
              \<And>x.
                 x \<in> ?A \<Longrightarrow>
                 ?h x \<in> ?B \<and>
                 ?k (?h x) = x \<and> ?\<gamma> (?h x) = ?\<phi> x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?\<phi> ?A =
                               comm_monoid_add.sum plus zero ?\<gamma>
                                ?B\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "sum.G_def" =
      \<open>comm_monoid_add.sum' plus zero ?p ?I \<equiv>
             if finite {x \<in> ?I. ?p x \<noteq> zero}
             then comm_monoid_add.sum plus zero ?p
                   {x \<in> ?I. ?p x \<noteq> zero}
             else zero\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "sum.finite_Collect_op" =
      \<open>\<lbrakk>finite {i \<in> ?I. ?x i \<noteq> zero};
              finite {i \<in> ?I. ?y i \<noteq> zero}\<rbrakk>
             \<Longrightarrow> finite
                                {i \<in> ?I.
                                 plus (?x i) (?y i) \<noteq> zero}\<close>
  notes theorem
    "sum.empty'" =
      (\<open>comm_monoid_add.sum' plus zero ?p {} = zero\<close>) ["simp"]
  notes theorem
    "sum.eq_sum" =
      (\<open>finite ?I \<Longrightarrow>
              comm_monoid_add.sum' plus zero ?p ?I =
              comm_monoid_add.sum plus zero ?p ?I\<close>)
      ["simp"]
  notes theorem
    "sum.insert'" =
      (\<open>finite {x \<in> ?I. ?p x \<noteq> zero} \<Longrightarrow>
              comm_monoid_add.sum' plus zero ?p (insert ?i ?I) =
              (if ?i \<in> ?I then comm_monoid_add.sum' plus zero ?p ?I
               else plus (?p ?i)
                     (comm_monoid_add.sum' plus zero ?p ?I))\<close>)
      ["simp"]
  notes theorem
    "sum.distrib_triv'" =
      \<open>finite ?I \<Longrightarrow>
             comm_monoid_add.sum' plus zero (\<lambda>i. plus (?g i) (?h i))
              ?I =
             plus (comm_monoid_add.sum' plus zero ?g ?I)
              (comm_monoid_add.sum' plus zero ?h ?I)\<close>
  notes theorem
    "sum.non_neutral'" =
      \<open>comm_monoid_add.sum' plus zero ?g
              {x \<in> ?I. ?g x \<noteq> zero} =
             comm_monoid_add.sum' plus zero ?g ?I\<close>
  notes theorem
    "sum.distrib'" =
      \<open>\<lbrakk>finite {x \<in> ?I. ?g x \<noteq> zero};
              finite {x \<in> ?I. ?h x \<noteq> zero}\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum' plus zero
                                (\<lambda>i. plus (?g i) (?h i)) ?I =
                               plus (comm_monoid_add.sum' plus zero ?g ?I)
                                (comm_monoid_add.sum' plus zero ?h
                                  ?I)\<close>
  notes theorem
    "sum.cong'" =
      \<open>\<lbrakk>?A = ?B;
              \<And>x. x \<in> ?B \<Longrightarrow> ?g x = ?h x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum' plus zero ?g ?A =
                               comm_monoid_add.sum' plus zero ?h ?B\<close>
  notes theorem
    "sum.mono_neutral_cong_left'" =
      \<open>\<lbrakk>?S \<subseteq> ?T;
              \<And>i. i \<in> ?T - ?S \<Longrightarrow> ?h i = zero;
              \<And>x. x \<in> ?S \<Longrightarrow> ?g x = ?h x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum' plus zero ?g ?S =
                               comm_monoid_add.sum' plus zero ?h ?T\<close>
  notes theorem
    "sum.mono_neutral_cong_right'" =
      \<open>\<lbrakk>?S \<subseteq> ?T;
              \<forall>i\<in>?T - ?S. ?g i = zero;
              \<And>x. x \<in> ?S \<Longrightarrow> ?g x = ?h x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum' plus zero ?g ?T =
                               comm_monoid_add.sum' plus zero ?h ?S\<close>
  notes theorem
    "sum.mono_neutral_left'" =
      \<open>\<lbrakk>?S \<subseteq> ?T;
              \<forall>i\<in>?T - ?S. ?g i = zero\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum' plus zero ?g ?S =
                               comm_monoid_add.sum' plus zero ?g ?T\<close>
  notes theorem
    "sum.mono_neutral_right'" =
      \<open>\<lbrakk>?S \<subseteq> ?T;
              \<forall>i\<in>?T - ?S. ?g i = zero\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum' plus zero ?g ?T =
                               comm_monoid_add.sum' plus zero ?g ?S\<close>
  notes theorem
    "sum.atLeastLessThan_reindex" =
      \<open>bij_betw ?h {?m..<?n} {?h ?m..<?h ?n} \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?h ?m..<?h ?n} =
             comm_monoid_add.sum plus zero (?g \<circ> ?h) {?m..<?n}\<close>
  notes theorem
    "sum.atLeastAtMost_reindex" =
      \<open>bij_betw ?h {?m..?n} {?h ?m..?h ?n} \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?h ?m..?h ?n} =
             comm_monoid_add.sum plus zero (?g \<circ> ?h) {?m..?n}\<close>
  notes theorem
    "sum.atLeastLessThan_shift_bounds" =
      \<open>comm_monoid_add.sum plus zero ?g {?m + ?k..<?n + ?k} =
             comm_monoid_add.sum plus zero (?g \<circ> (+) ?k)
              {?m..<?n}\<close>
  notes theorem
    "sum.atLeastAtMost_shift_bounds" =
      \<open>comm_monoid_add.sum plus zero ?g {?m + ?k..?n + ?k} =
             comm_monoid_add.sum plus zero (?g \<circ> (+) ?k)
              {?m..?n}\<close>
  notes theorem
    "sum.atLeast_Suc_lessThan_Suc_shift" =
      \<open>comm_monoid_add.sum plus zero ?g {Suc ?m..<Suc ?n} =
             comm_monoid_add.sum plus zero (?g \<circ> Suc)
              {?m..<?n}\<close>
  notes theorem
    "sum.atLeast_Suc_atMost_Suc_shift" =
      \<open>comm_monoid_add.sum plus zero ?g {Suc ?m..Suc ?n} =
             comm_monoid_add.sum plus zero (?g \<circ> Suc) {?m..?n}\<close>
  notes theorem
    "sum.atLeast_int_lessThan_int_shift" =
      \<open>comm_monoid_add.sum plus zero ?g {int ?m..<int ?n} =
             comm_monoid_add.sum plus zero (?g \<circ> int)
              {?m..<?n}\<close>
  notes theorem
    "sum.atLeast_int_atMost_int_shift" =
      \<open>comm_monoid_add.sum plus zero ?g {int ?m..int ?n} =
             comm_monoid_add.sum plus zero (?g \<circ> int) {?m..?n}\<close>
  notes theorem
    "sum.atLeast0_lessThan_Suc" =
      \<open>comm_monoid_add.sum plus zero ?g {0..<Suc ?n} =
             plus (comm_monoid_add.sum plus zero ?g {0..<?n})
              (?g ?n)\<close>
  notes theorem
    "sum.atLeast0_atMost_Suc" =
      \<open>comm_monoid_add.sum plus zero ?g {0..Suc ?n} =
             plus (comm_monoid_add.sum plus zero ?g {0..?n})
              (?g (Suc ?n))\<close>
  notes theorem
    "sum.atLeast0_lessThan_Suc_shift" =
      \<open>comm_monoid_add.sum plus zero ?g {0..<Suc ?n} =
             plus (?g 0)
              (comm_monoid_add.sum plus zero (?g \<circ> Suc)
                {0..<?n})\<close>
  notes theorem
    "sum.atLeast0_atMost_Suc_shift" =
      \<open>comm_monoid_add.sum plus zero ?g {0..Suc ?n} =
             plus (?g 0)
              (comm_monoid_add.sum plus zero (?g \<circ> Suc)
                {0..?n})\<close>
  notes theorem
    "sum.atLeast_Suc_lessThan" =
      \<open>?m < ?n \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?m..<?n} =
             plus (?g ?m)
              (comm_monoid_add.sum plus zero ?g {Suc ?m..<?n})\<close>
  notes theorem
    "sum.atLeast_Suc_atMost" =
      \<open>?m \<le> ?n \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?m..?n} =
             plus (?g ?m)
              (comm_monoid_add.sum plus zero ?g {Suc ?m..?n})\<close>
  notes theorem
    "sum.ivl_cong" =
      \<open>\<lbrakk>?a = ?c; ?b = ?d;
              \<And>x.
                 \<lbrakk>?c \<le> x; x < ?d\<rbrakk>
                 \<Longrightarrow> ?g x = ?h x\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero ?g {?a..<?b} =
                               comm_monoid_add.sum plus zero ?h
                                {?c..<?d}\<close>
  notes theorem
    "sum.atLeastLessThan_shift_0" =
      \<open>comm_monoid_add.sum plus zero ?g {?m..<?n} =
             comm_monoid_add.sum plus zero (?g \<circ> (+) ?m)
              {0..<?n - ?m}\<close>
  notes theorem
    "sum.atLeastAtMost_shift_0" =
      \<open>?m \<le> ?n \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?m..?n} =
             comm_monoid_add.sum plus zero (?g \<circ> (+) ?m)
              {0..?n - ?m}\<close>
  notes theorem
    "sum.atLeastLessThan_concat" =
      \<open>\<lbrakk>?m \<le> ?n; ?n \<le> ?p\<rbrakk>
             \<Longrightarrow> plus
                                (comm_monoid_add.sum plus zero ?g {?m..<?n})
                                (comm_monoid_add.sum plus zero ?g
                                  {?n..<?p}) =
                               comm_monoid_add.sum plus zero ?g
                                {?m..<?p}\<close>
  notes theorem
    "sum.atLeastLessThan_rev" =
      \<open>comm_monoid_add.sum plus zero ?g {?n..<?m} =
             comm_monoid_add.sum plus zero
              (\<lambda>i. ?g (?m + ?n - Suc i)) {?n..<?m}\<close>
  notes theorem
    "sum.atLeastAtMost_rev" =
      \<open>comm_monoid_add.sum plus zero ?g {?n..?m} =
             comm_monoid_add.sum plus zero (\<lambda>i. ?g (?m + ?n - i))
              {?n..?m}\<close>
  notes theorem
    "sum.atLeastLessThan_rev_at_least_Suc_atMost" =
      \<open>comm_monoid_add.sum plus zero ?g {?n..<?m} =
             comm_monoid_add.sum plus zero (\<lambda>i. ?g (?m + ?n - i))
              {Suc ?n..?m}\<close>
  notes theorem
    "sum.zero_middle" =
      \<open>\<lbrakk>1 \<le> ?p; ?k \<le> ?p\<rbrakk>
             \<Longrightarrow> comm_monoid_add.sum plus zero
                                (\<lambda>j.
                                    if j < ?k then ?g j
                                    else if j = ?k then zero
   else ?h (j - Suc 0))
                                {..?p} =
                               comm_monoid_add.sum plus zero
                                (\<lambda>j. if j < ?k then ?g j else ?h j)
                                {..?p - Suc 0}\<close>
  notes theorem
    "sum.atMost_Suc" =
      (\<open>comm_monoid_add.sum plus zero ?g {..Suc ?n} =
              plus (comm_monoid_add.sum plus zero ?g {..?n})
               (?g (Suc ?n))\<close>)
      ["simp"]
  notes theorem
    "sum.lessThan_Suc" =
      (\<open>comm_monoid_add.sum plus zero ?g {..<Suc ?n} =
              plus (comm_monoid_add.sum plus zero ?g {..<?n})
               (?g ?n)\<close>)
      ["simp"]
  notes theorem
    "sum.cl_ivl_Suc" =
      (\<open>comm_monoid_add.sum plus zero ?g {?m..Suc ?n} =
              (if Suc ?n < ?m then zero
               else plus (comm_monoid_add.sum plus zero ?g {?m..?n})
                     (?g (Suc ?n)))\<close>)
      ["simp"]
  notes theorem
    "sum.op_ivl_Suc" =
      (\<open>comm_monoid_add.sum plus zero ?g {?m..<Suc ?n} =
              (if ?n < ?m then zero
               else plus (comm_monoid_add.sum plus zero ?g {?m..<?n})
                     (?g ?n))\<close>)
      ["simp"]
  notes theorem
    "sum.head" =
      \<open>?m \<le> ?n \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?m..?n} =
             plus (?g ?m)
              (comm_monoid_add.sum plus zero ?g {?m<..?n})\<close>
  notes theorem
    "sum.ub_add_nat" =
      \<open>?m \<le> ?n + 1 \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?m..?n + ?p} =
             plus (comm_monoid_add.sum plus zero ?g {?m..?n})
              (comm_monoid_add.sum plus zero ?g {?n + 1..?n + ?p})\<close>
  notes theorem
    "sum.nat_group" =
      \<open>comm_monoid_add.sum plus zero
              (\<lambda>m.
                  comm_monoid_add.sum plus zero ?g {m * ?k..<m * ?k + ?k})
              {..<?n} =
             comm_monoid_add.sum plus zero ?g {..<?n * ?k}\<close>
  notes theorem
    "sum.triangle_reindex" =
      \<open>comm_monoid_add.sum plus zero (\<lambda>(i, j). ?g i j)
              {(i, j). i + j < ?n} =
             comm_monoid_add.sum plus zero
              (\<lambda>k.
                  comm_monoid_add.sum plus zero (\<lambda>i. ?g i (k - i))
                   {..k})
              {..<?n}\<close>
  notes theorem
    "sum.triangle_reindex_eq" =
      \<open>comm_monoid_add.sum plus zero (\<lambda>(i, j). ?g i j)
              {(i, j). i + j \<le> ?n} =
             comm_monoid_add.sum plus zero
              (\<lambda>k.
                  comm_monoid_add.sum plus zero (\<lambda>i. ?g i (k - i))
                   {..k})
              {..?n}\<close>
  notes theorem
    "sum.nat_diff_reindex" =
      \<open>comm_monoid_add.sum plus zero (\<lambda>i. ?g (?n - Suc i))
              {..<?n} =
             comm_monoid_add.sum plus zero ?g {..<?n}\<close>
  notes theorem
    "sum.shift_bounds_nat_ivl" =
      \<open>comm_monoid_add.sum plus zero ?g {?m + ?k..<?n + ?k} =
             comm_monoid_add.sum plus zero (\<lambda>i. ?g (i + ?k))
              {?m..<?n}\<close>
  notes theorem
    "sum.shift_bounds_cl_nat_ivl" =
      \<open>comm_monoid_add.sum plus zero ?g {?m + ?k..?n + ?k} =
             comm_monoid_add.sum plus zero (\<lambda>i. ?g (i + ?k))
              {?m..?n}\<close>
  notes theorem
    "sum.shift_bounds_cl_Suc_ivl" =
      \<open>comm_monoid_add.sum plus zero ?g {Suc ?m..Suc ?n} =
             comm_monoid_add.sum plus zero (\<lambda>i. ?g (Suc i))
              {?m..?n}\<close>
  notes theorem
    "sum.shift_bounds_Suc_ivl" =
      \<open>comm_monoid_add.sum plus zero ?g {Suc ?m..<Suc ?n} =
             comm_monoid_add.sum plus zero (\<lambda>i. ?g (Suc i))
              {?m..<?n}\<close>
  notes theorem
    "sum.atMost_Suc_shift" =
      \<open>comm_monoid_add.sum plus zero ?g {..Suc ?n} =
             plus (?g 0)
              (comm_monoid_add.sum plus zero (\<lambda>i. ?g (Suc i))
                {..?n})\<close>
  notes theorem
    "sum.lessThan_Suc_shift" =
      \<open>comm_monoid_add.sum plus zero ?g {..<Suc ?n} =
             plus (?g 0)
              (comm_monoid_add.sum plus zero (\<lambda>i. ?g (Suc i))
                {..<?n})\<close>
  notes theorem
    "sum.atMost_shift" =
      \<open>comm_monoid_add.sum plus zero ?g {..?n} =
             plus (?g 0)
              (comm_monoid_add.sum plus zero (\<lambda>i. ?g (Suc i))
                {..<?n})\<close>
  notes theorem
    "sum.last_plus" =
      \<open>?m \<le> ?n \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?m..?n} =
             plus (?g ?n)
              (comm_monoid_add.sum plus zero ?g {?m..<?n})\<close>
  notes theorem
    "sum.nested_swap" =
      \<open>comm_monoid_add.sum plus zero
              (\<lambda>i. comm_monoid_add.sum plus zero (?a i) {0..<i})
              {0..?n} =
             comm_monoid_add.sum plus zero
              (\<lambda>j.
                  comm_monoid_add.sum plus zero (\<lambda>i. ?a i j)
                   {Suc j..?n})
              {0..<?n}\<close>
  notes theorem
    "sum.nested_swap'" =
      \<open>comm_monoid_add.sum plus zero
              (\<lambda>i. comm_monoid_add.sum plus zero (?a i) {..<i})
              {..?n} =
             comm_monoid_add.sum plus zero
              (\<lambda>j.
                  comm_monoid_add.sum plus zero (\<lambda>i. ?a i j)
                   {Suc j..?n})
              {..<?n}\<close>
  notes theorem
    "sum.atLeast1_atMost_eq" =
      \<open>comm_monoid_add.sum plus zero ?g {Suc 0..?n} =
             comm_monoid_add.sum plus zero (\<lambda>k. ?g (Suc k))
              {..<?n}\<close>
  notes theorem
    "sum.atLeastLessThan_Suc" =
      \<open>?a \<le> ?b \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?a..<Suc ?b} =
             plus (comm_monoid_add.sum plus zero ?g {?a..<?b})
              (?g ?b)\<close>
  notes theorem
    "sum.nat_ivl_Suc'" =
      \<open>?m \<le> Suc ?n \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g {?m..Suc ?n} =
             plus (?g (Suc ?n))
              (comm_monoid_add.sum plus zero ?g {?m..?n})\<close>
  notes theorem
    "sum.in_pairs" =
      \<open>comm_monoid_add.sum plus zero ?g {2 * ?m..Suc (2 * ?n)} =
             comm_monoid_add.sum plus zero
              (\<lambda>i. plus (?g (2 * i)) (?g (Suc (2 * i))))
              {?m..?n}\<close>
  notes theorem
    "sum.in_pairs_0" =
      \<open>comm_monoid_add.sum plus zero ?g {..Suc (2 * ?n)} =
             comm_monoid_add.sum plus zero
              (\<lambda>i. plus (?g (2 * i)) (?g (Suc (2 * i))))
              {..?n}\<close>
  notes theorem
    "sum.F_parametric" =
      (\<open>bi_unique ?A \<Longrightarrow>
              rel_fun (rel_fun ?A (=)) (rel_fun (rel_set ?A) (=))
               (comm_monoid_add.sum plus zero)
               (comm_monoid_add.sum plus zero)\<close>)
      ["transfer_rule"]
  notes
    "sum_list.comm_monoid_list_axioms" =
      (\<open>comm_monoid_list plus zero\<close>)
      ["attribute" "<attribute>"]
  notes theorem
    "sum_list.rev" =
      (\<open>monoid_add.sum_list plus zero (rev ?xs) =
              monoid_add.sum_list plus zero ?xs\<close>)
      ["simp"]
  notes
    "sum.comm_monoid_list_set_axioms" =
      (\<open>comm_monoid_list_set plus zero\<close>)
      ["attribute" "<attribute>"]
  notes theorem
    "sum.distinct_set_conv_list" =
      \<open>distinct ?xs \<Longrightarrow>
             comm_monoid_add.sum plus zero ?g (set ?xs) =
             monoid_add.sum_list plus zero (map ?g ?xs)\<close>
  notes theorem
    "sum.set_conv_list" =
      (\<open>comm_monoid_add.sum plus zero ?g (set ?xs) =
              monoid_add.sum_list plus zero (map ?g (remdups ?xs))\<close>)
      ["code"]
  notes
    "comm_monoid_add_axioms" =
      (\<open>class.comm_monoid_add plus zero\<close>)
      ["attribute" "<attribute>"]
  notes "add_0" = \<open>plus zero ?a = ?a\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "sum_def" =
      \<open>comm_monoid_add.sum plus zero \<equiv>
             comm_monoid_set.F plus zero\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "sum'_def" =
      \<open>comm_monoid_add.sum' plus zero \<equiv>
             comm_monoid_set.G plus zero\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "sum_shift_lb_Suc0_0_upt" =
      \<open>?f 0 = zero \<Longrightarrow>
             comm_monoid_add.sum plus zero ?f {Suc 0..<?k} =
             comm_monoid_add.sum plus zero ?f {0..<?k}\<close>
  notes theorem
    "sum_shift_lb_Suc0_0" =
      \<open>?f 0 = zero \<Longrightarrow>
             comm_monoid_add.sum plus zero ?f {Suc 0..?k} =
             comm_monoid_add.sum plus zero ?f {0..?k}\<close>
  notes theorem
    "sum_list_map_remove1" =
      \<open>?x \<in> set ?xs \<Longrightarrow>
             monoid_add.sum_list plus zero (map ?f ?xs) =
             plus (?f ?x)
              (monoid_add.sum_list plus zero
                (map ?f (remove1 ?x ?xs)))\<close>
  notes theorem
    "distinct_sum_list_conv_Sum" =
      \<open>distinct ?xs \<Longrightarrow>
             monoid_add.sum_list plus zero ?xs =
             comm_monoid_add.sum plus zero (\<lambda>x. x) (set ?xs)\<close>
  notes theorem
    "sum_list_addf" =
      \<open>monoid_add.sum_list plus zero
              (map (\<lambda>x. plus (?f x) (?g x)) ?xs) =
             plus (monoid_add.sum_list plus zero (map ?f ?xs))
              (monoid_add.sum_list plus zero (map ?g ?xs))\<close>
  notes
    "add.group_axioms" = (\<open>group plus zero uminus\<close>)
      ["attribute" "<attribute>"]
  notes "add.group_left_neutral" = \<open>plus zero ?a = ?a\<close>
  notes
    "add.left_inverse" = (\<open>plus (uminus ?a) ?a = zero\<close>)
      ["simp"]
  notes theorem
    "add.left_cancel" = \<open>(plus ?a ?b = plus ?a ?c) = (?b = ?c)\<close>
  notes theorem
    "add.inverse_unique" =
      \<open>plus ?a ?b = zero \<Longrightarrow> uminus ?a = ?b\<close>
  notes theorem
    "add.inverse_neutral" = (\<open>uminus zero = zero\<close>) ["simp"]
  notes theorem
    "add.inverse_inverse" = (\<open>uminus (uminus ?a) = ?a\<close>)
      ["simp"]
  notes theorem
    "add.right_inverse" = (\<open>plus ?a (uminus ?a) = zero\<close>)
      ["simp"]
  notes theorem
    "add.inverse_distrib_swap" =
      \<open>uminus (plus ?a ?b) = plus (uminus ?b) (uminus ?a)\<close>
  notes theorem
    "add.right_cancel" =
      \<open>(plus ?b ?a = plus ?c ?a) = (?b = ?c)\<close>
  notes
    "cancel_semigroup_add_axioms" =
      (\<open>class.cancel_semigroup_add plus\<close>)
      ["attribute" "<attribute>"]
  notes
    "add_left_imp_eq" =
      \<open>plus ?a ?b = plus ?a ?c \<Longrightarrow> ?b = ?c\<close>
  notes
    "add_right_imp_eq" =
      \<open>plus ?b ?a = plus ?c ?a \<Longrightarrow> ?b = ?c\<close>
  notes theorem
    "add_left_cancel" =
      (\<open>(plus ?a ?b = plus ?a ?c) = (?b = ?c)\<close>) ["simp"]
  notes theorem
    "add_right_cancel" =
      (\<open>(plus ?b ?a = plus ?c ?a) = (?b = ?c)\<close>) ["simp"]
  notes theorem "inj_on_add" = (\<open>inj_on (plus ?a) ?A\<close>) ["simp"]
  notes theorem "inj_add_left" = \<open>inj (plus ?a)\<close>
  notes theorem
    "inj_on_add'" = (\<open>inj_on (\<lambda>b. plus b ?a) ?A\<close>)
      ["simp"]
  notes theorem
    "bij_betw_add" =
      (\<open>bij_betw (plus ?a) ?A ?B = (plus ?a ` ?A = ?B)\<close>)
      ["simp"]
  notes
    "group_add_axioms" =
      (\<open>class.group_add minus plus zero uminus\<close>)
      ["attribute" "<attribute>"]
  notes "left_minus" = \<open>plus (uminus ?a) ?a = zero\<close>
  notes
    "add_uminus_conv_diff" =
      (\<open>plus ?a (uminus ?b) = minus ?a ?b\<close>) ["simp"]
  notes theorem
    "diff_conv_add_uminus" =
      \<open>minus ?a ?b = plus ?a (uminus ?b)\<close>
  notes theorem
    "minus_unique" =
      \<open>plus ?a ?b = zero \<Longrightarrow> uminus ?a = ?b\<close>
  notes theorem "minus_zero" = \<open>uminus zero = zero\<close>
  notes theorem "minus_minus" = \<open>uminus (uminus ?a) = ?a\<close>
  notes theorem "right_minus" = \<open>plus ?a (uminus ?a) = zero\<close>
  notes theorem "diff_self" = (\<open>minus ?a ?a = zero\<close>) ["simp"]
  notes theorem
    "minus_add_cancel" = (\<open>plus (uminus ?a) (plus ?a ?b) = ?b\<close>)
      ["simp"]
  notes theorem
    "add_minus_cancel" = (\<open>plus ?a (plus (uminus ?a) ?b) = ?b\<close>)
      ["simp"]
  notes theorem
    "diff_add_cancel" = (\<open>plus (minus ?a ?b) ?b = ?a\<close>) ["simp"]
  notes theorem
    "add_diff_cancel" = (\<open>minus (plus ?a ?b) ?b = ?a\<close>) ["simp"]
  notes theorem
    "minus_add" =
      \<open>uminus (plus ?a ?b) = plus (uminus ?b) (uminus ?a)\<close>
  notes theorem
    "right_minus_eq" = (\<open>(minus ?a ?b = zero) = (?a = ?b)\<close>)
      ["simp"]
  notes theorem
    "eq_iff_diff_eq_0" = \<open>(?a = ?b) = (minus ?a ?b = zero)\<close>
  notes theorem
    "diff_0" = (\<open>minus zero ?a = uminus ?a\<close>) ["simp"]
  notes theorem
    "diff_0_right" = (\<open>minus ?a zero = ?a\<close>) ["simp"]
  notes theorem
    "diff_minus_eq_add" = (\<open>minus ?a (uminus ?b) = plus ?a ?b\<close>)
      ["simp"]
  notes theorem
    "neg_equal_iff_equal" =
      (\<open>(uminus ?a = uminus ?b) = (?a = ?b)\<close>) ["simp"]
  notes theorem
    "neg_equal_0_iff_equal" =
      (\<open>(uminus ?a = zero) = (?a = zero)\<close>) ["simp"]
  notes theorem
    "neg_0_equal_iff_equal" =
      (\<open>(zero = uminus ?a) = (zero = ?a)\<close>) ["simp"]
  notes theorem
    "equation_minus_iff" =
      \<open>(?a = uminus ?b) = (?b = uminus ?a)\<close>
  notes theorem
    "minus_equation_iff" =
      \<open>(uminus ?a = ?b) = (uminus ?b = ?a)\<close>
  notes theorem
    "eq_neg_iff_add_eq_0" =
      \<open>(?a = uminus ?b) = (plus ?a ?b = zero)\<close>
  notes theorem
    "add_eq_0_iff2" = \<open>(plus ?a ?b = zero) = (?a = uminus ?b)\<close>
  notes theorem
    "neg_eq_iff_add_eq_0" =
      \<open>(uminus ?a = ?b) = (plus ?a ?b = zero)\<close>
  notes theorem
    "add_eq_0_iff" = \<open>(plus ?a ?b = zero) = (?b = uminus ?a)\<close>
  notes theorem
    "minus_diff_eq" = (\<open>uminus (minus ?a ?b) = minus ?b ?a\<close>)
      ["simp"]
  notes theorem
    "add_diff_eq" =
      (\<open>plus ?a (minus ?b ?c) = minus (plus ?a ?b) ?c\<close>)
      ["algebra_simps", "algebra_split_simps", "field_simps",
        "field_split_simps"]
  notes theorem
    "diff_add_eq_diff_diff_swap" =
      \<open>minus ?a (plus ?b ?c) = minus (minus ?a ?c) ?b\<close>
  notes theorem
    "diff_eq_eq" = (\<open>(minus ?a ?b = ?c) = (?a = plus ?c ?b)\<close>)
      ["algebra_simps", "algebra_split_simps", "field_simps",
        "field_split_simps"]
  notes theorem
    "eq_diff_eq" = (\<open>(?a = minus ?c ?b) = (plus ?a ?b = ?c)\<close>)
      ["algebra_simps", "algebra_split_simps", "field_simps",
        "field_split_simps"]
  notes theorem
    "diff_diff_eq2" =
      (\<open>minus ?a (minus ?b ?c) = minus (plus ?a ?c) ?b\<close>)
      ["algebra_simps", "algebra_split_simps", "field_simps",
        "field_split_simps"]
  notes theorem
    "diff_eq_diff_eq" =
      \<open>minus ?a ?b = minus ?c ?d \<Longrightarrow>
             (?a = ?b) = (?c = ?d)\<close>
  notes theorem
    "minus_comp_minus" = (\<open>uminus \<circ> uminus = id\<close>)
      ["simp"]
  notes
    "cancel_ab_semigroup_add_axioms" =
      (\<open>class.cancel_ab_semigroup_add plus minus\<close>)
      ["attribute" "<attribute>"]
  notes
    "add_diff_cancel_left'" = (\<open>minus (plus ?a ?b) ?a = ?b\<close>)
      ["simp"]
  notes
    "diff_diff_add" =
      (\<open>minus (minus ?a ?b) ?c = minus ?a (plus ?b ?c)\<close>)
      ["algebra_simps", "algebra_split_simps", "field_simps",
        "field_split_simps"]
  notes theorem
    "add_diff_cancel_right'" = (\<open>minus (plus ?a ?b) ?b = ?a\<close>)
      ["simp"]
  notes theorem
    "add_diff_cancel_left" =
      (\<open>minus (plus ?c ?a) (plus ?c ?b) = minus ?a ?b\<close>)
      ["simp"]
  notes theorem
    "add_diff_cancel_right" =
      (\<open>minus (plus ?a ?c) (plus ?b ?c) = minus ?a ?b\<close>)
      ["simp"]
  notes theorem
    "diff_right_commute" =
      \<open>minus (minus ?a ?c) ?b = minus (minus ?a ?b) ?c\<close>
  notes
    "cancel_comm_monoid_add_axioms" =
      (\<open>class.cancel_comm_monoid_add plus minus zero\<close>)
      ["attribute" "<attribute>"]
  notes theorem "diff_zero" = (\<open>minus ?a zero = ?a\<close>) ["simp"]
  notes theorem "diff_cancel" = (\<open>minus ?a ?a = zero\<close>) ["simp"]
  notes theorem
    "add_implies_diff" =
      \<open>plus ?c ?b = ?a \<Longrightarrow> ?c = minus ?a ?b\<close>
  notes theorem
    "add_cancel_right_right" =
      (\<open>(?a = plus ?a ?b) = (?b = zero)\<close>) ["simp"]
  notes theorem
    "add_cancel_right_left" =
      (\<open>(?a = plus ?b ?a) = (?b = zero)\<close>) ["simp"]
  notes theorem
    "add_cancel_left_right" =
      (\<open>(plus ?a ?b = ?a) = (?b = zero)\<close>) ["simp"]
  notes theorem
    "add_cancel_left_left" =
      (\<open>(plus ?b ?a = ?a) = (?b = zero)\<close>) ["simp"]
  notes
    "ab_group_add_axioms" =
      (\<open>class.ab_group_add plus zero minus uminus\<close>)
      ["attribute" "<attribute>"]
  notes "ab_left_minus" = \<open>plus (uminus ?a) ?a = zero\<close>
  notes
    "ab_diff_conv_add_uminus" =
      \<open>minus ?a ?b = plus ?a (uminus ?b)\<close>
  notes theorem
    "uminus_add_conv_diff" =
      (\<open>plus (uminus ?a) ?b = minus ?b ?a\<close>) ["simp"]
  notes theorem
    "minus_add_distrib" =
      (\<open>uminus (plus ?a ?b) = plus (uminus ?a) (uminus ?b)\<close>)
      ["simp"]
  notes theorem
    "diff_add_eq" =
      (\<open>plus (minus ?a ?b) ?c = minus (plus ?a ?c) ?b\<close>)
      ["algebra_simps", "algebra_split_simps", "field_simps",
        "field_split_simps"]
  notes theorem "surj_plus" = (\<open>surj (plus ?a)\<close>) ["simp"]
  notes theorem
    "inj_diff_right" = (\<open>inj (\<lambda>b. minus b ?a)\<close>)
      ["simp"]
  notes theorem
    "surj_diff_right" = (\<open>surj (\<lambda>x. minus x ?a)\<close>)
      ["simp"]
  notes theorem
    "translation_Compl" = \<open>plus ?a ` (- ?t) = - plus ?a ` ?t\<close>
  notes theorem
    "translation_subtract_Compl" =
      \<open>(\<lambda>x. minus x ?a) ` (- ?t) =
             - (\<lambda>x. minus x ?a) ` ?t\<close>
  notes theorem
    "translation_diff" =
      \<open>plus ?a ` (?s - ?t) = plus ?a ` ?s - plus ?a ` ?t\<close>
  notes theorem
    "translation_subtract_diff" =
      \<open>(\<lambda>x. minus x ?a) ` (?s - ?t) =
             (\<lambda>x. minus x ?a) ` ?s -
             (\<lambda>x. minus x ?a) ` ?t\<close>
  notes theorem
    "translation_Int" =
      \<open>plus ?a ` (?s \<inter> ?t) =
             plus ?a ` ?s \<inter> plus ?a ` ?t\<close>
  notes theorem
    "translation_subtract_Int" =
      \<open>(\<lambda>x. minus x ?a) ` (?s \<inter> ?t) =
             (\<lambda>x. minus x ?a) ` ?s \<inter>
             (\<lambda>x. minus x ?a) ` ?t\<close>
  notes theorem
    "uminus_sum_list_map" =
      \<open>uminus (monoid_add.sum_list plus zero (map ?f ?xs)) =
             monoid_add.sum_list plus zero
              (map (uminus \<circ> ?f) ?xs)\<close>
  notes theorem
    "sum_list_subtractf" =
      \<open>monoid_add.sum_list plus zero
              (map (\<lambda>x. minus (?f x) (?g x)) ?xs) =
             minus (monoid_add.sum_list plus zero (map ?f ?xs))
              (monoid_add.sum_list plus zero (map ?g ?xs))\<close>
locale module
  fixes
    scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*s\<close> 75)
  assumes "module (*s)"
locale vector_space
  fixes
    scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*s\<close> 75)
  assumes "vector_space (*s)"
Enter MATCH
\<lambda>a b c d e f g h i j. i \<equiv>\<^sup>?
\<lambda>a b c d e f. ?Rha42
\<lambda>a b c d. rel_set C \<equiv>\<^sup>? \<lambda>a b c d. ?Rg17
\<lambda>a b. rel_set A \<equiv>\<^sup>? \<lambda>a b. ?Rf17
?x' \<equiv>\<^sup>?
\<lambda>S S' pls mns um zero scl pls' mns' um' zero' scl'.
   ?a17 (?aa17 S pls mns um zero scl) (?ab17 S' pls' mns' um' zero' scl')
Enter MATCH
\<lambda>a b c d. rel_set C \<equiv>\<^sup>? \<lambda>a b c d. ?Rg17
\<lambda>a b. rel_set A \<equiv>\<^sup>? \<lambda>a b. ?Rf17
?x' \<equiv>\<^sup>?
\<lambda>S S' pls mns um zero scl pls' mns' um' zero' scl'.
   ?a17 (?aa17 S pls mns um zero scl) (?ab17 S' pls' mns' um' zero' scl')
Enter MATCH
\<lambda>a b. rel_set A \<equiv>\<^sup>? \<lambda>a b. ?Rf17
?x' \<equiv>\<^sup>?
\<lambda>S S' pls mns um zero scl pls' mns' um' zero' scl'.
   ?a17 (?aa17 S pls mns um zero scl) (?ab17 S' pls' mns' um' zero' scl')
### theory "HOL-Types_To_Sets.Linear_Algebra_On_With"
### 1.167s elapsed time, 2.888s cpu time, 0.000s GC time
Loading theory "HOL-Types_To_Sets.Linear_Algebra_On" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Bump_Function" via "Smooth_Manifolds.Smooth" via "Smooth_Manifolds.Analysis_More")
Enter MATCH
\<lambda>a b c d e f g h i j. i \<equiv>\<^sup>?
\<lambda>a b c d e f. ?Rha45
\<lambda>a b c d e f g h i j. j \<equiv>\<^sup>? \<lambda>a b c d e f. ?Rh44
\<lambda>a b c d e f g h i j. i \<equiv>\<^sup>?
\<lambda>a b c d e f. ?Rha44
\<lambda>a b c d. rel_set C \<equiv>\<^sup>? \<lambda>a b c d. ?Rg19
\<lambda>a b. rel_set A \<equiv>\<^sup>? \<lambda>a b. ?Rf19
?x' \<equiv>\<^sup>?
\<lambda>S S' pls mns um zero scl b pls' mns' um' zero' scl' b'.
   ?a19 (?aa19 S pls mns um zero scl b)
    (?ab19 S' pls' mns' um' zero' scl' b')
Enter MATCH
\<lambda>a b c d e f g h i j. j \<equiv>\<^sup>? \<lambda>a b c d e f. ?Rh44
\<lambda>a b c d e f g h i j. i \<equiv>\<^sup>?
\<lambda>a b c d e f. ?Rha44
\<lambda>a b c d. rel_set C \<equiv>\<^sup>? \<lambda>a b c d. ?Rg19
\<lambda>a b. rel_set A \<equiv>\<^sup>? \<lambda>a b. ?Rf19
?x' \<equiv>\<^sup>?
\<lambda>S S' pls mns um zero scl b pls' mns' um' zero' scl' b'.
   ?a19 (?aa19 S pls mns um zero scl b)
    (?ab19 S' pls' mns' um' zero' scl' b')
Enter MATCH
\<lambda>a b c d e f g h i j. i \<equiv>\<^sup>?
\<lambda>a b c d e f. ?Rha44
\<lambda>a b c d. rel_set C \<equiv>\<^sup>? \<lambda>a b c d. ?Rg19
\<lambda>a b. rel_set A \<equiv>\<^sup>? \<lambda>a b. ?Rf19
?x' \<equiv>\<^sup>?
\<lambda>S S' pls mns um zero scl b pls' mns' um' zero' scl' b'.
   ?a19 (?aa19 S pls mns um zero scl b)
    (?ab19 S' pls' mns' um' zero' scl' b')
Enter MATCH
\<lambda>a b c d. rel_set C \<equiv>\<^sup>? \<lambda>a b c d. ?Rg19
\<lambda>a b. rel_set A \<equiv>\<^sup>? \<lambda>a b. ?Rf19
?x' \<equiv>\<^sup>?
\<lambda>S S' pls mns um zero scl b pls' mns' um' zero' scl' b'.
   ?a19 (?aa19 S pls mns um zero scl b)
    (?ab19 S' pls' mns' um' zero' scl' b')
Enter MATCH
\<lambda>a b. rel_set A \<equiv>\<^sup>? \<lambda>a b. ?Rf19
?x' \<equiv>\<^sup>?
\<lambda>S S' pls mns um zero scl b pls' mns' um' zero' scl' b'.
   ?a19 (?aa19 S pls mns um zero scl b)
    (?ab19 S' pls' mns' um' zero' scl' b')
locale module_on
  fixes S :: "'b set"
    and
    scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*s\<close> 75)
  assumes "module_on S (*s)"
locale module_pair_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
  assumes "module_pair_on S1 S2 scale1 scale2"
locale module_hom_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and
    s1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*a\<close> 75)
    and
    s2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
      (infixr \<open>*b\<close> 75)
    and f :: "'b \<Rightarrow> 'c"
  assumes "module_hom_on S1 S2 (*a) (*b) f"
locale vector_space_on
  fixes S :: "'b set"
    and
    scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*s\<close> 75)
  assumes "vector_space_on S (*s)"
locale linear_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and s1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and s2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and f :: "'b \<Rightarrow> 'c"
  assumes "linear_on S1 S2 s1 s2 f"
locale finite_dimensional_vector_space_on
  fixes S :: "'a set"
    and scale :: "'b \<Rightarrow> 'a \<Rightarrow> 'a"
    and basis :: "'a set"
  assumes "finite_dimensional_vector_space_on S scale basis"
locale vector_space_pair_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
  assumes "vector_space_pair_on S1 S2 scale1 scale2"
locale finite_dimensional_vector_space_pair_1_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and Basis1 :: "'b set"
  assumes
    "finite_dimensional_vector_space_pair_1_on S1 S2 scale1 scale2 Basis1"
locale finite_dimensional_vector_space_pair_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and Basis1 :: "'b set"
    and Basis2 :: "'c set"
  assumes
    "finite_dimensional_vector_space_pair_on S1 S2 scale1 scale2 Basis1
      Basis2"
locale local_typedef_module_on
  fixes S :: "'b set"
    and scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and s :: "'s itself"
  assumes "local_typedef_module_on TYPE('s) S scale"
locale local_typedef_vector_space_on
  fixes S :: "'b set"
    and scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and s :: "'s itself"
  assumes "local_typedef_vector_space_on TYPE('s) S scale"
locale local_typedef_finite_dimensional_vector_space_on
  fixes S :: "'b set"
    and scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and Basis :: "'b set"
    and s :: "'s itself"
  assumes
    "local_typedef_finite_dimensional_vector_space_on TYPE('s) S scale
      Basis"
locale local_typedef_module_pair
  fixes S1 :: "'b set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and s :: "'s itself"
    and S2 :: "'c set"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and t :: "'t itself"
  assumes "local_typedef_module_pair TYPE('s) TYPE('t) S1 scale1 S2 scale2"
locale local_typedef_vector_space_pair
  fixes S1 :: "'b set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and s :: "'s itself"
    and S2 :: "'c set"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and t :: "'t itself"
  assumes
    "local_typedef_vector_space_pair TYPE('s) TYPE('t) S1 scale1 S2 scale2"
locale local_typedef_finite_dimensional_vector_space_pair_1
  fixes S1 :: "'b set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and Basis1 :: "'b set"
    and s :: "'s itself"
    and S2 :: "'c set"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and t :: "'t itself"
  assumes
    "local_typedef_finite_dimensional_vector_space_pair_1 TYPE('s) TYPE('t)
      S1 scale1 Basis1 S2 scale2"
locale local_typedef_finite_dimensional_vector_space_pair
  fixes S1 :: "'b set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and Basis1 :: "'b set"
    and s :: "'s itself"
    and S2 :: "'c set"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and Basis2 :: "'c set"
    and t :: "'t itself"
  assumes
    "local_typedef_finite_dimensional_vector_space_pair TYPE('s) TYPE('t) S1
      scale1 Basis1 S2 scale2 Basis2"
locale module_on
  fixes S :: "'b set"
    and
    scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*s\<close> 75)
  assumes "module_on S (*s)"
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Rule already declared as introduction (intro)
### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
### (?A ===> ?B) ?f ?g
locale module
  fixes
    scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*s\<close> 75)
  assumes "module (*s)"
  notes
    "module_axioms" = (\<open>module (*s)\<close>)
      ["attribute" "<attribute>"]
  notes
    "scale_right_distrib" =
      (\<open>?a *s (?x + ?y) = ?a *s ?x + ?a *s ?y\<close>)
      ["algebra_simps", "algebra_split_simps"]
  notes
    "scale_left_distrib" =
      (\<open>(?a + ?b) *s ?x = ?a *s ?x + ?b *s ?x\<close>)
      ["algebra_simps", "algebra_split_simps"]
  notes
    "scale_scale" = (\<open>?a *s ?b *s ?x = (?a * ?b) *s ?x\<close>)
      ["simp"]
  notes "scale_one" = (\<open>(1::'a) *s ?x = ?x\<close>) ["simp"]
  notes theorem
    "scale_left_commute" = \<open>?a *s ?b *s ?x = ?b *s ?a *s ?x\<close>
  notes theorem
    "scale_zero_left" = (\<open>(0::'a) *s ?x = (0::'b)\<close>) ["simp"]
  notes theorem
    "scale_minus_left" = (\<open>- ?a *s ?x = - (?a *s ?x)\<close>) ["simp"]
  notes theorem
    "scale_left_diff_distrib" =
      (\<open>(?a - ?b) *s ?x = ?a *s ?x - ?b *s ?x\<close>)
      ["algebra_simps", "algebra_split_simps"]
  notes theorem
    "scale_sum_left" =
      \<open>sum ?f ?A *s ?x = (\<Sum>a\<in>?A. ?f a *s ?x)\<close>
  notes theorem
    "scale_zero_right" = (\<open>?a *s (0::'b) = (0::'b)\<close>) ["simp"]
  notes theorem
    "scale_minus_right" = (\<open>?a *s - ?x = - (?a *s ?x)\<close>)
      ["simp"]
  notes theorem
    "scale_right_diff_distrib" =
      (\<open>?a *s (?x - ?y) = ?a *s ?x - ?a *s ?y\<close>)
      ["algebra_simps", "algebra_split_simps"]
  notes theorem
    "scale_sum_right" =
      \<open>?a *s sum ?f ?A = (\<Sum>x\<in>?A. ?a *s ?f x)\<close>
  notes theorem
    "sum_constant_scale" =
      \<open>(\<Sum>x\<in>?A. ?y) = of_nat (card ?A) *s ?y\<close>
  notes theorem
    "scale_left_distrib_NO_MATCH" =
      \<open>NO_MATCH (?x div ?y) ?c \<Longrightarrow>
             (?a + ?b) *s ?x = ?a *s ?x + ?b *s ?x\<close>
  notes theorem
    "scale_right_distrib_NO_MATCH" =
      \<open>NO_MATCH (?x div ?y) ?a \<Longrightarrow>
             ?a *s (?x + ?y) = ?a *s ?x + ?a *s ?y\<close>
  notes theorem
    "scale_left_diff_distrib_NO_MATCH" =
      \<open>NO_MATCH (?x div ?y) ?c \<Longrightarrow>
             (?a - ?b) *s ?x = ?a *s ?x - ?b *s ?x\<close>
  notes theorem
    "scale_right_diff_distrib_NO_MATCH" =
      \<open>NO_MATCH (?x div ?y) ?a \<Longrightarrow>
             ?a *s (?x - ?y) = ?a *s ?x - ?a *s ?y\<close>
  notes theorem
    (\<open>NO_MATCH (?x div ?y) ?c \<Longrightarrow>
            (?a + ?b) *s ?x = ?a *s ?x + ?b *s ?x\<close>)
      ["field_simps", "field_split_simps"]
      (\<open>NO_MATCH (?x div ?y) ?a \<Longrightarrow>
              ?a *s (?x + ?y) = ?a *s ?x + ?a *s ?y\<close>)
      ["field_simps", "field_split_simps"]
      (\<open>NO_MATCH (?x div ?y) ?c \<Longrightarrow>
              (?a - ?b) *s ?x = ?a *s ?x - ?b *s ?x\<close>)
      ["field_simps", "field_split_simps"]
      (\<open>NO_MATCH (?x div ?y) ?a \<Longrightarrow>
              ?a *s (?x - ?y) = ?a *s ?x - ?a *s ?y\<close>)
      ["field_simps", "field_split_simps"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "subspace_def" =
      \<open>local.subspace ?S =
             ((0::'b) \<in> ?S \<and>
              (\<forall>x\<in>?S. \<forall>y\<in>?S. x + y \<in> ?S) \<and>
              (\<forall>c. \<forall>x\<in>?S. c *s x \<in> ?S))\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "subspaceI" =
      \<open>\<lbrakk>(0::'b) \<in> ?S;
              \<And>x y.
                 \<lbrakk>x \<in> ?S; y \<in> ?S\<rbrakk>
                 \<Longrightarrow> x + y \<in> ?S;
              \<And>c x.
                 x \<in> ?S \<Longrightarrow> c *s x \<in> ?S\<rbrakk>
             \<Longrightarrow> local.subspace ?S\<close>
  notes theorem
    "subspace_UNIV" = (\<open>local.subspace UNIV\<close>) ["simp"]
  notes theorem
    "subspace_single_0" = (\<open>local.subspace {0::'b}\<close>) ["simp"]
  notes theorem
    "subspace_0" =
      \<open>local.subspace ?S \<Longrightarrow> (0::'b) \<in> ?S\<close>
  notes theorem
    "subspace_add" =
      \<open>\<lbrakk>local.subspace ?S; ?x \<in> ?S; ?y \<in> ?S\<rbrakk>
             \<Longrightarrow> ?x + ?y \<in> ?S\<close>
  notes theorem
    "subspace_scale" =
      \<open>\<lbrakk>local.subspace ?S; ?x \<in> ?S\<rbrakk>
             \<Longrightarrow> ?c *s ?x \<in> ?S\<close>
  notes theorem
    "subspace_neg" =
      \<open>\<lbrakk>local.subspace ?S; ?x \<in> ?S\<rbrakk>
             \<Longrightarrow> - ?x \<in> ?S\<close>
  notes theorem
    "subspace_diff" =
      \<open>\<lbrakk>local.subspace ?S; ?x \<in> ?S; ?y \<in> ?S\<rbrakk>
             \<Longrightarrow> ?x - ?y \<in> ?S\<close>
  notes theorem
    "subspace_sum" =
      \<open>\<lbrakk>local.subspace ?A;
              \<And>x. x \<in> ?B \<Longrightarrow> ?f x \<in> ?A\<rbrakk>
             \<Longrightarrow> sum ?f ?B \<in> ?A\<close>
  notes theorem
    "subspace_Int" =
      \<open>(\<And>i.
                 i \<in> ?I \<Longrightarrow>
                 local.subspace (?s i)) \<Longrightarrow>
             local.subspace (\<Inter> (?s ` ?I))\<close>
  notes theorem
    "subspace_Inter" =
      \<open>Ball ?f local.subspace \<Longrightarrow>
             local.subspace (\<Inter> ?f)\<close>
  notes theorem
    "subspace_inter" =
      \<open>\<lbrakk>local.subspace ?A; local.subspace ?B\<rbrakk>
             \<Longrightarrow> local.subspace (?A \<inter> ?B)\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "span_explicit" =
      \<open>local.span ?b =
             {\<Sum>a\<in>t. r a *s a |t r.
              finite t \<and> t \<subseteq> ?b}\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "span_explicit'" =
      \<open>local.span ?b =
             {\<Sum>v | f v \<noteq> (0::'a). f v *s v |f.
              finite {v. f v \<noteq> (0::'a)} \<and>
              (\<forall>v.
                  f v \<noteq> (0::'a) \<longrightarrow>
                  v \<in> ?b)}\<close>
  notes theorem
    "span_alt" =
      \<open>local.span ?B =
             {\<Sum>x | f x \<noteq> (0::'a). f x *s x |f.
              {x. f x \<noteq> (0::'a)} \<subseteq> ?B \<and>
              finite {x. f x \<noteq> (0::'a)}}\<close>
  notes theorem
    "span_finite" =
      \<open>finite ?S \<Longrightarrow>
             local.span ?S =
             range (\<lambda>u. \<Sum>v\<in>?S. u v *s v)\<close>
  notes theorem
    "span_induct_alt" =
      (\<open>\<lbrakk>?x \<in> local.span ?S; ?h (0::'b);
               \<And>c x y.
                  \<lbrakk>x \<in> ?S; ?h y\<rbrakk>
                  \<Longrightarrow> ?h (c *s x + y)\<rbrakk>
              \<Longrightarrow> ?h ?x\<close>)
      ["consumes" 1, "case_names" base step, "induct" set : local.span]
  notes theorem
    "span_mono" =
      \<open>?A \<subseteq> ?B \<Longrightarrow>
             local.span ?A \<subseteq> local.span ?B\<close>
  notes theorem
    "span_base" =
      \<open>?a \<in> ?S \<Longrightarrow> ?a \<in> local.span ?S\<close>
  notes theorem
    "span_superset" = \<open>?S \<subseteq> local.span ?S\<close>
  notes theorem "span_zero" = \<open>(0::'b) \<in> local.span ?S\<close>
  notes theorem
    "span_UNIV" = (\<open>local.span UNIV = UNIV\<close>) ["simp"]
  notes theorem
    "span_add" =
      \<open>\<lbrakk>?x \<in> local.span ?S;
              ?y \<in> local.span ?S\<rbrakk>
             \<Longrightarrow> ?x + ?y \<in> local.span ?S\<close>
  notes theorem
    "span_scale" =
      \<open>?x \<in> local.span ?S \<Longrightarrow>
             ?c *s ?x \<in> local.span ?S\<close>
  notes theorem
    "subspace_span" = (\<open>local.subspace (local.span ?S)\<close>)
      ["iff"]
  notes theorem
    "span_neg" =
      \<open>?x \<in> local.span ?S \<Longrightarrow>
             - ?x \<in> local.span ?S\<close>
  notes theorem
    "span_diff" =
      \<open>\<lbrakk>?x \<in> local.span ?S;
              ?y \<in> local.span ?S\<rbrakk>
             \<Longrightarrow> ?x - ?y \<in> local.span ?S\<close>
  notes theorem
    "span_sum" =
      \<open>(\<And>x.
                 x \<in> ?A \<Longrightarrow>
                 ?f x \<in> local.span ?S) \<Longrightarrow>
             sum ?f ?A \<in> local.span ?S\<close>
  notes theorem
    "span_minimal" =
      \<open>\<lbrakk>?S \<subseteq> ?T; local.subspace ?T\<rbrakk>
             \<Longrightarrow> local.span ?S \<subseteq> ?T\<close>
  notes theorem
    "span_def" = \<open>local.span ?S = local.subspace hull ?S\<close>
  notes theorem
    "span_unique" =
      \<open>\<lbrakk>?S \<subseteq> ?T; local.subspace ?T;
              \<And>T'.
                 \<lbrakk>?S \<subseteq> T'; local.subspace T'\<rbrakk>
                 \<Longrightarrow> ?T \<subseteq> T'\<rbrakk>
             \<Longrightarrow> local.span ?S = ?T\<close>
  notes theorem
    "span_subspace_induct" =
      (\<open>\<lbrakk>?x \<in> local.span ?S; local.subspace ?P;
               \<And>x. x \<in> ?S \<Longrightarrow> x \<in> ?P\<rbrakk>
              \<Longrightarrow> ?x \<in> ?P\<close>)
      ["consumes" 2]
  notes theorem
    "span_induct" =
      (\<open>\<lbrakk>?x \<in> local.span ?S; local.subspace (Collect ?P);
               \<And>x. x \<in> ?S \<Longrightarrow> ?P x\<rbrakk>
              \<Longrightarrow> ?P ?x\<close>)
      ["consumes" 1, "case_names" base step, "induct" set : local.span]
  notes theorem
    "span_empty" = (\<open>local.span {} = {0::'b}\<close>) ["simp"]
  notes theorem
    "span_subspace" =
      \<open>\<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> local.span ?A;
              local.subspace ?B\<rbrakk>
             \<Longrightarrow> local.span ?A = ?B\<close>
  notes theorem
    "span_span" = \<open>local.span (local.span ?A) = local.span ?A\<close>
  notes theorem
    "span_add_eq" =
      \<open>?x \<in> local.span ?S \<Longrightarrow>
             (?x + ?y \<in> local.span ?S) =
             (?y \<in> local.span ?S)\<close>
  notes theorem
    "span_add_eq2" =
      \<open>?y \<in> local.span ?S \<Longrightarrow>
             (?x + ?y \<in> local.span ?S) =
             (?x \<in> local.span ?S)\<close>
  notes theorem
    "span_singleton" =
      \<open>local.span {?x} = range (\<lambda>k. k *s ?x)\<close>
  notes theorem
    "span_Un" =
      \<open>local.span (?S \<union> ?T) =
             {x + y |x y.
              x \<in> local.span ?S \<and> y \<in> local.span ?T}\<close>
  notes theorem
    "span_insert" =
      \<open>local.span (insert ?a ?S) =
             {x. \<exists>k. x - k *s ?a \<in> local.span ?S}\<close>
  notes theorem
    "span_breakdown" =
      \<open>\<lbrakk>?b \<in> ?S; ?a \<in> local.span ?S\<rbrakk>
             \<Longrightarrow> \<exists>k.
                                  ?a - k *s ?b
                                  \<in> local.span (?S - {?b})\<close>
  notes theorem
    "span_breakdown_eq" =
      \<open>(?x \<in> local.span (insert ?a ?S)) =
             (\<exists>k. ?x - k *s ?a \<in> local.span ?S)\<close>
  notes theorem
    "span_clauses" =
      \<open>?a \<in> ?S \<Longrightarrow> ?a \<in> local.span ?S\<close>
      \<open>(0::'b) \<in> local.span ?S\<close>
      \<open>\<lbrakk>?x \<in> local.span ?S;
              ?y \<in> local.span ?S\<rbrakk>
             \<Longrightarrow> ?x + ?y \<in> local.span ?S\<close>
      \<open>?x \<in> local.span ?S \<Longrightarrow>
             ?c *s ?x \<in> local.span ?S\<close>
  notes theorem
    "span_eq_iff" =
      (\<open>(local.span ?s = ?s) = local.subspace ?s\<close>) ["simp"]
  notes theorem
    "span_eq" =
      \<open>(local.span ?S = local.span ?T) =
             (?S \<subseteq> local.span ?T \<and>
              ?T \<subseteq> local.span ?S)\<close>
  notes theorem
    "eq_span_insert_eq" =
      \<open>?x - ?y \<in> local.span ?S \<Longrightarrow>
             local.span (insert ?x ?S) = local.span (insert ?y ?S)\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "dependent_explicit" =
      \<open>local.dependent ?s =
             (\<exists>t u.
                 finite t \<and>
                 t \<subseteq> ?s \<and>
                 (\<Sum>v\<in>t. u v *s v) = (0::'b) \<and>
                 (\<exists>v\<in>t. u v \<noteq> (0::'a)))\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "dependent_mono" =
      \<open>\<lbrakk>local.dependent ?B; ?B \<subseteq> ?A\<rbrakk>
             \<Longrightarrow> local.dependent ?A\<close>
  notes theorem
    "independent_mono" =
      \<open>\<lbrakk>local.independent ?A; ?B \<subseteq> ?A\<rbrakk>
             \<Longrightarrow> local.independent ?B\<close>
  notes theorem
    "dependent_zero" =
      \<open>(0::'b) \<in> ?A \<Longrightarrow> local.dependent ?A\<close>
  notes theorem
    "independent_empty" = (\<open>local.independent {}\<close>)
      ["HOL.intro"]
  notes theorem
    "independent_explicit_module" =
      \<open>local.independent ?s =
             (\<forall>t u v.
                 finite t \<longrightarrow>
                 t \<subseteq> ?s \<longrightarrow>
                 (\<Sum>v\<in>t. u v *s v) = (0::'b) \<longrightarrow>
                 v \<in> t \<longrightarrow> u v = (0::'a))\<close>
  notes theorem
    "independentD" =
      \<open>\<lbrakk>local.independent ?s; finite ?t; ?t \<subseteq> ?s;
              (\<Sum>v\<in>?t. ?u v *s v) = (0::'b); ?v \<in> ?t\<rbrakk>
             \<Longrightarrow> ?u ?v = (0::'a)\<close>
  notes theorem
    "independent_Union_directed" =
      \<open>\<lbrakk>\<And>c d.
                         \<lbrakk>c \<in> ?C; d \<in> ?C\<rbrakk>
                         \<Longrightarrow> c \<subseteq> d \<or>
     d \<subseteq> c;
              \<And>c.
                 c \<in> ?C \<Longrightarrow> local.independent c\<rbrakk>
             \<Longrightarrow> local.independent (\<Union> ?C)\<close>
  notes theorem
    "dependent_finite" =
      \<open>finite ?S \<Longrightarrow>
             local.dependent ?S =
             (\<exists>u.
                 (\<exists>v\<in>?S. u v \<noteq> (0::'a)) \<and>
                 (\<Sum>v\<in>?S. u v *s v) = (0::'b))\<close>
  notes theorem
    "dependent_alt" =
      \<open>local.dependent ?B =
             (\<exists>X.
                 finite {x. X x \<noteq> (0::'a)} \<and>
                 {x. X x \<noteq> (0::'a)} \<subseteq> ?B \<and>
                 (\<Sum>x | X x \<noteq> (0::'a). X x *s x) = (0::'b) \<and>
                 (\<exists>x. X x \<noteq> (0::'a)))\<close>
  notes theorem
    "independent_alt" =
      \<open>local.independent ?B =
             (\<forall>X.
                 finite {x. X x \<noteq> (0::'a)} \<longrightarrow>
                 {x. X x \<noteq> (0::'a)} \<subseteq> ?B \<longrightarrow>
                 (\<Sum>x | X x \<noteq> (0::'a). X x *s x) =
                 (0::'b) \<longrightarrow>
                 (\<forall>x. X x = (0::'a)))\<close>
  notes theorem
    "independentD_alt" =
      \<open>\<lbrakk>local.independent ?B;
              finite {x. ?X x \<noteq> (0::'a)};
              {x. ?X x \<noteq> (0::'a)} \<subseteq> ?B;
              (\<Sum>x | ?X x \<noteq> (0::'a). ?X x *s x) =
              (0::'b)\<rbrakk>
             \<Longrightarrow> ?X ?x = (0::'a)\<close>
  notes theorem
    "independentD_unique" =
      \<open>\<lbrakk>local.independent ?B;
              finite {x. ?X x \<noteq> (0::'a)};
              {x. ?X x \<noteq> (0::'a)} \<subseteq> ?B;
              finite {x. ?Y x \<noteq> (0::'a)};
              {x. ?Y x \<noteq> (0::'a)} \<subseteq> ?B;
              (\<Sum>x | ?X x \<noteq> (0::'a). ?X x *s x) =
              (\<Sum>x | ?Y x \<noteq> (0::'a). ?Y x *s x)\<rbrakk>
             \<Longrightarrow> ?X = ?Y\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "representation_def" =
      \<open>local.representation ?basis ?v =
             (if local.independent ?basis \<and> ?v \<in> local.span ?basis
              then SOME f.
                      (\<forall>v.
                          f v \<noteq> (0::'a) \<longrightarrow>
                          v \<in> ?basis) \<and>
                      finite {v. f v \<noteq> (0::'a)} \<and>
                      (\<Sum>v | f v \<noteq> (0::'a). f v *s v) = ?v
              else (\<lambda>b. 0::'a))\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "unique_representation" =
      \<open>\<lbrakk>local.independent ?basis;
              \<And>v.
                 ?f v \<noteq> (0::'a) \<Longrightarrow> v \<in> ?basis;
              \<And>v.
                 ?g v \<noteq> (0::'a) \<Longrightarrow> v \<in> ?basis;
              finite {v. ?f v \<noteq> (0::'a)};
              finite {v. ?g v \<noteq> (0::'a)};
              (\<Sum>v | ?f v \<noteq> (0::'a). ?f v *s v) =
              (\<Sum>v | ?g v \<noteq> (0::'a). ?g v *s v)\<rbrakk>
             \<Longrightarrow> ?f = ?g\<close>
  notes theorem
    "representation_ne_zero" =
      \<open>local.representation ?basis ?v ?b \<noteq>
             (0::'a) \<Longrightarrow>
             ?b \<in> ?basis\<close>
  notes theorem
    "finite_representation" =
      \<open>finite
              {b. local.representation ?basis ?v b \<noteq> (0::'a)}\<close>
  notes theorem
    "sum_nonzero_representation_eq" =
      \<open>\<lbrakk>local.independent ?basis;
              ?v \<in> local.span ?basis\<rbrakk>
             \<Longrightarrow> (\<Sum>b | local.representation ?basis ?v
     b \<noteq>
    (0::'a).
                                  local.representation ?basis ?v b *s b) =
                               ?v\<close>
  notes theorem
    "sum_representation_eq" =
      \<open>\<lbrakk>local.independent ?basis; ?v \<in> local.span ?basis;
              finite ?B; ?basis \<subseteq> ?B\<rbrakk>
             \<Longrightarrow> (\<Sum>b\<in>?B.
                                  local.representation ?basis ?v b *s b) =
                               ?v\<close>
  notes theorem
    "representation_eqI" =
      \<open>\<lbrakk>local.independent ?basis; ?v \<in> local.span ?basis;
              \<And>b.
                 ?f b \<noteq> (0::'a) \<Longrightarrow> b \<in> ?basis;
              finite {b. ?f b \<noteq> (0::'a)};
              (\<Sum>b | ?f b \<noteq> (0::'a). ?f b *s b) = ?v\<rbrakk>
             \<Longrightarrow> local.representation ?basis ?v = ?f\<close>
  notes theorem
    "representation_basis" =
      \<open>\<lbrakk>local.independent ?basis; ?b \<in> ?basis\<rbrakk>
             \<Longrightarrow> local.representation ?basis ?b =
                               (\<lambda>v.
                                   if v = ?b then 1::'a
                                   else (0::'a))\<close>
  notes theorem
    "representation_zero" =
      \<open>local.representation ?basis (0::'b) =
             (\<lambda>b. 0::'a)\<close>
  notes theorem
    "representation_diff" =
      \<open>\<lbrakk>local.independent ?basis; ?v \<in> local.span ?basis;
              ?u \<in> local.span ?basis\<rbrakk>
             \<Longrightarrow> local.representation ?basis (?u - ?v) =
                               (\<lambda>b.
                                   local.representation ?basis ?u b -
                                   local.representation ?basis ?v b)\<close>
  notes theorem
    "representation_neg" =
      \<open>\<lbrakk>local.independent ?basis;
              ?v \<in> local.span ?basis\<rbrakk>
             \<Longrightarrow> local.representation ?basis (- ?v) =
                               (\<lambda>b.
                                   - local.representation ?basis ?v
b)\<close>
  notes theorem
    "representation_add" =
      \<open>\<lbrakk>local.independent ?basis; ?v \<in> local.span ?basis;
              ?u \<in> local.span ?basis\<rbrakk>
             \<Longrightarrow> local.representation ?basis (?u + ?v) =
                               (\<lambda>b.
                                   local.representation ?basis ?u b +
                                   local.representation ?basis ?v b)\<close>
  notes theorem
    "representation_sum" =
      \<open>\<lbrakk>local.independent ?basis;
              \<And>i.
                 i \<in> ?I \<Longrightarrow>
                 ?v i \<in> local.span ?basis\<rbrakk>
             \<Longrightarrow> local.representation ?basis (sum ?v ?I) =
                               (\<lambda>b.
                                   \<Sum>i\<in>?I.
                                     local.representation ?basis (?v i)
b)\<close>
  notes theorem
    "representation_scale" =
      \<open>\<lbrakk>local.independent ?basis;
              ?v \<in> local.span ?basis\<rbrakk>
             \<Longrightarrow> local.representation ?basis (?r *s ?v) =
                               (\<lambda>b.
                                   ?r *
                                   local.representation ?basis ?v b)\<close>
  notes theorem
    "representation_extend" =
      \<open>\<lbrakk>local.independent ?basis; ?v \<in> local.span ?basis';
              ?basis' \<subseteq> ?basis\<rbrakk>
             \<Longrightarrow> local.representation ?basis ?v =
                               local.representation ?basis' ?v\<close>
  notes theorem
    "spanning_subset_independent" =
      \<open>\<lbrakk>?B \<subseteq> ?A; local.independent ?A;
              ?A \<subseteq> local.span ?B\<rbrakk>
             \<Longrightarrow> ?A = ?B\<close>
  notes theorem
    "module_hom_scale_self" =
      (\<open>module_hom (*s) (*s) ((*s) ?c)\<close>) ["simp"]
  notes theorem
    "module_hom_scale_left" =
      (\<open>module_hom (*) (*s) (\<lambda>r. r *s ?x)\<close>) ["simp"]
  notes theorem "module_hom_id" = \<open>module_hom (*s) (*s) id\<close>
  notes theorem
    "module_hom_ident" = \<open>module_hom (*s) (*s) (\<lambda>x. x)\<close>
  notes theorem
    "module_hom_uminus" = \<open>module_hom (*s) (*s) uminus\<close>
  notes theorem
    "span_with" = \<open>local.span = span_with (+) (0::'b) (*s)\<close>
  notes theorem
    "dependent_with" =
      \<open>local.dependent = dependent_with (+) (0::'b) (*s)\<close>
  notes theorem
    "subspace_with" =
      \<open>local.subspace = subspace_with (+) (0::'b) (*s)\<close>
locale vector_space_on
  fixes S :: "'b set"
    and
    scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*s\<close> 75)
  assumes "vector_space_on S (*s)"
locale finite_dimensional_vector_space_on
  fixes S :: "'a set"
    and scale :: "'b \<Rightarrow> 'a \<Rightarrow> 'a"
    and basis :: "'a set"
  assumes "finite_dimensional_vector_space_on S scale basis"
locale module_pair_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
  assumes "module_pair_on S1 S2 scale1 scale2"
locale vector_space_pair_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
  assumes "vector_space_pair_on S1 S2 scale1 scale2"
locale finite_dimensional_vector_space_pair_1_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and Basis1 :: "'b set"
  assumes
    "finite_dimensional_vector_space_pair_1_on S1 S2 scale1 scale2 Basis1"
locale finite_dimensional_vector_space_pair_on
  fixes S1 :: "'b set"
    and S2 :: "'c set"
    and scale1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and scale2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and Basis1 :: "'b set"
    and Basis2 :: "'c set"
  assumes
    "finite_dimensional_vector_space_pair_on S1 S2 scale1 scale2 Basis1
      Basis2"
### theory "HOL-Types_To_Sets.Linear_Algebra_On"
### 12.960s elapsed time, 21.020s cpu time, 0.760s GC time
Loading theory "Smooth_Manifolds.Analysis_More" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Bump_Function" via "Smooth_Manifolds.Smooth")
instantiation
  fun :: (type, scaleR) scaleR
  scaleR_fun == scaleR ::
    real
    \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b
bundle no_matrix_mult
### Ignoring duplicate rewrite rule:
### open {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed UNIV \<equiv> True
### Ignoring duplicate rewrite rule:
### closed ?S1 \<Longrightarrow> closed (insert ?a1 ?S1) \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {..<?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..<?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {..?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous bot ?f1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \<noteq> (0::?'b1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x / ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \<noteq> 1;
###  0 < ?g1 ?a1\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. log (?f1 x) (?g1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \<noteq> 0\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x powr ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; cos (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. tan (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; sin (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. cot (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 ?g1 \<Longrightarrow>
### continuous ?F1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 ?g1 \<Longrightarrow>
### continuous_on ?s1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 (\<lambda>x. x) \<equiv> True
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
locale vector_space_on
  fixes S :: "'b set"
    and
    scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*s\<close> 75)
  assumes "vector_space_on S (*s)"
### theory "Smooth_Manifolds.Analysis_More"
### 2.888s elapsed time, 9.024s cpu time, 0.000s GC time
Loading theory "Smooth_Manifolds.Chart" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Differentiable_Manifold" via "Smooth_Manifolds.Topological_Manifold")
Loading theory "Smooth_Manifolds.Smooth" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Bump_Function")
*** Undefined fact: "sum_not_0" (line 429 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
*** At command "by" (line 429 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
Found termination order: "(\<lambda>p. size (snd (snd p))) <*mlex*> {}"
*** Undefined fact: "sum_not_0" (line 434 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
*** At command "by" (line 434 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
### Ignoring duplicate rewrite rule:
### topspace (subtopology ?U1 ?V1) \<equiv> topspace ?U1 \<inter> ?V1
consts
  nth_derivative ::
    "nat
     \<Rightarrow> ('a \<Rightarrow> 'b)
                   \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
### Ignoring duplicate rewrite rule:
### topspace (subtopology ?U1 ?V1) \<equiv> topspace ?U1 \<inter> ?V1
### theory "Smooth_Manifolds.Chart"
### 1.001s elapsed time, 3.912s cpu time, 0.360s GC time
Loading theory "Smooth_Manifolds.Topological_Manifold" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity" via "Smooth_Manifolds.Differentiable_Manifold")
locale manifold
  fixes charts :: "('a, 'e) chart set"
### theory "Smooth_Manifolds.Topological_Manifold"
### 0.126s elapsed time, 0.504s cpu time, 0.000s GC time
### theory "Smooth_Manifolds.Smooth"
### 1.852s elapsed time, 7.316s cpu time, 0.360s GC time
Loading theory "Smooth_Manifolds.Bump_Function" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity")
Loading theory "Smooth_Manifolds.Differentiable_Manifold" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space" via "Smooth_Manifolds.Partition_Of_Unity")
### Ignoring duplicate rewrite rule:
### frechet_derivative (\<lambda>x. ?c1) (at ?a1) \<equiv> \<lambda>x. 0::?'b1
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### theory "Smooth_Manifolds.Bump_Function"
### 0.780s elapsed time, 2.560s cpu time, 0.000s GC time
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
locale c_manifold'
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold' charts k"
locale submanifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
    and S :: "'a set"
  assumes "submanifold charts k S"
locale c_manifolds
  fixes k :: "enat"
    and charts1 :: "('a, 'b) chart set"
    and charts2 :: "('c, 'd) chart set"
  assumes "c_manifolds k charts1 charts2"
locale diff
  fixes k :: "enat"
    and charts1 :: "('a, 'e) chart set"
    and charts2 :: "('b, 'f) chart set"
    and f :: "'a \<Rightarrow> 'b"
  assumes "diff k charts1 charts2 f"
locale c_manifolds
  fixes k :: "enat"
    and charts1 :: "('a, 'b) chart set"
    and charts2 :: "('c, 'd) chart set"
  assumes "c_manifolds k charts1 charts2"
locale diff
  fixes k :: "enat"
    and charts1 :: "('a, 'e) chart set"
    and charts2 :: "('b, 'f) chart set"
    and f :: "'a \<Rightarrow> 'b"
  assumes "diff k charts1 charts2 f"
locale diff
  fixes k :: "enat"
    and charts1 :: "('a, 'e) chart set"
    and charts2 :: "('b, 'f) chart set"
    and f :: "'a \<Rightarrow> 'b"
  assumes "diff k charts1 charts2 f"
locale c_manifolds
  fixes k :: "enat"
    and charts1 :: "('a, 'b) chart set"
    and charts2 :: "('c, 'd) chart set"
  assumes "c_manifolds k charts1 charts2"
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### Ignoring duplicate rewrite rule:
### open {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed UNIV \<equiv> True
### Ignoring duplicate rewrite rule:
### closed ?S1 \<Longrightarrow> closed (insert ?a1 ?S1) \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {..<?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..<?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {..?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous bot ?f1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \<noteq> (0::?'b1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x / ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \<noteq> 1;
###  0 < ?g1 ?a1\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. log (?f1 x) (?g1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \<noteq> 0\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x powr ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; cos (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. tan (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; sin (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. cot (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 ?g1 \<Longrightarrow>
### continuous ?F1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 ?g1 \<Longrightarrow>
### continuous_on ?s1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### frechet_derivative (\<lambda>x. ?c1) (at ?a1) \<equiv> \<lambda>x. 0::?'b1
locale c_manifolds
  fixes k :: "enat"
    and charts1 :: "('a, 'b) chart set"
    and charts2 :: "('c, 'd) chart set"
  assumes "c_manifolds k charts1 charts2"
locale diff
  fixes k :: "enat"
    and charts1 :: "('a, 'e) chart set"
    and charts2 :: "('b, 'f) chart set"
    and f :: "'a \<Rightarrow> 'b"
  assumes "diff k charts1 charts2 f"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
locale diff_fun
  fixes k :: "enat"
    and charts :: "('a, 'c) chart set"
    and f :: "'a \<Rightarrow> 'b"
  assumes "diff_fun k charts f"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
locale diff_fun
  fixes k :: "enat"
    and charts :: "('a, 'c) chart set"
    and f :: "'a \<Rightarrow> 'b"
  assumes "diff_fun k charts f"
locale diffeomorphism
  fixes k :: "enat"
    and charts1 :: "('a, 'b) chart set"
    and charts2 :: "('c, 'd) chart set"
    and f :: "'a \<Rightarrow> 'c"
    and f' :: "'c \<Rightarrow> 'a"
  assumes "Differentiable_Manifold.diffeomorphism k charts1 charts2 f f'"
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
locale diff_fun
  fixes k :: "enat"
    and charts :: "('a, 'c) chart set"
    and f :: "'a \<Rightarrow> 'b"
  assumes "diff_fun k charts f"
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### theory "Smooth_Manifolds.Differentiable_Manifold"
### 2.195s elapsed time, 8.140s cpu time, 0.420s GC time
Loading theory "Smooth_Manifolds.Partition_Of_Unity" (required by "Smooth_Manifolds.Cotangent_Space" via "Smooth_Manifolds.Tangent_Space")
Loading theory "Smooth_Manifolds.Product_Manifold"
### Ignoring duplicate rewrite rule:
### open {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed UNIV \<equiv> True
### Ignoring duplicate rewrite rule:
### closed ?S1 \<Longrightarrow> closed (insert ?a1 ?S1) \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {..<?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..<?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {..?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous bot ?f1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \<noteq> (0::?'b1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x / ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \<noteq> 1;
###  0 < ?g1 ?a1\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. log (?f1 x) (?g1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \<noteq> 0\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x powr ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; cos (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. tan (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; sin (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. cot (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 ?g1 \<Longrightarrow>
### continuous ?F1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 ?g1 \<Longrightarrow>
### continuous_on ?s1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 (\<lambda>x. x) \<equiv> True
Loading theory "Smooth_Manifolds.Projective_Space"
locale c_manifold_prod
  fixes k :: "enat"
    and charts1 :: "('a, 'b) chart set"
    and charts2 :: "('c, 'd) chart set"
  assumes "c_manifold_prod k charts1 charts2"
### theory "Smooth_Manifolds.Product_Manifold"
### 0.363s elapsed time, 1.444s cpu time, 0.000s GC time
Loading theory "Smooth_Manifolds.Sphere"
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### theory "Smooth_Manifolds.Partition_Of_Unity"
### 0.726s elapsed time, 2.888s cpu time, 0.000s GC time
Loading theory "Smooth_Manifolds.Tangent_Space" (required by "Smooth_Manifolds.Cotangent_Space")
instantiation
  sphere :: (real_normed_vector) topological_space
  open_sphere == open :: 'a sphere set \<Rightarrow> bool
instantiation
  nonzero :: (euclidean_space) topological_space
  open_nonzero == open :: 'a nonzero set \<Rightarrow> bool
locale real_vector_space_on
  fixes S :: "'a set"
  assumes "real_vector_space_on S"
instantiation
  nonzero :: (euclidean_space) scaleR
  scaleR_nonzero == scaleR ::
    real \<Rightarrow> 'a nonzero \<Rightarrow> 'a nonzero
### theory "Smooth_Manifolds.Sphere"
### 0.557s elapsed time, 2.220s cpu time, 0.000s GC time
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
instantiation
  nonzero :: (euclidean_space) plus
  plus_nonzero == plus ::
    'a nonzero \<Rightarrow> 'a nonzero \<Rightarrow> 'a nonzero
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### frechet_derivative id (at ?a1) \<equiv> id
instantiation
  nonzero :: (euclidean_space) minus
  minus_nonzero == minus ::
    'a nonzero \<Rightarrow> 'a nonzero \<Rightarrow> 'a nonzero
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
locale real_vector_space_pair_on
  fixes S :: "'a set"
    and T :: "'b set"
  assumes "real_vector_space_pair_on S T"
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### frechet_derivative id (at ?a1) \<equiv> id
instantiation
  nonzero :: (euclidean_space) dist
  dist_nonzero == dist ::
    'a nonzero \<Rightarrow> 'a nonzero \<Rightarrow> real
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
instantiation
  nonzero :: (euclidean_space) norm
  norm_nonzero == norm :: 'a nonzero \<Rightarrow> real
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
Proofs for inductive predicate(s) "proj_rel"
locale finite_dimensional_real_vector_space_on
  fixes S :: "'a set"
    and basis :: "'a set"
  assumes "finite_dimensional_real_vector_space_on S basis"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### No map function defined for Projective_Space.nonzero. This will cause problems later on.
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Generation of a parametrized correspondence relation failed.
### Reason:  No relator for the type "Projective_Space.nonzero" found.
locale finite_dimensional_real_vector_space_pair_1_on
  fixes S1 :: "'a set"
    and S2 :: "'b set"
    and basis :: "'a set"
  assumes "finite_dimensional_real_vector_space_pair_1_on S1 S2 basis"
instantiation
  proj_space :: (euclidean_space) topological_space
  open_proj_space == open :: 'a proj_space set \<Rightarrow> bool
locale finite_dimensional_real_vector_space_pair_on
  fixes S1 :: "'a set"
    and S2 :: "'b set"
    and Basis1 :: "'a set"
    and Basis2 :: "'b set"
  assumes "finite_dimensional_real_vector_space_pair_on S1 S2 Basis1 Basis2"
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### Ignoring duplicate rewrite rule:
### frechet_derivative (\<lambda>x. ?c1) (at ?a1) \<equiv> \<lambda>x. 0::?'b1
### theory "Smooth_Manifolds.Projective_Space"
### 2.176s elapsed time, 8.616s cpu time, 0.464s GC time
### Ignoring duplicate rewrite rule:
### open {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed UNIV \<equiv> True
### Ignoring duplicate rewrite rule:
### closed ?S1 \<Longrightarrow> closed (insert ?a1 ?S1) \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {..<?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..<?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {..?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous bot ?f1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \<noteq> (0::?'b1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x / ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \<noteq> 1;
###  0 < ?g1 ?a1\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. log (?f1 x) (?g1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \<noteq> 0\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x powr ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; cos (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. tan (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; sin (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. cot (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 ?g1 \<Longrightarrow>
### continuous ?F1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 ?g1 \<Longrightarrow>
### continuous_on ?s1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### open {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed UNIV \<equiv> True
### Ignoring duplicate rewrite rule:
### closed ?S1 \<Longrightarrow> closed (insert ?a1 ?S1) \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {..<?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..<?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {..?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous bot ?f1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \<noteq> (0::?'b1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x / ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \<noteq> 1;
###  0 < ?g1 ?a1\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. log (?f1 x) (?g1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \<noteq> 0\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x powr ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; cos (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. tan (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; sin (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. cot (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 ?g1 \<Longrightarrow>
### continuous ?F1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 ?g1 \<Longrightarrow>
### continuous_on ?s1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 (\<lambda>x. x) \<equiv> True
locale diff
  fixes k :: "enat"
    and charts1 :: "('a, 'e) chart set"
    and charts2 :: "('b, 'f) chart set"
    and f :: "'a \<Rightarrow> 'b"
  assumes "diff k charts1 charts2 f"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### ((\<lambda>x. x) \<longlongrightarrow> ?a1) (at ?a1 within ?s1) \<equiv>
### True
### Ignoring duplicate rewrite rule:
### ((\<lambda>x. ?k1) \<longlongrightarrow> ?k1) ?F1 \<equiv> True
### Ignoring duplicate rewrite rule:
### (?f1 \<longlongrightarrow> ?x1) ?F1 \<Longrightarrow>
### ((\<lambda>x. ereal (?f1 x)) \<longlongrightarrow> ereal ?x1) ?F1 \<equiv>
### True
### Ignoring duplicate rewrite rule:
### (?f1 \<longlongrightarrow> ?x1) ?F1 \<Longrightarrow>
### ((\<lambda>x. - ?f1 x) \<longlongrightarrow> - ?x1) ?F1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>\<bar>?c1\<bar> \<noteq> \<infinity>;
###  (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?c1 * ?f1 x) \<longlongrightarrow>
###                    ?c1 * ?x1)
###                    ?F1 \<equiv>
###                   True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<noteq> 0; (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?c1 * ?f1 x) \<longlongrightarrow>
###                    ?c1 * ?x1)
###                    ?F1 \<equiv>
###                   True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?y1 \<noteq> - \<infinity>; ?x1 \<noteq> - \<infinity>;
###  (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?f1 x + ?y1) \<longlongrightarrow>
###                    ?x1 + ?y1)
###                    ?F1 \<equiv>
###                   True
### Ignoring duplicate rewrite rule:
### \<lbrakk>\<bar>?y1\<bar> \<noteq> \<infinity>;
###  (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk>
### \<Longrightarrow> ((\<lambda>x. ?f1 x + ?y1) \<longlongrightarrow>
###                    ?x1 + ?y1)
###                    ?F1 \<equiv>
###                   True
### Ignoring duplicate rewrite rule:
### (?f1 \<longlongrightarrow> ?x1) ?F1 \<Longrightarrow>
### ((\<lambda>x. ennreal (?f1 x)) \<longlongrightarrow> ennreal ?x1)
###  ?F1 \<equiv>
### True
### Ignoring duplicate rewrite rule:
### (?f1 \<longlongrightarrow> ereal ?x1) ?net1 \<Longrightarrow>
### ((\<lambda>x. real_of_ereal (?f1 x)) \<longlongrightarrow> ?x1)
###  ?net1 \<equiv>
### True
### Ignoring duplicate introduction (intro)
### open {}
### Ignoring duplicate introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### real_polynomial_function (\<lambda>x. ?c)
### Rule already declared as introduction (intro)
### \<lbrakk>real_polynomial_function ?f; real_polynomial_function ?g\<rbrakk>
### \<Longrightarrow> real_polynomial_function (\<lambda>x. ?f x + ?g x)
### Rule already declared as introduction (intro)
### \<lbrakk>real_polynomial_function ?f; real_polynomial_function ?g\<rbrakk>
### \<Longrightarrow> real_polynomial_function (\<lambda>x. ?f x * ?g x)
### Rule already declared as introduction (intro)
### \<lbrakk>real_polynomial_function ?f; real_polynomial_function ?g\<rbrakk>
### \<Longrightarrow> real_polynomial_function (\<lambda>x. ?f x - ?g x)
### Ignoring duplicate introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### closed {}
### Ignoring duplicate introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Ignoring duplicate introduction (intro)
### closed UNIV
### Ignoring duplicate introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Ignoring duplicate introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Ignoring duplicate introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Ignoring duplicate introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Ignoring duplicate introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Ignoring duplicate introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### frechet_derivative (\<lambda>x. ?c1) (at ?a1) \<equiv> \<lambda>x. 0::?'b1
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
locale diffeomorphism
  fixes k :: "enat"
    and charts1 :: "('a, 'b) chart set"
    and charts2 :: "('c, 'd) chart set"
    and f :: "'a \<Rightarrow> 'c"
    and f' :: "'c \<Rightarrow> 'a"
  assumes "Differentiable_Manifold.diffeomorphism k charts1 charts2 f f'"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### ?y1 \<in> ball ?x1 ?e1 \<equiv> dist ?x1 ?y1 < ?e1
locale submanifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
    and S :: "'a set"
  assumes "submanifold charts k S"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open src.carrier
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open src.carrier
locale submanifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
    and S :: "'a set"
  assumes "submanifold charts k S"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### theory "Smooth_Manifolds.Tangent_Space"
### 5.677s elapsed time, 21.916s cpu time, 0.864s GC time
Loading theory "Smooth_Manifolds.Cotangent_Space"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
locale real_vector_space_pair_on
  fixes S :: "'a set"
    and T :: "'b set"
  assumes "real_vector_space_pair_on S T"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
locale real_vector_space_on
  fixes S :: "'a set"
  assumes "real_vector_space_on S"
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
locale diff
  fixes k :: "enat"
    and charts1 :: "('a, 'e) chart set"
    and charts2 :: "('b, 'f) chart set"
    and f :: "'a \<Rightarrow> 'b"
  assumes "diff k charts1 charts2 f"
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Introduced fixed type variable(s): 'b in "a__"
locale c_manifold
  fixes charts :: "('a, 'b) chart set"
    and k :: "enat"
  assumes "c_manifold charts k"
### theory "Smooth_Manifolds.Cotangent_Space"
### 2.723s elapsed time, 10.692s cpu time, 0.392s GC time
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### frechet_derivative (\<lambda>x. ?c1) (at ?a1) \<equiv> \<lambda>x. 0::?'b1
\<lbrakk>\<forall>x.
            x \<in> manifold_eucl.diff_fun_space k \<longrightarrow>
            X x \<in> UNIV;
 \<forall>x.
    x \<in> ?S \<longrightarrow>
    ?g x \<in> manifold_eucl.diff_fun_space k\<rbrakk>
\<Longrightarrow> X (\<lambda>x. \<Sum>i\<in>?S. ?g i x) =
                  (\<Sum>a\<in>?S. X (?g a))
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Smooth_Manifolds/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Smooth_Manifolds/document -o pdf -n document
*** Undefined fact: "sum_not_0" (line 434 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
*** At command "by" (line 434 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
*** Undefined fact: "sum_not_0" (line 429 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
*** At command "by" (line 429 of "$AFP/Smooth_Manifolds/Analysis_More.thy")