Theorems · Theorem · field theory

Function.Periodic.image_uIcc

∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α] [inst_1 : LinearOrder α]
  [IsOrderedAddMonoid α] [Archimedean α],
  Function.Periodic f c → c ≠ 0 → ∀ (a : α), f '' Set.uIcc a (a + c) = Set.range f

Defined in: Mathlib.Algebra.Field.Periodic
Cited by: 1 results in Mathlib
Foundations: Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommGroup LinearOrder IsOrderedAddMonoid Archimedean

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites20

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
AddCommGroupstatement and proof · cited by 12,871
LinearOrderstatement and proof · cited by 8,572
Set.imagestatement and proof · cited by 5,609
Set.rangestatement and proof · cited by 4,705
LT.lt.leproof · cited by 2,189
Set.Iccproof · cited by 1,702
IsOrderedAddMonoidstatement and proof · cited by 1,659
Archimedeanstatement and proof · cited by 603
Set.uIccstatement · cited by 393
Function.Periodicstatement and proof · cited by 154
Ne.lt_or_gtproof · cited by 108

Cited by1

Results whose statement or proof uses this declaration.

Function.Periodic.compact_of_continuousproof · cited by 1