Fixed points of a self-map

In this file we define the set Function.fixedPoints of fixed points of a function f : α → α. The related predicate IsFixedPt is defined in Mathlib.Logic.Function.Defs.

Tags

fixed point

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

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

Equations

• Function.fixedPoints f = {x : α | Function.IsFixedPt f x}

@[instance_reducible]

instance Function.fixedPoints.decidable {α : Type u_1} [DecidableEq α] (f : α → α) (x : α) : Decidable (x ∈ fixedPoints f)

Equations

• Function.fixedPoints.decidable f x = Function.IsFixedPt.decidable

@[simp]

theorem Function.mem_fixedPoints {α : Type u_1} {x : α} {f : α → α} : x ∈ fixedPoints f ↔ IsFixedPt f x

theorem Function.mem_fixedPoints_iff {α : Type u_2} {f : α → α} {x : α} : x ∈ fixedPoints f ↔ f x = x

@[simp]

theorem Function.fixedPoints_id {α : Type u_1} : fixedPoints id = Set.univ

@[simp]

theorem Function.inter_subset_fixedPoints_comp {α : Type u_1} {f g : α → α} : fixedPoints f ∩ fixedPoints g ⊆ fixedPoints (f ∘ g)

theorem Function.fixedPoints_subset_range {α : Type u_1} {f : α → α} : fixedPoints f ⊆ Set.range f