section ‹Library Additions›
theory Analysis_More
  imports "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
    "HOL-Library.Function_Algebras"
    "HOL-Types_To_Sets.Linear_Algebra_On"
begin


lemma openin_open_Int'[intro]:
  "open S ⟹ openin (top_of_set U) (S ∩ U)"
  by (auto simp: openin_open)

subsection ‹Parametricity rules for topology›

text ‹TODO: also check with theory ‹Transfer_Euclidean_Space_Vector› in AFP/ODE...›

context includes lifting_syntax begin

lemma Sigma_transfer[transfer_rule]:
  "(rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B)) Sigma Sigma"
  unfolding Sigma_def
  by transfer_prover

lemma filterlim_transfer[transfer_rule]:
  "((A ===> B) ===> rel_filter B ===> rel_filter A ===> (=)) filterlim filterlim"
  if [transfer_rule]: "bi_unique B"
  unfolding filterlim_iff
  by transfer_prover

lemma nhds_transfer[transfer_rule]:
  "(A ===> rel_filter A) nhds nhds"
  if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
  unfolding nhds_def
  by transfer_prover

lemma at_within_transfer[transfer_rule]:
  "(A ===> rel_set A ===> rel_filter A) at_within at_within"
  if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
  unfolding at_within_def
  by transfer_prover

lemma continuous_on_transfer[transfer_rule]:
  "(rel_set A ===> (A ===> B) ===> (=)) continuous_on continuous_on"
  if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
    "bi_unique B" "bi_total B" "(rel_set B ===> (=)) open open"
  unfolding continuous_on_def
  by transfer_prover

lemma continuous_on_transfer_right_total[transfer_rule]:
  "(rel_set A ===> (A ===> B) ===> (=)) (λX::'a::t2_space set. continuous_on (X ∩ Collect AP)) (λY::'b::t2_space set. continuous_on Y)"
  if DomainA: "Domainp A = AP"
    and [folded DomainA, transfer_rule]: "bi_unique A" "right_total A" "(rel_set A ===> (=)) (openin (top_of_set (Collect AP))) open"
    "bi_unique B" "bi_total B" "(rel_set B ===> (=)) open open"
  unfolding DomainA[symmetric]
proof (intro rel_funI)
  fix X Y f g
  assume H[transfer_rule]: "rel_set A X Y" "(A ===> B) f g"
  from H(1) have XA: "x ∈ X ⟹ Domainp A x" for x
    by (auto simp: rel_set_def)
  then have *: "X ∩ Collect (Domainp A) = X" by auto
  have "openin (top_of_set (Collect (Domainp A))) (Collect (Domainp A))" by auto
  show " continuous_on (X ∩ Collect (Domainp A)) f = continuous_on Y g"
    unfolding continuous_on_eq_continuous_within continuous_within_topological *
    apply transfer
    apply safe
    subgoal for x B
      apply (drule bspec, assumption, drule spec, drule mp, assumption, drule mp, assumption)
      apply clarsimp
      subgoal for AA
        apply (rule exI[where x="AA ∩ Collect (Domainp A)"])
        by (auto intro: XA)
      done
    subgoal using XA by (force simp: openin_subtopology)
    done
qed

lemma continuous_on_transfer_right_total2[transfer_rule]:
  "(rel_set A ===> (A ===> B) ===> (=)) (λX::'a::t2_space set. continuous_on X) (λY::'b::t2_space set. continuous_on Y)"
  if DomainB: "Domainp B = BP"
  and [folded DomainB, transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
    "bi_unique B" "right_total B" "(rel_set B ===> (=)) ((openin (top_of_set (Collect BP)))) open"
  unfolding DomainB[symmetric]
proof (intro rel_funI)
  fix X Y f g
  assume H[transfer_rule]: "rel_set A X Y" "(A ===> B) f g"
  show "continuous_on X f = continuous_on Y g"
    unfolding continuous_on_eq_continuous_within continuous_within_topological
    apply transfer
    apply safe
    subgoal for x C
      apply (clarsimp simp: openin_subtopology)
      apply (drule bspec, assumption, drule spec, drule mp, assumption, drule mp, assumption)
      apply clarsimp
      by (meson Domainp_applyI H(1) H(2) rel_setD1)
    subgoal for x C
    proof -
      let ?sub = "top_of_set (Collect (Domainp B))"
      assume cont: "∀x∈X. ∀Ba∈{A. Ball A (Domainp B)}.
          openin (top_of_set (Collect (Domainp B))) Ba ⟶ f x ∈ Ba ⟶ (∃Aa.  open Aa ∧ x ∈ Aa ∧ (∀y∈X. y ∈ Aa ⟶ f y ∈ Ba))"
        and x: "x ∈ X" "open C" "f x ∈ C"
      let ?B = "C ∩ Collect (Domainp B)"
      have "?B ∈ {A. Ball A (Domainp B)}" by auto
      have "openin ?sub (Collect (Domainp B))" by auto
      then have "openin ?sub ?B" using ‹open C› by auto
      moreover have "f x ∈ ?B" using x
        apply transfer apply auto
        by (meson Domainp_applyI H(1) H(2) rel_setD1)
      ultimately obtain D where "open D ∧ x ∈ D ∧ (∀y∈X. y ∈ D ⟶ f y ∈ ?B)"
        using cont x
        by blast
      then show "∃A. open A ∧ x ∈ A ∧ (∀y∈X. y ∈ A ⟶ f y ∈ C)" by auto
    qed
    done
qed


lemma generate_topology_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "right_total A" "bi_unique A"
  shows "(rel_set (rel_set A) ===> rel_set A ===> (=)) (generate_topology o (insert (Collect (Domainp A)))) generate_topology"
proof (intro rel_funI)
  fix B C X Y assume t[transfer_rule]: "rel_set (rel_set A) B C" "rel_set A X Y"
  then have "X ⊆ Collect (Domainp A)" by (auto simp: rel_set_def)
  with t have rI: "rel_set A (X ∩ Collect (Domainp A)) Y"
    by (auto simp: inf_absorb1)
  have eq_UNIV_I: "Z = UNIV" if [transfer_rule]: "rel_set A {a. Domainp A a} Z" for Z
    using that assms
    apply (auto simp: right_total_def rel_set_def)
    using bi_uniqueDr by fastforce
  show "(generate_topology ∘ insert (Collect (Domainp A))) B X = generate_topology C Y"
    unfolding o_def
  proof (rule iffI)
    fix x
    assume "generate_topology (insert (Collect (Domainp A)) B) X"
    then show "generate_topology C Y" unfolding o_def
      using rI
    proof (induction X arbitrary: Y)
      case [transfer_rule]: UNIV
      with eq_UNIV_I[of Y] show ?case
        by (simp add: generate_topology.UNIV)
    next
      case (Int a b)
      note [transfer_rule] = Int(5)
      obtain a' where a'[transfer_rule]: "rel_set A (a ∩ Collect (Domainp A)) a'"
        by (metis Domainp_iff Domainp_set Int_Collect)
      obtain b' where b'[transfer_rule]: "rel_set A (b ∩ Collect (Domainp A)) b'"
        by (metis Domainp_iff Domainp_set Int_Collect)
      from Int.IH(1)[OF a'] Int.IH(2)[OF b']
      have "generate_topology C a'" "generate_topology C b'" by auto
      from generate_topology.Int[OF this] have "generate_topology C (a' ∩ b')" .
      also have "a' ∩ b' = Y"
        by transfer auto
      finally show ?case
        by (simp add: generate_topology.Int)
    next
      case (UN K)
      note [transfer_rule] = UN(3)
      have "∃K'. ∀k. rel_set A (k ∩ Collect (Domainp A)) (K' k)"
        by (rule choice) (metis Domainp_iff Domainp_set Int_Collect)
      then obtain K' where K': "⋀k. rel_set A (k ∩ Collect (Domainp A)) (K' k)" by metis
      from UN.IH[OF _ this] have "generate_topology C k'" if "k' ∈ K'`K" for k' using that by auto
      from generate_topology.UN[OF this] have "generate_topology C (⋃(K' ` K))" .
      also
      from K' have [transfer_rule]: "(rel_set (=) ===> rel_set A) (λx. x ∩ Collect (Domainp A)) K'"
        by (fastforce simp: rel_fun_def rel_set_def)
      have "⋃(K' ` K) = Y"
        by transfer auto
      finally show ?case
        by (simp add: generate_topology.UN)
    next
      case (Basis s)
      from this(1) show ?case
      proof
        assume "s = Collect (Domainp A)" 
        with eq_UNIV_I[of Y] Basis(2)
        show ?case
          by (simp add: generate_topology.UNIV)
      next
        assume "s ∈ B"
        with Basis(2) obtain t where [transfer_rule]: "rel_set A (s ∩ Collect (Domainp A)) t" by auto
        from Basis(1) t(1) have s: "s ∩ Collect (Domainp A) = s"
          by (force simp: rel_set_def)
        have "t ∈ C" using ‹s ∈ B› s
          by transfer auto
        also note [transfer_rule] = Basis(2)
        have "t = Y"
          by transfer auto
        finally show ?case
          by (rule generate_topology.Basis)
      qed
    qed
  next
    assume "generate_topology C Y"
    then show "generate_topology (insert (Collect (Domainp A)) B) X"
      using ‹rel_set A X Y›
    proof (induction arbitrary: X)
      case [transfer_rule]: UNIV
      have "UNIV = (UNIV::'b set)" by auto
      then have "X = {a. Domainp A a}" by transfer
      then show ?case by (intro generate_topology.Basis) auto
    next
      case (Int a b)
      obtain a' b' where [transfer_rule]: "rel_set A a' a" "rel_set A b' b"
        by (meson assms(1) right_total_def right_total_rel_set)
      from generate_topology.Int[OF Int.IH(1)[OF this(1)] Int.IH(2)[OF this(2)]]
      have "generate_topology (insert {a. Domainp A a} B) (a' ∩ b')" by simp
      also
      define I where "I = a ∩ b"
      from ‹rel_set A X (a ∩ b)› have [transfer_rule]: "rel_set A X I" by (simp add: I_def)
      from I_def
      have "a' ∩ b' = X" by transfer simp
      finally show ?case .
    next
      case (UN K)
      have "∃K'. ∀k. rel_set A (K' k) k"
        by (rule choice) (meson assms(1) right_total_def right_total_rel_set)
      then obtain K' where K': "⋀k. rel_set A (K' k) k" by metis
      from UN.IH[OF _ this] have "generate_topology (insert {a. Domainp A a} B) k"
        if "k ∈ K'`K" for k using that by auto
      from generate_topology.UN[OF this]
      have "generate_topology (insert {a. Domainp A a} B) (⋃(K'`K))" by auto
      also
      from K' have [transfer_rule]: "(rel_set (=) ===> rel_set A) K' id"
        by (fastforce simp: rel_fun_def rel_set_def)
      define U where "U =  (⋃(id ` K))"
      from ‹rel_set A X _› have [transfer_rule]: "rel_set A X U" by (simp add: U_def)
      from U_def have "⋃(K' ` K) = X" by transfer simp
      finally show ?case .
    next
      case (Basis s)
      note [transfer_rule] = ‹rel_set A X s›
      from ‹s ∈ C› have "X ∈ B" by transfer
      then show ?case by (intro generate_topology.Basis) auto
    qed
  qed
qed

end


subsection ‹Miscellaneous›

lemmas [simp del] = mem_ball

lemma in_closureI[intro, simp]: "x ∈ X ⟹ x ∈ closure X"
  using closure_subset by auto

lemmas open_continuous_vimage = continuous_on_open_vimage[THEN iffD1, rule_format]
lemma open_continuous_vimage': "open s ⟹ continuous_on s f ⟹ open B ⟹ open (s ∩ f -` B)"
  using open_continuous_vimage[of s f B] by (auto simp: Int_commute)

lemma support_on_mono: "support_on carrier f ⊆ support_on carrier g"
  if "⋀x. x ∈ carrier ⟹ f x ≠ 0 ⟹ g x ≠ 0"
  using that
  by (auto simp: support_on_def)


lemma image_prod: "(λ(x, y). (f x, g y)) ` (A × B) = f ` A × g ` B" by auto


subsection ‹Closed support›

definition "csupport_on X S = closure (support_on X S)"

lemma closed_csupport_on[intro, simp]: "closed (csupport_on carrier φ)"
  by (auto simp: csupport_on_def)

lemma not_in_csupportD: "x ∉ csupport_on carrier φ ⟹ x ∈ carrier ⟹ φ x = 0"
  by (auto simp: csupport_on_def support_on_def)

lemma csupport_on_mono: "csupport_on carrier f ⊆ csupport_on carrier g"
  if "⋀x. x ∈ carrier ⟹ f x ≠ 0 ⟹ g x ≠ 0"
  unfolding csupport_on_def
  apply (rule closure_mono)
  using that
  by (rule support_on_mono)

subsection ‹Homeomorphism›

lemma homeomorphism_empty[simp]:
  "homeomorphism {} t f f' ⟷ t = {}"
  "homeomorphism s {} f f' ⟷ s = {}"
  by (auto simp: homeomorphism_def)

lemma homeomorphism_add:
  "homeomorphism UNIV UNIV (λx. x + c) (λx. x - c)"
  for c::"_::real_normed_vector"
  unfolding homeomorphism_def
  by (auto simp: algebra_simps continuous_intros intro!: image_eqI[where x="x - c" for x])

lemma in_range_scaleR_iff: "x ∈ range ((*⇩R) c) ⟷ c = 0 ⟶ x = 0"
  for x::"_::real_vector"
  by (auto simp: intro!: image_eqI[where x="x /⇩R c"])

lemma homeomorphism_scaleR:
  "homeomorphism UNIV UNIV (λx. c *⇩R x::_::real_normed_vector) (λx. x /⇩R c)"
  if "c ≠ 0"
  using that
  unfolding homeomorphism_def
  by (auto simp: in_range_scaleR_iff algebra_simps intro!: continuous_intros)


lemma homeomorphism_prod:
  "homeomorphism (a × b) (c × d) (λ(x, y). (f x, g y)) (λ(x, y). (f' x, g' y))"
  if "homeomorphism a c f f'"
     "homeomorphism b d g g'"
  using that by (simp add: homeomorphism_def image_prod)
    (auto simp add: split_beta intro!: continuous_intros elim: continuous_on_compose2)


subsection ‹Generalizations›

lemma openin_subtopology_eq_generate_topology:
  "openin (top_of_set S) x = generate_topology (insert S ((λB. B ∩ S) ` BB)) x"
  if open_gen: "open = generate_topology BB" and subset: "x ⊆ S"
proof -
  have "generate_topology (insert S ((λB. B ∩ S) ` BB)) (T ∩ S)"
    if "generate_topology BB T"
    for T
    using that
  proof (induction)
    case UNIV
    then show ?case by (auto intro!: generate_topology.Basis)
  next
    case (Int a b)
    have "generate_topology (insert S ((λB. B ∩ S) ` BB)) (a ∩ S ∩ (b ∩ S))"
      by (rule generate_topology.Int) (use Int in auto)
    then show ?case by (simp add: ac_simps)
  next
    case (UN K)
    then have "generate_topology (insert S ((λB. B ∩ S) ` BB)) (⋃k∈K. k ∩ S)"
      by (intro generate_topology.UN) auto
    then show ?case by simp
  next
    case (Basis s)
    then show ?case
      by (intro generate_topology.Basis) auto
  qed
  moreover
  have "∃T. generate_topology BB T ∧ x = T ∩ S"
    if "generate_topology (insert S ((λB. B ∩ S) ` BB)) x" "x ≠ UNIV"
    using that
  proof (induction)
    case UNIV
    then show ?case by simp
  next
    case (Int a b)
    then show ?case
      using generate_topology.Int 
      by auto
  next
    case (UN K)
    from UN.IH have "∀k∈K-{UNIV}. ∃T. generate_topology BB T ∧ k = T ∩ S" by auto
    from this[THEN bchoice] obtain T where T: "⋀k. k ∈ T ` (K - {UNIV}) ⟹ generate_topology BB k" "⋀k. k ∈ K - {UNIV} ⟹ k = (T k) ∩ S"
      by auto
    from generate_topology.UN[OF T(1)]
    have "generate_topology BB (⋃(T ` (K - {UNIV})))" by auto
    moreover have "⋃K = (⋃(T ` (K - {UNIV}))) ∩ S" if "UNIV ∉ K" using T(2) UN that by auto
    ultimately show ?case
      apply (cases "UNIV ∈ K") subgoal using UN by auto
      subgoal by auto
      done
  next
    case (Basis s)
    then show ?case
      using generate_topology.UNIV generate_topology.Basis by blast
  qed
  moreover
  have "∃T. generate_topology BB T ∧ UNIV = T ∩ S" if "generate_topology (insert S ((λB. B ∩ S) ` BB)) x"
     "x = UNIV"
  proof -
    have "S = UNIV"
      using that ‹x ⊆ S›
      by auto
    then show ?thesis by (simp add: generate_topology.UNIV)
  qed
  ultimately show ?thesis
    by (metis open_gen open_openin openin_open_Int' openin_subtopology)
qed

subsection ‹Equal topologies›

lemma topology_eq_iff: "t = s ⟷ (topspace t = topspace s ∧
  (∀x⊆topspace t. openin t x = openin s x))"
  by (metis (full_types) openin_subset topology_eq)


subsection ‹Finer topologies›

definition finer_than (infix "(finer'_than)" 50)
  where "T1 finer_than T2 ⟷ continuous_map T1 T2 (λx. x)"

lemma finer_than_iff_nhds:
  "T1 finer_than T2 ⟷ (∀X. openin T2 X ⟶ openin T1 (X ∩ topspace T1)) ∧ (topspace T1 ⊆ topspace T2)"
  by (auto simp: finer_than_def continuous_map_alt)

lemma continuous_on_finer_topo:
  "continuous_map s t f"
  if "continuous_map s' t f" "s finer_than s'"
  using that
  by (auto simp: finer_than_def o_def dest: continuous_map_compose)

lemma continuous_on_finer_topo2:
  "continuous_map s t f"
  if "continuous_map s t' f" "t' finer_than t"
  using that
  by (auto simp: finer_than_def o_def dest: continuous_map_compose)

lemma antisym_finer_than: "S = T" if "S finer_than T" "T finer_than S"
  using that
  apply (auto simp: finer_than_def topology_eq_iff continuous_map_alt)
  apply (metis inf.orderE)+
  done

lemma subtopology_finer_than[simp]: "top_of_set X finer_than euclidean"
  by (auto simp: finer_than_iff_nhds openin_subtopology)

subsection ‹Support›

lemma support_on_nonneg_sum:
  "support_on X (λx. ∑i∈S. f i x) = (⋃i∈S. support_on X (f i))"
  if "finite S" "⋀x i . x ∈ X ⟹ i ∈ S ⟹ f i x ≥ 0"
  for f::"_⇒_⇒_::ordered_comm_monoid_add"
  using that by (auto simp: support_on_def sum_nonneg_eq_0_iff)

lemma support_on_nonneg_sum_subset:
  "support_on X (λx. ∑i∈S. f i x) ⊆ (⋃i∈S. support_on X (f i))"
  for f::"_⇒_⇒_::ordered_comm_monoid_add"
by (cases "finite S") (auto simp: support_on_def, meson sum.neutral)

lemma support_on_nonneg_sum_subset':
  "support_on X (λx. ∑i∈S x. f i x) ⊆ (⋃x∈X. (⋃i∈S x. support_on X (f i)))"
  for f::"_⇒_⇒_::ordered_comm_monoid_add"
  by (auto simp: support_on_def, meson sum.neutral)

subsection ‹Final topology (Bourbaki, General Topology I, 4.)›

definition "final_topology X Y f =
  topology (λU. U ⊆ X ∧
    (∀i. openin (Y i) (f i -` U ∩ topspace (Y i))))"

lemma openin_final_topology:
  "openin (final_topology X Y f) =
    (λU. U ⊆ X ∧ (∀i. openin (Y i) (f i -` U ∩ topspace (Y i))))"
  unfolding final_topology_def
  apply (rule topology_inverse')
  unfolding istopology_def
proof safe
  fix S T i
  assume "∀i. openin (Y i) (f i -` S ∩ topspace (Y i))"
    "∀i. openin (Y i) (f i -` T ∩ topspace (Y i))"
  then have "openin (Y i) (f i -` S ∩ topspace (Y i) ∩ (f i -` T ∩ topspace (Y i)))"
    (is "openin _ ?I")
    by auto
  also have "?I = f i -` (S ∩ T) ∩ topspace (Y i)"
    (is "_ = ?R")
    by auto
  finally show "openin (Y i) ?R" .
next
  fix K i
  assume "∀U∈K. U ⊆ X ∧ (∀i. openin (Y i) (f i -` U ∩ topspace (Y i)))"
  then have "openin (Y i) (⋃X∈K. f i -` X ∩ topspace (Y i))"
    by (intro openin_Union) auto
  then show "openin (Y i) (f i -` ⋃K ∩ topspace (Y i))"
    by (auto simp: vimage_Union)
qed force+

lemma topspace_final_topology:
  "topspace (final_topology X Y f) = X"
  if "⋀i. f i ∈ topspace (Y i) → X"
proof -
  have *: "f i -` X ∩ topspace (Y i) = topspace (Y i)" for i
    using that
    by auto
  show ?thesis
    unfolding topspace_def
    unfolding openin_final_topology
    apply (rule antisym)
     apply force
    apply (rule subsetI)
    apply (rule UnionI[where X=X])
    using that
    by (auto simp: *)
qed

lemma continuous_on_final_topologyI2:
  "continuous_map (Y i) (final_topology X Y f) (f i)"
  if "⋀i. f i ∈ topspace (Y i) → X"
  using that
  by (auto simp: openin_final_topology continuous_map_alt topspace_final_topology)

lemma continuous_on_final_topologyI1:
  "continuous_map (final_topology X Y f) Z g"
  if hyp: "⋀i. continuous_map (Y i) Z (g o f i)"
    and that: "⋀i. f i ∈ topspace (Y i) → X" "g ∈ X → topspace Z"
  unfolding continuous_map_alt
proof safe
  fix V assume V: "openin Z V"
  have oV: "openin (Y i) (f i -` g -` V ∩ topspace (Y i))"
    for i
    using hyp[rule_format, of i] V
    by (auto simp: continuous_map_alt vimage_comp dest!: spec[where x=V])
  have *: "f i -` g -` V ∩ f i -` X ∩ topspace (Y i) =
      f i -` g -` V ∩ topspace (Y i)"
    (is "_ = ?rhs i")
    for i using that
    by auto
  show "openin (final_topology X Y f) (g -` V ∩ topspace (final_topology X Y f))"
    by (auto simp: openin_final_topology oV topspace_final_topology that *)
qed (use that in ‹auto simp: topspace_final_topology›)


lemma continuous_on_final_topology_iff:
  "continuous_map (final_topology X Y f) Z g ⟷ (∀i. continuous_map (Y i) Z (g o f i))"
  if "⋀i. f i ∈ topspace (Y i) → X" "g ∈ X → topspace Z"
  using that
  by (auto intro!: continuous_on_final_topologyI1[OF _ that]
      intro: continuous_map_compose[OF continuous_on_final_topologyI2[OF that(1)]])


subsection ‹Quotient topology›

definition map_topology :: "('a ⇒ 'b) ⇒ 'a topology ⇒ 'b topology" where
  "map_topology p X = final_topology (p ` topspace X) (λ_. X) (λ(_::unit). p)"

lemma openin_map_topology:
  "openin (map_topology p X) = (λU. U ⊆ p ` topspace X ∧ openin X (p -` U ∩ topspace X))"
  by (auto simp: map_topology_def openin_final_topology)

lemma topspace_map_topology[simp]: "topspace (map_topology f T) = f ` topspace T"
  unfolding map_topology_def
  by (subst topspace_final_topology) auto

lemma continuous_on_map_topology:
  "continuous_map T (map_topology f T) f"
  unfolding continuous_map_alt openin_map_topology
  by auto

lemma continuous_map_composeD:
  "continuous_map T X (g ∘ f) ⟹ g ∈ f ` topspace T → topspace X"
  by (auto simp: continuous_map_def)

lemma continuous_on_map_topology2:
  "continuous_map T X (g ∘ f) ⟷ continuous_map (map_topology f T) X g"
  unfolding map_topology_def
  apply safe
  subgoal
    apply (rule continuous_on_final_topologyI1)
    subgoal by assumption
    subgoal by force
    subgoal by (rule continuous_map_composeD)
    done
  subgoal
    apply (erule continuous_map_compose[rotated])
    apply (rule continuous_on_final_topologyI2)
    by force
  done

lemma map_sub_finer_than_commute:
  "map_topology f (subtopology T (f -` X)) finer_than subtopology (map_topology f T) X"
  by (auto simp: finer_than_def continuous_map_def openin_subtopology openin_map_topology
      topspace_subtopology)

lemma sub_map_finer_than_commute:
  "subtopology (map_topology f T) X finer_than map_topology f (subtopology T (f -` X))"
  if "openin T (f -` X)"― ‹this is more or less the condition from
    🌐‹https://math.stackexchange.com/questions/705840/quotient-topology-vs-subspace-topology››
  unfolding finer_than_def continuous_map_alt
proof (rule conjI, clarsimp)
  fix U
  assume "openin (map_topology f (subtopology T (f -` X))) U"
  then obtain W where W: "U ⊆ f ` (topspace T ∩ f -` X)" "openin T W" "f -` U ∩ (topspace T ∩ f -` X) = W ∩ f -` X"
    by (auto simp: topspace_subtopology openin_subtopology openin_map_topology)
  have "(f -` f ` W ∩ f -` X) ∩ topspace T = W ∩ topspace T ∩ f -` X"
    apply auto
    by (metis Int_iff W(3) vimage_eq)
  also have "openin T …"
    by (auto intro!: W that)
  finally show "openin (subtopology (map_topology f T) X) (U ∩ (f ` topspace T ∩ X))"
    using W
    unfolding topspace_subtopology topspace_map_topology openin_subtopology openin_map_topology
    by (intro exI[where x="(f ` W ∩ X)"]) auto
qed auto

lemma subtopology_map_topology:
  "subtopology (map_topology f T) X = map_topology f (subtopology T (f -` X))"
  if "openin T (f -` X)"
  apply (rule antisym_finer_than)
  using sub_map_finer_than_commute[OF that] map_sub_finer_than_commute[of f T X]
  by auto

lemma quotient_map_map_topology:
  "quotient_map X (map_topology f X) f"
  by (auto simp: quotient_map_def openin_map_topology ac_simps)
    (simp_all add: vimage_def Int_def)

lemma topological_space_quotient: "class.topological_space (openin (map_topology f euclidean))"
  if "surj f"
  apply standard
    apply (auto simp: )
  using that
  by (auto simp: openin_map_topology)

lemma t2_space_quotient: "class.t2_space (open::'b set ⇒ bool)"
  if open_def: "open = (openin (map_topology (p::'a::t2_space⇒'b::topological_space) euclidean))"
    "surj p" and open_p: "⋀X. open X ⟹ open (p ` X)" and "closed {(x, y). p x = p y}" (is "closed ?R")
  apply (rule class.t2_space.intro)
  subgoal by (unfold open_def, rule topological_space_quotient; fact)
proof standard
  fix a b::'b
  obtain x y where a_def: "a = p x" and b_def: "b = p y" using ‹surj p› by fastforce
  assume "a ≠ b"
  with ‹closed ?R› have "open (-?R)" "(x, y) ∈ -?R" by (auto simp add: a_def b_def)
  from open_prod_elim[OF this]
  obtain N⇩x N⇩y where "open N⇩x" "open N⇩y" "(x, y) ∈ N⇩x × N⇩y" "N⇩x × N⇩y ⊆ -?R" .
  then have "p ` N⇩x ∩ p ` N⇩y = {}" by auto
  moreover
  from ‹open N⇩x› ‹open N⇩y› have "open (p ` N⇩x)" "open (p ` N⇩y)"
    using open_p by blast+
  moreover have "a ∈ p ` N⇩x" "b ∈ p ` N⇩y" using ‹(x, y) ∈ _ × _› by (auto simp: a_def b_def)
  ultimately show "∃U V. open U ∧ open V ∧ a ∈ U ∧ b ∈ V ∧ U ∩ V = {}" by blast
qed

lemma second_countable_topology_quotient: "class.second_countable_topology (open::'b set ⇒ bool)"
  if open_def: "open = (openin (map_topology (p::'a::second_countable_topology⇒'b::topological_space) euclidean))"
    "surj p" and open_p: "⋀X. open X ⟹ open (p ` X)"
  apply (rule class.second_countable_topology.intro)
  subgoal by (unfold open_def, rule topological_space_quotient; fact)
proof standard
  have euclidean_def: "euclidean = map_topology p euclidean"
    by (simp add: openin_inverse open_def)
  have continuous_on: "continuous_on UNIV p"
    using continuous_map_iff_continuous2 continuous_on_map_topology euclidean_def by fastforce
  from ex_countable_basis[where 'a='a] obtain A::"'a set set" where "countable A" "topological_basis A"
    by auto
  define B where "B = (λX. p ` X) ` A"
  have "countable (B::'b set set)"
    by (auto simp: B_def intro!: ‹countable A›)
  moreover have "topological_basis B"
  proof (rule topological_basisI)
    fix B' assume "B' ∈ B" then show "open B'" using ‹topological_basis A›
      by (auto simp: B_def topological_basis_open intro!: open_p)
  next
    fix x::'b and O' assume "open O'" "x ∈ O'"
    have "open (p -` O')"
      using ‹open O'›
      by (rule open_vimage) (auto simp: continuous_on)
    obtain y where y: "y ∈ p -` {x}"
      using ‹x ∈ O'›
      by auto (metis UNIV_I open_def(2) rangeE)
    then have "y ∈ p -` O'" using ‹x ∈ O'› by auto
    from topological_basisE[OF ‹topological_basis A› ‹open (p -` O')› this]
    obtain C where "C ∈ A" "y ∈ C" "C ⊆ p -` O'" .
    let ?B' = "p ` C"
    have "?B' ∈ B"
      using ‹C ∈ A› by (auto simp: B_def)
    moreover
    have "x ∈ ?B'" using y ‹y ∈ C› ‹x ∈ O'›
      by auto
    moreover
    have "?B' ⊆ O'"
      using ‹C ⊆ _› by auto
    ultimately show "∃B'∈B. x ∈ B' ∧ B' ⊆ O'" by metis
  qed
  ultimately show "∃B::'b set set. countable B ∧ open = generate_topology B"
    by (auto simp: topological_basis_imp_subbasis)
qed


subsection ‹Closure›

lemma closure_Union: "closure (⋃X) = (⋃x∈X. closure x)" if "finite X"
  using that
  by (induction X) auto

subsection ‹Compactness›

lemma compact_if_closed_subset_of_compact:
  "compact S" if "closed S" "compact T" "S ⊆ T"
proof (rule compactI)
  fix UU assume UU: "∀t∈UU. open t" "S ⊆ ⋃UU"
  have "T ⊆ ⋃(insert (- S) (UU))" "⋀B. B ∈ insert (- S) UU ⟹ open B"
    using UU ‹S ⊆ T›
    by (auto simp: open_Compl ‹closed S›)
  from compactE[OF ‹compact T› this]
  obtain 𝒯' where 𝒯: "𝒯' ⊆ insert (- S) UU" "finite 𝒯'" "T ⊆ ⋃𝒯'"
    by metis
  show "∃C'⊆UU. finite C' ∧ S ⊆ ⋃C'"
    apply (rule exI[where x="𝒯' - {-S}"])
    using 𝒯 UU
    apply auto
  proof -
    fix x assume "x ∈ S"
    with 𝒯 ‹S ⊆ T› obtain U where "x ∈ U" "U ∈ 𝒯'" using 𝒯
      by auto
    then show "∃X∈𝒯' - {- S}. x ∈ X"
      using 𝒯 UU ‹x ∈ S›
      apply -
      apply (rule bexI[where x=U])
      by auto
  qed
qed

subsection ‹Locally finite›

definition "locally_finite_on X I U ⟷ (∀p∈X. ∃N. p∈N ∧ open N ∧ finite {i∈I. U i ∩ N ≠ {}})"

lemmas locally_finite_onI = locally_finite_on_def[THEN iffD2, rule_format]

lemma locally_finite_onE:
  assumes "locally_finite_on X I U"
  assumes "p ∈ X"
  obtains N where "p ∈ N" "open N" "finite {i∈I. U i ∩ N ≠ {}}"
  using assms
  by (auto simp: locally_finite_on_def)

lemma locally_finite_onD:
  assumes "locally_finite_on X I U"
  assumes "p ∈ X"
  shows "finite {i∈I. p ∈ U i}"
  apply (rule locally_finite_onE[OF assms])
  apply (rule finite_subset)
  by auto

lemma locally_finite_on_open_coverI: "locally_finite_on X I U"
  if fin: "⋀j. j ∈ I ⟹ finite {i∈I. U i ∩ U j ≠ {}}"
    and open_cover: "X ⊆ (⋃i∈I. U i)" "⋀i. i ∈ I ⟹ open (U i)"
proof (rule locally_finite_onI)
  fix p assume "p ∈ X"
  then obtain i where i: "i ∈ I" "p ∈ U i" "open (U i)"
    using open_cover
    by blast
  show "∃N. p ∈ N ∧ open N ∧ finite {i ∈ I. U i ∩ N ≠ {}}"
    by (intro exI[where x="U i"] conjI i fin)
qed

lemma locally_finite_compactD:
  "finite {i∈I. U i ∩ V ≠ {}}"
  if lf: "locally_finite_on X I U"
    and compact: "compact V"
    and subset: "V ⊆ X"
proof -
  have "∃N. ∀p ∈ X. p ∈ N p ∧ open (N p) ∧ finite {i∈I. U i ∩ N p ≠ {}}"
    by (rule bchoice) (auto elim!: locally_finite_onE[OF lf, rule_format])
  then obtain N where N: "⋀p. p ∈ X ⟹ p ∈ N p"
    "⋀p. p ∈ X ⟹ open (N p)"
    "⋀p. p ∈ X ⟹ finite {i∈I. U i ∩ N p ≠ {}}"
    by blast
  have "V ⊆ (⋃p∈X. N p)" "⋀B. B ∈ N ` X ⟹ open B"
    using N subset by force+
  from compactE[OF compact this]
  obtain C where C: "C ⊆ X" "finite C" "V ⊆ ⋃(N ` C)"
    by (metis finite_subset_image)
  then have "{i∈I. U i ∩ V ≠ {}} ⊆ {i∈I. U i ∩ ⋃(N ` C) ≠ {}}"
    by force
  also have "… ⊆ (⋃c∈C. {i∈I. U i ∩ N c ≠ {}})"
    by force
  also have "finite …"
    apply (rule finite_Union)
    using C by (auto intro!: C N)
  finally (finite_subset) show ?thesis .
qed

lemma closure_Int_open_eq_empty: "open S ⟹ (closure T ∩ S) = {} ⟷ T ∩ S = {}"
  by (auto simp: open_Int_closure_eq_empty ac_simps)

lemma locally_finite_on_subset:
  assumes "locally_finite_on X J U"
  assumes "⋀i. i ∈ I ⟹ V i ⊆ U i" "I ⊆ J"
  shows "locally_finite_on X I V"
proof (rule locally_finite_onI)
  fix p assume "p ∈ X"
  from locally_finite_onE[OF assms(1) this]
  obtain N where "p ∈ N" "open N" "finite {i ∈ J. U i ∩ N ≠ {}}" .
  then show "∃N. p ∈ N ∧ open N ∧ finite {i ∈ I. V i ∩ N ≠ {}}"
    apply (intro exI[where x=N])
    using assms
    by (auto elim!: finite_subset[rotated])
qed

lemma locally_finite_on_closure:
  "locally_finite_on X I (λx. closure (U x))"
  if "locally_finite_on X I U"
proof (rule locally_finite_onI)
  fix p assume "p ∈ X"
  from locally_finite_onE[OF that this] obtain N
    where "p ∈ N" "open N" "finite {i ∈ I. U i ∩ N ≠ {}}" .
  then show "∃N. p ∈ N ∧ open N ∧ finite {i ∈ I. closure (U i) ∩ N ≠ {}}"
    by (auto intro!: exI[where x=N] simp: closure_Int_open_eq_empty)
qed


lemma locally_finite_on_closedin_Union_closure:
  "closedin (top_of_set X) (⋃i∈I. closure (U i))"
  if "locally_finite_on X I U" "⋀i. i ∈ I ⟹ closure (U i) ⊆ X"
  unfolding closedin_def
  apply safe
  subgoal using that(2) by auto
  subgoal
    apply (subst openin_subopen)
  proof clarsimp
    fix x
    assume x: "x ∈ X" "∀i∈I. x ∉ closure (U i)"
    from locally_finite_onE[OF that(1) ‹x ∈ X›]
    obtain N where N: "x ∈ N" "open N" "finite {i ∈ I. U i ∩ N ≠ {}}" (is "finite ?I").
    define N' where "N' = N - (⋃i ∈ ?I. closure (U i))"
    have "open N'"
      by (auto simp: N'_def intro!: N)
    then have "openin (top_of_set X) (X ∩ N')"
      by (rule openin_open_Int)
    moreover
    have "x ∈ X ∩ N'" using x
      by (auto simp: N'_def N)
    moreover
    have "X ∩ N' ⊆ X - (⋃i∈I. closure (U i))"
      using x that(2)
      apply (auto simp: N'_def)
      by (meson N(2) closure_iff_nhds_not_empty dual_order.refl)
    ultimately show "∃T. openin (top_of_set X) T ∧ x ∈ T ∧ T ⊆ X - (⋃i∈I. closure (U i))"
      by auto
  qed
  done

lemma closure_subtopology_minimal:
  "S ⊆ T ⟹ closedin (top_of_set X) T ⟹ closure S ∩ X ⊆ T"
  apply (auto simp: closedin_closed)
  using closure_minimal by blast

lemma locally_finite_on_closure_Union:
  "(⋃i∈I. closure (U i)) = closure (⋃i∈I. (U i)) ∩ X"
  if "locally_finite_on X I U" "⋀i. i ∈ I ⟹ closure (U i) ⊆ X"
proof (rule antisym)
  show "(⋃i∈I. closure (U i)) ⊆ closure (⋃i∈I. U i) ∩ X"
    using that
    apply auto
    by (metis (no_types, lifting) SUP_le_iff closed_closure closure_minimal closure_subset subsetCE)
  show "closure (⋃i∈I. U i) ∩ X ⊆ (⋃i∈I. closure (U i))"
    apply (rule closure_subtopology_minimal)
    apply auto
    using that
    by (auto intro!: locally_finite_on_closedin_Union_closure)
qed


subsection ‹Refinement of cover›

definition refines :: "'a set set ⇒ 'a set set ⇒ bool" (infix "refines" 50)
  where "A refines B ⟷ (∀s∈A. (∃t. t ∈ B ∧ s ⊆ t))"

lemma refines_subset: "x refines y" if "z refines y" "x ⊆ z"
  using that by (auto simp: refines_def)

subsection ‹Functions as vector space›

instantiation "fun" :: (type, scaleR) scaleR begin

definition scaleR_fun :: "real ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
  "scaleR_fun r f = (λx. r *⇩R f x)"

lemma scaleR_fun_beta[simp]: "(r *⇩R f) x = r *⇩R f x"
  by (simp add: scaleR_fun_def)

instance ..

end

instance "fun" :: (type, real_vector) real_vector
  by standard (auto simp: scaleR_fun_def algebra_simps)


subsection ‹Additional lemmas›

lemmas [simp del] = vimage_Un vimage_Int

lemma finite_Collect_imageI: "finite {U ∈ f ` X. P U}" if "finite {x∈X. P (f x)}"
proof -
  have "{d ∈ f ` X. P d} ⊆ f ` {c ∈ X. P (f c)}"
    by blast
  then show ?thesis
    using finite_surj that by blast
qed

lemma plus_compose: "(x + y) ∘ f = (x ∘ f) + (y ∘ f)"
  by auto

lemma mult_compose: "(x * y) ∘ f = (x ∘ f) * (y ∘ f)"
  by auto

lemma scaleR_compose: "(c *⇩R x) ∘ f = c *⇩R (x ∘ f)"
  by (auto simp:)

lemma image_scaleR_ball:
  fixes a :: "'a::real_normed_vector"
  shows "c ≠ 0 ⟹ (*⇩R) c ` ball a r = ball (c *⇩R a) (abs c *⇩R r)"
proof (auto simp: mem_ball dist_norm, goal_cases)
  case (1 b)
  have "norm (c *⇩R a - c *⇩R b)  = abs c * norm (a - b)"
    by (auto simp: norm_scaleR[symmetric] algebra_simps simp del: norm_scaleR)
  also have "… < abs c * r"
    apply (rule mult_strict_left_mono)
    using 1 by auto
  finally show ?case .
next
  case (2 x)
  have "norm (a - x /⇩R c) < r"
  proof -
    have "norm (a - x /⇩R c) = abs c *⇩R norm (a - x /⇩R c) /⇩R abs c"
      using 2 by auto
    also have "abs c *⇩R norm (a - x /⇩R c) = norm (c *⇩R a - x)"
      using 2
      by (auto simp: norm_scaleR[symmetric] algebra_simps simp del: norm_scaleR)
    also have "… < ¦c¦ * r"
      by fact
    also have "¦c¦ * r /⇩R ¦c¦ = r" using 2 by auto
    finally show ?thesis using 2 by auto
  qed
  then have xdc: "x /⇩R c ∈ ball a r"
    by (auto simp: mem_ball dist_norm)
  show ?case
    apply (rule image_eqI[OF _ xdc])
    using 2 by simp
qed


subsection ‹Continuity›

lemma continuous_within_topologicalE:
  assumes "continuous (at x within s) f"
    "open B" "f x ∈ B"
  obtains A where "open A" "x ∈ A" "⋀y. y ∈ s ⟹ y ∈ A ⟹ f y ∈ B"
  using assms continuous_within_topological by metis

lemma continuous_within_topologicalE':
  assumes "continuous (at x) f"
    "open B" "f x ∈ B"
  obtains A where "open A" "x ∈ A" "f ` A ⊆ B"
  using assms continuous_within_topologicalE[OF assms]
  by (metis UNIV_I image_subsetI)

lemma continuous_on_inverse: "continuous_on S f ⟹ 0 ∉ f ` S ⟹ continuous_on S (λx. inverse (f x))"
  for f::"_⇒_::real_normed_div_algebra"
  by (auto simp: continuous_on_def intro!: tendsto_inverse)


subsection ‹@{term "(has_derivative)"}›

lemma has_derivative_plus_fun[derivative_intros]:
  "(x + y has_derivative x' + y') (at a within A)"
  if [derivative_intros]:
    "(x has_derivative x') (at a within A)"
    "(y has_derivative y') (at a within A)"
  by (auto simp: plus_fun_def intro!: derivative_eq_intros)

lemma has_derivative_scaleR_fun[derivative_intros]:
  "(x *⇩R y has_derivative x *⇩R y') (at a within A)"
  if [derivative_intros]:
    "(y has_derivative y') (at a within A)"
  by (auto simp: scaleR_fun_def intro!: derivative_eq_intros)

lemma has_derivative_times_fun[derivative_intros]:
  "(x * y has_derivative (λh. x a * y' h + x' h * y a)) (at a within A)"
  if [derivative_intros]:
    "(x has_derivative x') (at a within A)"
    "(y has_derivative y') (at a within A)"
  for x y::"_⇒'a::real_normed_algebra"
  by (auto simp: times_fun_def intro!: derivative_eq_intros)

lemma real_sqrt_has_derivative_generic:
  "x ≠ 0 ⟹ (sqrt has_derivative (*) ((if x > 0 then 1 else -1) * inverse (sqrt x) / 2)) (at x within S)"
  apply (rule has_derivative_at_withinI)
  using DERIV_real_sqrt_generic[of x "(if x > 0 then 1 else -1) * inverse (sqrt x) / 2"] at_within_open[of x "UNIV - {0}"]
  by (auto simp: has_field_derivative_def open_delete ac_simps split: if_splits)

lemma sqrt_has_derivative:
  "((λx. sqrt (f x)) has_derivative (λxa. (if 0 < f x then 1 else - 1) / (2 * sqrt (f x)) * f' xa)) (at x within S)"
  if "(f has_derivative f') (at x within S)" "f x ≠ 0"
  by (rule has_derivative_eq_rhs[OF has_derivative_compose[OF that(1) real_sqrt_has_derivative_generic, OF that(2)]])
    (auto simp: divide_simps)

lemmas has_derivative_norm_compose[derivative_intros] = has_derivative_compose[OF _ has_derivative_norm]

subsection ‹Differentiable›

lemmas differentiable_on_empty[simp]

lemma differentiable_transform_eventually: "f differentiable (at x within X)"
  if "g differentiable (at x within X)"
    "f x = g x"
    "∀⇩F x in (at x within X). f x = g x"
  using that
  apply (auto simp: differentiable_def)
  subgoal for D
    apply (rule exI[where x=D])
    apply (auto simp: has_derivative_within)
    by (simp add: eventually_mono Lim_transform_eventually)
  done

lemma differentiable_within_eqI: "f differentiable at x within X"
  if "g differentiable at x within X" "⋀x. x ∈ X ⟹ f x = g x"
    "x ∈ X" "open X"
  apply (rule differentiable_transform_eventually)
    apply (rule that)
   apply (auto simp: that)
proof -
  have "∀⇩F x in at x within X. x ∈ X"
    using ‹open X›
    using eventually_at_topological by blast
  then show " ∀⇩F x in at x within X. f x = g x"
    by eventually_elim (auto simp: that)
qed

lemma differentiable_eqI: "f differentiable at x"
  if "g differentiable at x" "⋀x. x ∈ X ⟹ f x = g x" "x ∈ X" "open X"
  using that
  unfolding at_within_open[OF that(3,4), symmetric]
  by (rule differentiable_within_eqI)

lemma differentiable_on_eqI:
  "f differentiable_on S"
  if "g differentiable_on S" "⋀x. x ∈ S ⟹ f x = g x" "open S"
  using that differentiable_eqI[of g _ S f]
  by (auto simp: differentiable_on_eq_differentiable_at)

lemma differentiable_on_comp: "(f o g) differentiable_on S"
  if "g differentiable_on S" "f differentiable_on (g ` S)"
  using that
  by (auto simp: differentiable_on_def intro: differentiable_chain_within)

lemma differentiable_on_comp2: "(f o g) differentiable_on S"
  if  "f differentiable_on T" "g differentiable_on S" "g ` S ⊆ T"
  apply (rule differentiable_on_comp)
   apply (rule that)
  apply (rule differentiable_on_subset)
  apply (rule that)
  apply (rule that)
  done

lemmas differentiable_on_compose2 = differentiable_on_comp2[unfolded o_def]

lemma differentiable_on_openD: "f differentiable at x"
  if "f differentiable_on X" "open X" "x ∈ X"
  using differentiable_on_eq_differentiable_at that by blast

lemma differentiable_on_add_fun[intro, simp]:
  "x differentiable_on UNIV ⟹ y differentiable_on UNIV ⟹ x + y differentiable_on UNIV"
  by (auto simp: plus_fun_def)

lemma differentiable_on_mult_fun[intro, simp]:
  "x differentiable_on UNIV ⟹ y differentiable_on UNIV ⟹ x * y differentiable_on UNIV"
  for x y::"_⇒'a::real_normed_algebra"
  by (auto simp: times_fun_def)

lemma differentiable_on_scaleR_fun[intro, simp]:
  "y differentiable_on UNIV ⟹ x *⇩R y differentiable_on UNIV"
  by (auto simp: scaleR_fun_def)

lemma sqrt_differentiable:
  "(λx. sqrt (f x)) differentiable (at x within S)"
  if "f differentiable (at x within S)" "f x ≠ 0"
  using that
  using sqrt_has_derivative[of f _ x S]
  by (auto simp: differentiable_def)

lemma sqrt_differentiable_on: "(λx. sqrt (f x)) differentiable_on S"
  if "f differentiable_on S" "0 ∉ f ` S"
  using sqrt_differentiable[of f _ S] that
  by (force simp: differentiable_on_def)

lemma differentiable_on_inverse: "f differentiable_on S ⟹ 0 ∉ f ` S ⟹ (λx. inverse (f x)) differentiable_on S"
  for f::"_⇒_::real_normed_field"
  by (auto simp: differentiable_on_def intro!: differentiable_inverse)

lemma differentiable_on_openI:
  "f differentiable_on S"
  if "open S" "⋀x. x ∈ S ⟹ ∃f'. (f has_derivative f') (at x)"
  using that
  by (auto simp: differentiable_on_def at_within_open[where S=S] differentiable_def)

lemmas differentiable_norm_compose_at = differentiable_compose[OF differentiable_norm_at]

lemma differentiable_on_Pair:
  "f differentiable_on S ⟹ g differentiable_on S ⟹ (λx. (f x, g x)) differentiable_on S"
  unfolding differentiable_on_def
  using differentiable_Pair[of f _ S g] by auto

lemma differentiable_at_fst:
  "(λx. fst (f x)) differentiable at x within X" if "f differentiable at x within X"
  using that
  by (auto simp: differentiable_def dest!: has_derivative_fst)

lemma differentiable_at_snd:
  "(λx. snd (f x)) differentiable at x within X" if "f differentiable at x within X"
  using that
  by (auto simp: differentiable_def dest!: has_derivative_snd)

lemmas frechet_derivative_worksI = frechet_derivative_works[THEN iffD1]

lemma sin_differentiable_at: "(λx. sin (f x::real)) differentiable at x within X"
  if "f differentiable at x within X"
  using differentiable_def has_derivative_sin that by blast

lemma cos_differentiable_at: "(λx. cos (f x::real)) differentiable at x within X"
  if "f differentiable at x within X"
  using differentiable_def has_derivative_cos that by blast


subsection ‹Frechet derivative›

lemmas frechet_derivative_transform_within_open_ext =
  fun_cong[OF frechet_derivative_transform_within_open]

lemmas frechet_derivative_at' = frechet_derivative_at[symmetric]

lemma frechet_derivative_plus_fun:
  "x differentiable at a ⟹ y differentiable at a ⟹
  frechet_derivative (x + y) (at a) =
    frechet_derivative x (at a) + frechet_derivative y (at a)"
  by (rule frechet_derivative_at')
    (auto intro!: derivative_eq_intros frechet_derivative_worksI)

lemmas frechet_derivative_plus = frechet_derivative_plus_fun[unfolded plus_fun_def]

lemma frechet_derivative_zero_fun: "frechet_derivative 0 (at a) = 0"
  by (auto simp: frechet_derivative_const zero_fun_def)

lemma frechet_derivative_sin:
  "frechet_derivative (λx. sin (f x)) (at x) = (λxa. frechet_derivative f (at x) xa * cos (f x))"
  if "f differentiable (at x)"
  for f::"_⇒real"
  by (rule frechet_derivative_at'[OF has_derivative_sin[OF frechet_derivative_worksI[OF that]]])

lemma frechet_derivative_cos:
  "frechet_derivative (λx. cos (f x)) (at x) = (λxa. frechet_derivative f (at x) xa * - sin (f x))"
  if "f differentiable (at x)"
  for f::"_⇒real"
  by (rule frechet_derivative_at'[OF has_derivative_cos[OF frechet_derivative_worksI[OF that]]])

lemma differentiable_sum_fun:
  "(⋀i. i ∈ I ⟹ (f i differentiable at a)) ⟹ sum f I differentiable at a"
  by (induction I rule: infinite_finite_induct) (auto simp: zero_fun_def plus_fun_def)

lemma frechet_derivative_sum_fun:
  "(⋀i. i ∈ I ⟹ (f i differentiable at a)) ⟹
  frechet_derivative (∑i∈I. f i) (at a) = (∑i∈I. frechet_derivative (f i) (at a))"
  by (induction I rule: infinite_finite_induct)
    (auto simp: frechet_derivative_zero_fun frechet_derivative_plus_fun differentiable_sum_fun)

lemma sum_fun_def: "(∑i∈I. f i) = (λx. ∑i∈I. f i x)"
  by (induction I rule: infinite_finite_induct) auto

lemmas frechet_derivative_sum = frechet_derivative_sum_fun[unfolded sum_fun_def]


lemma frechet_derivative_times_fun:
  "f differentiable at a ⟹ g differentiable at a ⟹
  frechet_derivative (f * g) (at a) =
  (λx. f a * frechet_derivative g (at a) x + frechet_derivative f (at a) x * g a)"
  for f g::"_⇒'a::real_normed_algebra"
  by (rule frechet_derivative_at') (auto intro!: derivative_eq_intros frechet_derivative_worksI)

lemmas frechet_derivative_times = frechet_derivative_times_fun[unfolded times_fun_def]

lemma frechet_derivative_scaleR_fun:
  "y differentiable at a ⟹
  frechet_derivative (x *⇩R y) (at a) =
    x *⇩R frechet_derivative y (at a)"
  by (rule frechet_derivative_at')
    (auto intro!: derivative_eq_intros frechet_derivative_worksI)

lemmas frechet_derivative_scaleR = frechet_derivative_scaleR_fun[unfolded scaleR_fun_def]

lemma frechet_derivative_compose:
  "frechet_derivative (f o g) (at x) = frechet_derivative (f) (at (g x)) o frechet_derivative g (at x)"
  if "g differentiable at x" "f differentiable at (g x)"
  by (meson diff_chain_at frechet_derivative_at' frechet_derivative_works that)

lemma frechet_derivative_compose_eucl:
  "frechet_derivative (f o g) (at x) =
    (λv. ∑i∈Basis. ((frechet_derivative g (at x) v) ∙ i) *⇩R frechet_derivative f (at (g x)) i)"
  (is "?l = ?r")
  if "g differentiable at x" "f differentiable at (g x)"
proof (rule ext)
  fix v
  interpret g: linear "frechet_derivative g (at x)"
    using that(1)
    by (rule linear_frechet_derivative)
  interpret f: linear "frechet_derivative f (at (g x))"
    using that(2)
    by (rule linear_frechet_derivative)
  have "frechet_derivative (f o g) (at x) v =
    frechet_derivative f (at (g x)) (∑i∈Basis. (frechet_derivative g (at x) v ∙ i) *⇩R i)"
    unfolding frechet_derivative_compose[OF that] o_apply
    by (simp add: euclidean_representation)
  also have "… = ?r v"
    by (auto simp: g.sum g.scaleR f.sum f.scaleR)
  finally show "?l v = ?r v" .
qed


lemma frechet_derivative_works_on_open:
  "f differentiable_on X ⟹ open X ⟹ x ∈ X ⟹
    (f has_derivative frechet_derivative f (at x)) (at x)"
  and frechet_derivative_works_on:
  "f differentiable_on X ⟹ x ∈ X ⟹
    (f has_derivative frechet_derivative f (at x within X)) (at x within X)"
  by (auto simp: differentiable_onD differentiable_on_openD frechet_derivative_worksI)

lemma frechet_derivative_inverse: "frechet_derivative (λx. inverse (f x)) (at x) =
    (λh. - 1 / (f x)⇧2 * frechet_derivative f (at x) h)"
  if "f differentiable at x" "f x ≠ 0" for f::"_⇒_::real_normed_field"
  apply (rule frechet_derivative_at')
  using that
  by (auto intro!: derivative_eq_intros frechet_derivative_worksI
      simp: divide_simps algebra_simps power2_eq_square)

lemma frechet_derivative_sqrt: "frechet_derivative (λx. sqrt (f x)) (at x) =
  (λv. (if f x > 0 then 1 else -1) / (2 * sqrt (f x)) * frechet_derivative f (at x) v)"
  if "f differentiable at x" "f x ≠ 0" 
  apply (rule frechet_derivative_at')
  apply (rule sqrt_has_derivative[THEN has_derivative_eq_rhs])
  by (auto intro!: frechet_derivative_worksI that simp: divide_simps)

lemma frechet_derivative_norm: "frechet_derivative (λx. norm (f x)) (at x) =
    (λv. frechet_derivative f (at x) v ∙ sgn (f x))"
  if "f differentiable at x" "f x ≠ 0" 
  for f::"_⇒_::real_inner"
  apply (rule frechet_derivative_at')
  by (auto intro!: derivative_eq_intros frechet_derivative_worksI that simp: divide_simps)

lemma (in bounded_linear) frechet_derivative:
  "frechet_derivative f (at x) = f"
  apply (rule frechet_derivative_at')
  apply (rule has_derivative_eq_rhs)
   apply (rule has_derivative)
  by (auto intro!: derivative_eq_intros)

bundle no_matrix_mult begin
no_notation matrix_matrix_mult (infixl "**" 70)
end

lemma (in bounded_bilinear) frechet_derivative:
  includes no_matrix_mult
  shows
    "x differentiable at a ⟹ y differentiable at a ⟹
      frechet_derivative (λa. x a ** y a) (at a) =
        (λh. x a ** frechet_derivative y (at a) h + frechet_derivative x (at a) h ** y a)"
  by (rule frechet_derivative_at') (auto intro!: FDERIV frechet_derivative_worksI)

lemma frechet_derivative_divide: "frechet_derivative (λx. f x / g x) (at x) =
    (λh. frechet_derivative f (at x) h / (g x) -frechet_derivative g (at x) h * f x / (g x)⇧2)"
  if "f differentiable at x" "g differentiable at x" "g x ≠ 0" for f::"_⇒_::real_normed_field"
  using that
  by (auto simp: divide_inverse_commute bounded_bilinear.frechet_derivative[OF bounded_bilinear_mult]
      frechet_derivative_inverse)

lemma frechet_derivative_pair:
  "frechet_derivative (λx. (f x, g x)) (at x) = (λv. (frechet_derivative f (at x) v, frechet_derivative g (at x) v))"
  if "f differentiable (at x)" "g differentiable (at x)"
  apply (rule frechet_derivative_at')
  apply (rule derivative_eq_intros)
    apply (rule frechet_derivative_worksI) apply fact    
    apply (rule frechet_derivative_worksI) apply fact
  ..

lemma frechet_derivative_fst:
  "frechet_derivative (λx. fst (f x)) (at x) = (λxa. fst (frechet_derivative f (at x) xa))"
  if "(f differentiable at x)"
  for f::"_⇒(_::real_normed_vector × _::real_normed_vector)"
  apply (rule frechet_derivative_at')
  using that
  by (auto intro!: derivative_eq_intros frechet_derivative_worksI)

lemma frechet_derivative_snd:
  "frechet_derivative (λx. snd (f x)) (at x) = (λxa. snd (frechet_derivative f (at x) xa))"
  if "(f differentiable at x)"
  for f::"_⇒(_::real_normed_vector × _::real_normed_vector)"
  apply (rule frechet_derivative_at')
  using that
  by (auto intro!: derivative_eq_intros frechet_derivative_worksI)

lemma frechet_derivative_eq_vector_derivative_1:
  assumes "f differentiable at t"
  shows "frechet_derivative f (at t) 1 = vector_derivative f (at t)"
  apply (subst frechet_derivative_eq_vector_derivative)
   apply (rule assms) by auto


subsection ‹Linear algebra›

lemma (in vector_space) dim_pos_finite_dimensional_vector_spaceE:
  assumes "dim (UNIV::'b set) > 0"
  obtains basis where "finite_dimensional_vector_space scale basis"
proof -
  from assms obtain b where b: "local.span b = local.span UNIV" "local.independent b"
    by (auto simp: dim_def split: if_splits)
  then have "dim UNIV = card b"
    by (rule dim_eq_card)
  with assms have "finite b" by (auto simp: card_ge_0_finite)
  then have "finite_dimensional_vector_space scale b"
    by unfold_locales (auto simp: b)
  then show ?thesis ..
qed

context vector_space_on begin

context includes lifting_syntax assumes "∃(Rep::'s ⇒ 'b) (Abs::'b ⇒ 's). type_definition Rep Abs S" begin

interpretation local_typedef_vector_space_on S scale "TYPE('s)" by unfold_locales fact

lemmas_with [var_simplified explicit_ab_group_add,
    unoverload_type 'd,
    OF type.ab_group_add_axioms type_vector_space_on_with,
    folded dim_S_def,
    untransferred,
    var_simplified implicit_ab_group_add]:
    lt_dim_pos_finite_dimensional_vector_spaceE = vector_space.dim_pos_finite_dimensional_vector_spaceE

end

lemmas_with [cancel_type_definition,
    OF S_ne,
    folded subset_iff',
    simplified pred_fun_def, folded finite_dimensional_vector_space_on_with,
    simplified―‹too much?›]:
    dim_pos_finite_dimensional_vector_spaceE = lt_dim_pos_finite_dimensional_vector_spaceE

end


subsection ‹Extensional function space›

text ‹f is zero outside A. We use such functions to canonically represent
  functions whose domain is A›
definition extensional0 :: "'a set ⇒ ('a ⇒ 'b::zero) ⇒ bool"
  where "extensional0 A f = (∀x. x ∉ A ⟶ f x = 0)"

lemma extensional0_0[intro, simp]: "extensional0 X 0"
  by (auto simp: extensional0_def)

lemma extensional0_UNIV[intro, simp]: "extensional0 UNIV f"
  by (auto simp: extensional0_def)

lemma ext_extensional0:
  "f = g" if "extensional0 S f" "extensional0 S g" "⋀x. x ∈ S ⟹ f x = g x"
  using that by (force simp: extensional0_def fun_eq_iff)

lemma extensional0_add[intro, simp]:
  "extensional0 S f ⟹ extensional0 S g ⟹ extensional0 S (f + g::_⇒'a::comm_monoid_add)"
  by (auto simp: extensional0_def)

lemma extensinoal0_mult[intro, simp]:
  "extensional0 S x ⟹ extensional0 S y ⟹ extensional0 S (x * y)"
  for x y::"_⇒'a::mult_zero"
  by (auto simp: extensional0_def)

lemma extensional0_scaleR[intro, simp]: "extensional0 S f ⟹ extensional0 S (c *⇩R f::_⇒'a::real_vector)"
  by (auto simp: extensional0_def)

lemma extensional0_outside: "x ∉ S ⟹ extensional0 S f ⟹ f x = 0"
  by (auto simp: extensional0_def)

lemma subspace_extensional0: "subspace (Collect (extensional0 X))"
  by (auto simp: subspace_def)

text ‹Send the function f to its canonical representative as a function with domain A›
definition restrict0 :: "'a set ⇒ ('a ⇒ 'b::zero) ⇒ 'a ⇒ 'b"
  where "restrict0 A f x = (if x ∈ A then f x else 0)"

lemma restrict0_UNIV[simp]: "restrict0 UNIV = (λx. x)"
  by (intro ext) (auto simp: restrict0_def)

lemma extensional0_restrict0[intro, simp]: "extensional0 A (restrict0 A f)"
  by (auto simp: extensional0_def restrict0_def)

lemma restrict0_times: "restrict0 A (x * y) = restrict0 A x * restrict0 A y"
  for x::"'a⇒'b::mult_zero"
  by (auto simp: restrict0_def[abs_def])

lemma restrict0_apply_in[simp]: "x ∈ A ⟹ restrict0 A f x = f x"
  by (auto simp: restrict0_def)

lemma restrict0_apply_out[simp]: "x ∉ A ⟹ restrict0 A f x = 0"
  by (auto simp: restrict0_def)

lemma restrict0_scaleR: "restrict0 A (c *⇩R f::_⇒'a::real_vector) = c *⇩R restrict0 A f"
  by (auto simp: restrict0_def[abs_def])

lemma restrict0_add: "restrict0 A (f + g::_⇒'a::real_vector) = restrict0 A f + restrict0 A g"
  by (auto simp: restrict0_def[abs_def])

lemma restrict0_restrict0: "restrict0 X (restrict0 Y f) = restrict0 (X ∩ Y) f"
  by (auto simp: restrict0_def)

end