This files defines combine_at f g x which is an automorphism whose orbital at x is the union of that of f and g.

noncomputable def combine_at {α : Type u_1} [LinearOrder α] (f g : α ≃o α) (x : α) : α ≃o α

Given automorphisms f and g and an element x, combine_at f g x is an automorphism whose orbital at x is the union of that of f and g.

Equations

• combine_at f g x = (orbital_at_non_decr f x).trans (orbital_at_non_decr g x)

theorem not_decr_combine_at {α : Type u_1} [LinearOrder α] (f g : α ≃o α) (x y : α) : y ≤ (combine_at f g x) y

For any y, we have that y ≤ (combine_at f g x) y.

theorem f_le_combine_at {α : Type u_1} [LinearOrder α] {f : α ≃o α} (g : α ≃o α) {x y : α} : (orbital_at_non_decr f x) y ≤ (combine_at f g x) y

For any y in the orbital of x under f, (orbital_at_non_decr f x) y ≤ (combine_at f g x) y.

theorem inv_f_ge_combine_at {α : Type u_1} [LinearOrder α] {f : α ≃o α} (g : α ≃o α) {x y : α} : (combine_at f g x).symm y ≤ (orbital_at_non_decr f x).symm y

For any y in the orbital of x under f, (combine_at f g x).symm y ≤ (orbital_at_non_decr f x) y.

theorem inv_g_ge_combine_at {α : Type u_1} [LinearOrder α] {g : α ≃o α} (f : α ≃o α) {x y : α} : (combine_at f g x).symm y ≤ (orbital_at_non_decr g x).symm y

For any y in the orbital of x under f, (combine_at f g x).symm y ≤ (orbital_at_non_decr g x) y.

theorem g_le_combine_at {α : Type u_1} [LinearOrder α] {g : α ≃o α} (f : α ≃o α) {x y : α} : (orbital_at_non_decr g x) y ≤ (combine_at f g x) y

For any y in the orbital of x under f, (orbital_at_non_decr g x) y ≤ (combine_at f g x) y.

theorem pow_f_le_combine_at {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (n : ℕ) : (orbital_at_non_decr f x ^ n) y ≤ (combine_at f g x ^ n) y

For any y and natural number n, (orbital_at_non_decr f x)^n y ≤ (combine_at f g x)^n y.

theorem pow_g_le_combine_at {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (n : ℕ) : (orbital_at_non_decr g x ^ n) y ≤ (combine_at f g x ^ n) y

For any y and natural number n, (orbital_at_non_decr g x)^n y ≤ (combine_at f g x)^n y.

theorem pow_f_inv_ge_combine_at {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (n : ℕ) : (combine_at f g x ^ (-↑n)) y ≤ (orbital_at_non_decr f x ^ (-↑n)) y

For any y and natural number n, (combine_at f g x)^(-n) y ≤ (orbital_at_non_decr f x)^(-n) y.

theorem pow_g_inv_ge_combine_at {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (n : ℕ) : (combine_at f g x ^ (-↑n)) y ≤ (orbital_at_non_decr g x ^ (-↑n)) y

For any y and natural number n, (combine_at f g x)^(-n) y ≤ (orbital_at_non_decr g x)^(-n) y.

theorem pow_f_le_pow_combine_le {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} {z : ℤ} (pow_f_le : (orbital_at_non_decr f x ^ z) x ≤ y) : ∃ (l : ℤ), (combine_at f g x ^ l) x ≤ y

If there exists an integer z such that (orbital_at_non_decr f x)^z x ≤ y, then there exists an integer l such that (combine_at f g x)^l x ≤ y.

theorem pow_g_le_pow_combine_le {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} {z : ℤ} (pow_g_le : (orbital_at_non_decr g x ^ z) x ≤ y) : ∃ (l : ℤ), (combine_at f g x ^ l) x ≤ y

If there exists an integer z such that (orbital_at_non_decr g x)^z x ≤ y, then there exists an integer l such that (combine_at f g x)^l x ≤ y.

theorem pow_f_ge_combine_ge {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} {z : ℤ} (pow_f_ge : y ≤ (orbital_at_non_decr f x ^ z) x) : ∃ (u : ℤ), y ≤ (combine_at f g x ^ u) x

If there exists an integer z such that y ≤ (orbital_at_non_decr f x)^z x, then there exists an integer u such that y ≤ (combine_at f g x)^u x.

theorem pow_g_ge_combine_ge {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} {z : ℤ} (pow_g_ge : y ≤ (orbital_at_non_decr g x ^ z) x) : ∃ (u : ℤ), y ≤ (combine_at f g x ^ u) x

If there exists an integer z such that y ≤ (orbital_at_non_decr g x)^z x, then there exists an integer u such that y ≤ (combine_at f g x)^u x.

theorem f_fix_combine_le {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (fix : (orbital_at_non_decr f x) x = y) : ∃ (l : ℤ), (combine_at f g x ^ l) x ≤ y

If there exists a y such that (orbital_at_non_decr f x) x = y, then there exists an integer l such that (combine_at f g x)^l x ≤ y.

theorem g_fix_combine_le {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (fix : (orbital_at_non_decr g x) x = y) : ∃ (l : ℤ), (combine_at f g x ^ l) x ≤ y

If there exists a y such that (orbital_at_non_decr g x) x = y, then there exists an integer l such that (combine_at f g x)^l x ≤ y.

theorem f_fix_combine_ge {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (fix : (orbital_at_non_decr f x) x = y) : ∃ (u : ℤ), y ≤ (combine_at f g x ^ u) x

If there exists a y such that (orbital_at_non_decr f x) x = y, then there exists an integer u such that y ≤ (combine_at f g x)^u x.

theorem g_fix_combine_ge {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (fix : (orbital_at_non_decr g x) x = y) : ∃ (u : ℤ), y ≤ (combine_at f g x ^ u) x

If there exists a y such that (orbital_at_non_decr g x) x = y, then there exists an integer u such that y ≤ (combine_at f g x)^u x.

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

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

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

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

theorem f_g_orbital_subset_combine_orbital {α : Type u_1} [LinearOrder α] (f g : α ≃o α) (x : α) : elem_orbital f x ∪ elem_orbital g x ⊆ elem_orbital (combine_at f g x) x

The union of the orbital of x under f and the orbital of x under g is a subset of the orbital of x under combine_at f g x.

theorem combine_orbital_subset_f_g_orbital {α : Type u_1} [LinearOrder α] (f g : α ≃o α) (x : α) : elem_orbital (combine_at f g x) x ⊆ elem_orbital f x ∪ elem_orbital g x

theorem combine_orbital_eq_union {α : Type u_1} [LinearOrder α] (f g : α ≃o α) (x : α) : elem_orbital (combine_at f g x) x = elem_orbital f x ∪ elem_orbital g x

The orbital of x under combine_at f g x is equal to the union of the orbital of x under f and the orbital of x under g.

theorem not_mem_orbital_at_combine_at_eq {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (y_not_mem : y ∉ elem_orbital (combine_at f g x) x) : (combine_at f g x) y = y

If y is not in the orbital of x under combine_at f g x, then (combine_at f g x) y = y.

theorem not_mem_orbital_singleton {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (y_not_mem : y ∉ elem_orbital (combine_at f g x) x) : elem_orbital (combine_at f g x) y = {y}

If y is not in the orbital of x under (combine_at f g x), then the orbital of y under (combine_at f g x) is {y}.

theorem fix_at_fix_all {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x : α} (fix : (combine_at f g x) x = x) (y : α) : (combine_at f g x) y = y

If combine_at f g x fixes x, then it fixes everything.

theorem not_singleton_at_not_singleton {α : Type u_1} [LinearOrder α] {f g : α ≃o α} {x y : α} (not_single : ¬elem_orbital (combine_at f g x) y = {y}) : ¬elem_orbital (combine_at f g x) x = {x}

If the orbital of y under combine_at f g x is not {y}, then the orbital of x under combine_at f g x is not {x}.