test

Author: CBirkbeck

LeanBridge.lean

@@ -0,0 +1 @@
+import LeanBridge.Example

LeanBridge/Example.lean

@@ -0,0 +1,9 @@
+import Mathlib
+
+
+--this is just a test file to check that the import works
+variable {α β F : Type*} [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ}
+
+theorem HasSumUniformlyOn_of_bounded {f : α → β → F} (hu : Summable u) {s : Set β}
+    (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) : HasSumUniformlyOn f (fun x => ∑' n, f n x) {s} :=  by
+  simp [hasSumUniformlyOn_iff_tendstoUniformlyOn, tendstoUniformlyOn_tsum hu hfu]

LeanBridge/Mathlib/README.md

@@ -0,0 +1,3 @@
+# Mathlib
+
+This folder contains `.lean` files with declarations missing from the current version of Mathlib.