English
For a semilattice with join and an order-preserving map f: α →o α, the following are equivalent: (i) for all n1, n2, a1, a2, f^[n1+n2](a1 ⊔ a2) ≤ f^[n1] a1 ⊔ f^[n2] a2; (ii) for all a1, a2, f(a1 ⊔ a2) ≤ f a1 ⊔ a2.
Русский
Для полусложенного порядка с операцией объединения (⊔) и отображения f: α →o α верно: (i) для всех n1, n2, a1, a2 верно f^[n1+n2](a1 ⊔ a2) ≤ f^[n1] a1 ⊔ f^[n2] a2; тогда (ii) для всех a1, a2 верно f(a1 ⊔ a2) ≤ f a1 ⊔ a2, и наоборот.
LaTeX
$$$\forall f:\alpha \to_o \alpha,\;\left(\forall n_1,n_2,a_1,a_2,\ f^{[n_1+n_2]}(a_1 \ ⊔ \ a_2) \le f^{[n_1]} a_1 \ ⊔ \ f^{[n_2]} a_2\right) \iff \left(\forall a_1,a_2,\ f(a_1 \ ⊔ \ a_2) \le f a_1 \ ⊔ \ a_2\right)$$$$
Lean4
theorem iterate_sup_le_sup_iff {α : Type*} [SemilatticeSup α] (f : α →o α) :
(∀ n₁ n₂ a₁ a₂, f^[n₁ + n₂] (a₁ ⊔ a₂) ≤ f^[n₁] a₁ ⊔ f^[n₂] a₂) ↔ ∀ a₁ a₂, f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂ :=
by
constructor <;> intro h
· exact h 1 0
· intro n₁ n₂ a₁ a₂
have h' : ∀ n a₁ a₂, f^[n] (a₁ ⊔ a₂) ≤ f^[n] a₁ ⊔ a₂ :=
by
intro n
induction n with
| zero => intro a₁ a₂; rfl
| succ n ih =>
intro a₁ a₂
calc
f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
_ ≤ f^[n] (f a₁ ⊔ a₂) := (f.mono.iterate n (h a₁ a₂))
_ ≤ f^[n] (f a₁) ⊔ a₂ := (ih _ _)
_ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
calc
f^[n₁ + n₂] (a₁ ⊔ a₂) = f^[n₁] (f^[n₂] (a₁ ⊔ a₂)) := Function.iterate_add_apply f n₁ n₂ _
_ = f^[n₁] (f^[n₂] (a₂ ⊔ a₁)) := by rw [sup_comm]
_ ≤ f^[n₁] (f^[n₂] a₂ ⊔ a₁) := (f.mono.iterate n₁ (h' n₂ _ _))
_ = f^[n₁] (a₁ ⊔ f^[n₂] a₂) := by rw [sup_comm]
_ ≤ f^[n₁] a₁ ⊔ f^[n₂] a₂ := h' n₁ a₁ _
