[GOAL]
α : Type u
β : Type v
f fa g : α → α
x✝ y : α
fb : β → β
m n k : ℕ
e : Perm α
x : α
hx : IsFixedPt f x
⊢ IsFixedPt f (f x)
[PROOFSTEP]
convert hx
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n✝ k : ℕ
e : Perm α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f^[n]) s
[PROOFSTEP]
rw [Set.preimage_iterate_eq]
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n✝ k : ℕ
e : Perm α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f)^[n] s
[PROOFSTEP]
exact h.iterate n
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n✝ k : ℕ
e : Perm α
h : IsFixedPt (↑e) x
n : ℕ
⊢ IsFixedPt (↑(e ^ n)) x
[PROOFSTEP]
rw [Equiv.Perm.coe_pow]
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n✝ k : ℕ
e : Perm α
h : IsFixedPt (↑e) x
n : ℕ
⊢ IsFixedPt (↑e)^[n] x
[PROOFSTEP]
exact h.iterate _
[GOAL]
α✝ : Type u
β : Type v
f✝ fa g : α✝ → α✝
x✝ y : α✝
fb : β → β
m n k : ℕ
e : Perm α✝
α : Type u_1
f : α → α
x : α
⊢ x ∈ fixedPoints f ↔ f x = x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n k : ℕ
e : Perm α
x✝ : α
⊢ x✝ ∈ fixedPoints id ↔ x✝ ∈ Set.univ
[PROOFSTEP]
simpa using isFixedPt_id _
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n k : ℕ
e : Perm α
h : Function.Commute f g
⊢ Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
[PROOFSTEP]
simpa only [h.comp_eq] using Function.invOn_fixedPoints_comp f g
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n k : ℕ
e : Perm α
h : Function.Commute f g
⊢ Set.BijOn f (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
[PROOFSTEP]
simpa only [h.comp_eq] using bijOn_fixedPoints_comp g f
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n k : ℕ
e : Perm α
h : Function.Commute f g
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
[PROOFSTEP]
simpa only [h.comp_eq] using bijOn_fixedPoints_comp f g
