α : Type u_1
β : Type ?u.30100
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ minimalPeriod f x = 0 ↔ ¬x ∈ periodicPts f
α : Type u_1
β : Type ?u.30100
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ periodicOrbit f x = Cycle.nil ↔ ¬x ∈ periodicPts f
simp [periodicOrbit]
no goals
α : Type u_1
β : Type ?u.30100
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ minimalPeriod f x = 0 ↔ ¬x ∈ periodicPts f
exact minimalPeriod_eq_zero_iff_nmem_periodicPts