of_le — Mathlib

English

If m ≤ n and s is a m-dynamical net, then s is also an n-dynamical net (weakening in n preserves the property).

Русский

Если m ≤ n и множество s образует m-динамическую сеть, то оно также образует n-динамическую сеть (с слаблением условия по n).

LaTeX

$${\it (monotonicity in time) }\; m \le n \Rightarrow IsDynNetIn(T, F, U, n, s) \Rightarrow IsDynNetIn(T, F, U, m, s).$$

Lean4

theorem of_le {T : X → X} {F : Set X} {U : Set (X × X)} {m n : ℕ} (m_n : m ≤ n) {s : Set X} (h : IsDynNetIn T F U m s) :
    IsDynNetIn T F U n s :=
  ⟨h.1, PairwiseDisjoint.mono h.2 fun x ↦ ball_mono (dynEntourage_antitone T U m_n) x⟩

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