This file defines elem_orbit f x, which is the orbit of x under f. It then defines elem_orbital f x, the orbital of x under f, as the OrdClosure of the orbit of x under f. It then proves many key facts about the oribtal of x under f.

def elem_orbit {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x : α) : Set α

The orbit of x under an automorphism f.

Equations

• elem_orbit f x = MulAction.orbit (↥(Subgroup.zpowers f)) x

theorem swap_between {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (between : (∃ (l : ℤ), (f ^ l) x ≤ y) ∧ ∃ (u : ℤ), y ≤ (f ^ u) x) : (∃ (l : ℤ), (f ^ l) y ≤ x) ∧ ∃ (u : ℤ), x ≤ (f ^ u) y

If y lies between powers of x under f, then x lies between powers of x under f.

theorem mem_elem_orbit_iff {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x y : α) : y ∈ elem_orbit f x ↔ ∃ (z : ℤ), (f ^ z) x = y

y is in the orbit of x under f if and only if there exists an integer z such that (f^z) x = y.

theorem reflexive_elem_orbit {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x : α) : x ∈ elem_orbit f x

x is in the orbit of x under f.

theorem fix_orbit_eq {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x : α} (fix : f x = x) : elem_orbit f x = {x}

If f x = x, then the orbit of x under f is {x}.

def elem_orbital {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x : α) : Set α

The orbital of x under an automorphism f.

Equations

• elem_orbital f x = (elem_orbit f x).ordClosure

theorem elem_orbital_ordConnected {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x : α) : (elem_orbital f x).OrdConnected

The orbital of x under f is OrdConnected.

theorem elem_orbit_subset_elem_orbital {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x : α) : elem_orbit f x ⊆ elem_orbital f x

The orbit of x under f is a subset of the orbital of x under f.

theorem mem_elem_orbital_iff {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x y : α) : y ∈ elem_orbital f x ↔ (∃ (l : ℤ), (f ^ l) x ≤ y) ∧ ∃ (u : ℤ), y ≤ (f ^ u) x

y is in the orbital of x under f if and only if there exists integers l and u such that (f^l) x ≤ y and y ≤ (f^u) x.

theorem incr_mem_elem_orbital_strong {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (incr : isIncreasingAt f x) {l u : ℤ} (hl : (f ^ l) x ≤ y) (hu : y ≤ (f ^ u) x) : ∃ (z : ℤ), (f ^ z) x ≤ y ∧ y < (f ^ (z + 1)) x

If f is increasing at x and y is upper and lower bounded by powers of x under f, then there exists an integer z such that (f ^ z) x ≤ y and y < (f ^ (z+1)) x.

theorem decr_mem_elem_orbital_strong {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (decr : isDecreasingAt f x) {l u : ℤ} (hl : (f ^ l) x ≤ y) (hu : y ≤ (f ^ u) x) : ∃ (z : ℤ), (f ^ (z + 1)) x ≤ y ∧ y < (f ^ z) x

If f is decreasing at x and y is upper and lower bounded by powers of x under f, then there exists an integer z such that (f ^ (z+1)) x ≤ y and y < (f ^ z) x.

theorem mem_elem_orbital_mp_strong {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x y : α) : y ∈ elem_orbital f x → f x = y ∨ (∃ (z : ℤ), (f ^ z) x ≤ y ∧ y < (f ^ (z + 1)) x) ∨ ∃ (z : ℤ), (f ^ (z + 1)) x ≤ y ∧ y < (f ^ z) x

If y is in the orbital of x under f, then either f x = y or there is an integer z such that y is between f ^ z and f ^ (z+1).

theorem mem_elem_orbital_mpr_strong {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x y : α) : (f x = y ∨ (∃ (z : ℤ), (f ^ z) x ≤ y ∧ y < (f ^ (z + 1)) x) ∨ ∃ (z : ℤ), (f ^ (z + 1)) x ≤ y ∧ y < (f ^ z) x) → y ∈ elem_orbital f x

If f x = y or there is an integer z such that y is between f ^ z and f ^ (z+1), then y is in the orbital of x under f.

theorem mem_elem_orbital_strong_iff {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x y : α) : y ∈ elem_orbital f x ↔ f x = y ∨ (∃ (z : ℤ), (f ^ z) x ≤ y ∧ y < (f ^ (z + 1)) x) ∨ ∃ (z : ℤ), (f ^ (z + 1)) x ≤ y ∧ y < (f ^ z) x

y is in the orbital of x under f if and only if either f x = y or there is an integer z such that y is between f ^ z and f ^ (z+1).

theorem mem_elem_orbital_reflexive {α : Type u_1} [LinearOrder α] (f : α ≃o α) (x : α) : x ∈ elem_orbital f x

x is in the orbital of x under f.

theorem mem_elem_orbital_symmetric {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (y_mem : y ∈ elem_orbital f x) : x ∈ elem_orbital f y

If y is in the orbital of x under f, then x is in the orbital of y under f.

theorem mem_elem_orbital_transitive {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y z : α} (hxy : x ∈ elem_orbital f y) (hyz : y ∈ elem_orbital f z) : x ∈ elem_orbital f z

If x is in the orbital of y under f and y is in the orbital of z under f, then x is in the orbital of z under f.

theorem mem_elem_orbital_orbit_between {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (y_mem : y ∈ elem_orbital f x) {z : α} (z_mem_orbit : z ∈ elem_orbit f x) : (∃ (l : ℤ), (f ^ l) y ≤ z) ∧ ∃ (u : ℤ), z ≤ (f ^ u) y

If y is in the orbital of x under f and z is in the orbit of x under f, then z is lower and upper bounded by powers of y.

theorem mem_elem_orbital_eq {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (y_mem : y ∈ elem_orbital f x) : elem_orbital f y = elem_orbital f x

If y is in the orbital of x under f, then the orbital of y under f is equal to the orbital of x under f.

theorem pow_mem_elem_orbital {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (z : ℤ) (y_mem : y ∈ elem_orbital f x) : (f ^ z) y ∈ elem_orbital f x

If y is in the orbital of x under f, then, for any integer z, (f^z) y is in the oribtal of x under f.

theorem pow_mem_elem_orbital_one {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (y_mem : y ∈ elem_orbital f x) : f y ∈ elem_orbital f x

If y is in the orbital of x under f, then f y is in the orbital of x under f.

theorem fix_orbital_eq {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x : α} (fix : f x = x) : elem_orbital f x = {x}

If f x = x, then the orbital of x under f is {x}.

theorem not_fix_orbital_not_singleton {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x : α} (not_fix : f x ≠ x) : elem_orbital f x ≠ {x}

If f x ≠ x, then the orbital of x under f is not {x}.

theorem fix_iff_singleton_orbital {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x : α} : f x = x ↔ elem_orbital f x = {x}

f x = x if and only if the orbital of x under f is {x}.

theorem fix_mem_orbital_eq {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (y_mem : y ∈ elem_orbital f x) (fix : f y = y) : x = y

If y is in the orbital of x under f and f y = y, then x = y.

theorem singleton_orbital_swap {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (singleton_orbital : elem_orbital f x = {y}) : elem_orbital f x = {x}

If the orbital of x under f is {y}, then it is {x}.

theorem not_singleton_at_not_singleton_all {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x : α} (not_single : elem_orbital f x ≠ {x}) (y : α) : elem_orbital f x ≠ {y}

If the orbital of x under f is not {x}, then for any element y, the orbital of x under f is not {y}.

theorem neq_orbitals_not_mem_orbital {α : Type u_1} [LinearOrder α] {f : α ≃o α} {x y : α} (neq_orbitals : elem_orbital f x ≠ elem_orbital f y) : x ∉ elem_orbital f y

If the orbital of x under f is not equal to the orbital of y under f, then x is not in the orbital of y under f.