α : Type u_1
β : Type ?u.22741
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find (_ : x ∈ periodicPts f) ≤ n
α : Type u_1
β : Type ?u.22741
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n
rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
no goals
α : Type u_1
β : Type ?u.22741
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find (_ : x ∈ periodicPts f) ≤ n
exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩