General theory

DefinitionOmega-limit sets#

The ω-limit of a set s under ϕ with respect to a filter f is ⋂ u ∈ f, cl (ϕ u s).

omegaLimit.{u_1, u_2, u_3} {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β]
  (f : Filter τ) (ϕ : τ → α → β) (s : Set α) : Set β

Sources

• Mathlib documentation: omegaLimit
• Source of omegaLimit in Mathlib/Dynamics/OmegaLimit.lean
• Mathlib overview: Dynamics › General theory

MathlibomegaLimit

Uses 2

Statement usesClosure · Filter

DefinitionFixed points#

The set of fixed points of a map f : α → α.

Function.fixedPoints.{u_1} {α : Type u_1} (f : α → α) : Set α

Sources

• Mathlib documentation: Function.fixedPoints
• Source of Function.fixedPoints in Mathlib/Dynamics/FixedPoints/Defs.lean
• Mathlib overview: Dynamics › General theory

MathlibFunction.fixedPoints

Uses 1 · Used by 4

Statement usesSet

Used byDerangements Formula · Bourbaki–Witt theorem · Kleene fixed-point theorem · Knaster–Tarski theorem

DefinitionPeriodic points#

The set of periodic points of a map f : α → α.

Function.periodicPts.{u_1} {α : Type u_1} (f : α → α) : Set α

Sources

• Mathlib documentation: Function.periodicPts
• Source of Function.periodicPts in Mathlib/Dynamics/PeriodicPts/Defs.lean
• Mathlib overview: Dynamics › General theory

MathlibFunction.periodicPts

Uses 1 · Used by 3

Statement usesNatural number

Used byCauchy-Davenport theorem · Focal subgroup theorem · Dirichlet's unit theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.