feat(measure_theory/integral): define circle_integral (#10906)

leanprover-community · Dec 25, 2021 · 0aca706 · 0aca706
1 parent ef8005c
commit 0aca706
Show file tree

Hide file tree

Showing 3 changed files with 533 additions and 1 deletion.
diff --git a/src/algebra/periodic.lean b/src/algebra/periodic.lean
@@ -273,6 +273,12 @@ lemma periodic.exists_mem_Ioc [linear_ordered_add_comm_group α] [archimedean α
 let ⟨n, H, _⟩ := exists_unique_add_zsmul_mem_Ioc hc x a in
 ⟨x + n • c, H, (h.zsmul n x).symm⟩
 
+lemma periodic.image_Ioc [linear_ordered_add_comm_group α] [archimedean α]
+  (h : periodic f c) (hc : 0 < c) (a : α) :
+  f '' set.Ioc a (a + c) = set.range f :=
+(set.image_subset_range _ _).antisymm $ set.range_subset_iff.2 $ λ x,
+  let ⟨y, hy, hyx⟩ := h.exists_mem_Ioc hc x a in ⟨y, hy, hyx.symm⟩
+
 lemma periodic_with_period_zero [add_zero_class α]
   (f : α → β) :
   periodic f 0 :=