α : Type u_1
β : Type ?u.30921
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ (∃ a, a < minimalPeriod f x ∧ (f^[a]) x = y) ↔ ∃ n, (f^[n]) x = y
α : Type u_1
β : Type ?u.30921
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ y ∈ periodicOrbit f x ↔ ∃ n, (f^[n]) x = y
simp only [periodicOrbit, Cycle.mem_coe_iff, List.mem_map, List.mem_range]
α : Type u_1
β : Type ?u.30921
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ (∃ n, (f^[n]) x = y) → ∃ a, a < minimalPeriod f x ∧ (f^[a]) x = y
α : Type u_1
β : Type ?u.30921
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ (∃ a, a < minimalPeriod f x ∧ (f^[a]) x = y) ↔ ∃ n, (f^[n]) x = y
use fun ⟨a, _, ha'⟩ => ⟨a, ha'⟩
case intro
α : Type u_1
β : Type ?u.30921
f fa : α → α
fb : β → β
x : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ ∃ a, a < minimalPeriod f x ∧ (f^[a]) x = (f^[n]) x
α : Type u_1
β : Type ?u.30921
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ (∃ n, (f^[n]) x = y) → ∃ a, a < minimalPeriod f x ∧ (f^[a]) x = y
rintro ⟨n, rfl⟩
case intro
α : Type u_1
β : Type ?u.30921
f fa : α → α
fb : β → β
x : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ (f^[n % minimalPeriod f x]) x = (f^[n]) x
case intro
α : Type u_1
β : Type ?u.30921
f fa : α → α
fb : β → β
x : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ ∃ a, a < minimalPeriod f x ∧ (f^[a]) x = (f^[n]) x
use n % minimalPeriod f x, mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx)
no goals
case intro
α : Type u_1
β : Type ?u.30921
f fa : α → α
fb : β → β
x : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ (f^[n % minimalPeriod f x]) x = (f^[n]) x
rw [iterate_mod_minimalPeriod_eq]