dynEntourage_antitone — Mathlib

English

For fixed T and U, the sequence n ↦ dynEntourage(T, U, n) is antitone: if m ≤ n, then dynEntourage(T, U, n) ⊆ dynEntourage(T, U, m).

Русский

Для фиксированных T и U последовательность n ↦ dynEntourage(T, U, n) антимонотонна: если m ≤ n, то dynEntourage(T, U, n) ⊆ dynEntourage(T, U, m).

LaTeX

$$$\forall m,n \in \mathbb{N},\ m \le n \Rightarrow \ dynEntourage(T,U,n) \subseteq dynEntourage(T,U,m).$$$

Lean4

theorem dynEntourage_antitone (T : X → X) (U : Set (X × X)) : Antitone (fun n : ℕ ↦ dynEntourage T U n) := fun m n m_n ↦
  iInter₂_mono' fun k k_m ↦ by use k, lt_of_lt_of_le k_m m_n

Похожие утверждения