monotone_subset — Mathlib

English

If F ⊆ G and a dynamical network condition holds for G, then it also holds for F with the same entourage and index.

Русский

Если F ⊆ G и выполняется условие динамической сети для G, то оно выполняется и для F с теми же окружениями и индексами.

LaTeX

$$$F \\subseteq G \\implies \\text{IsDynNetIn } T\\, G\\, U\\, n\\, s \\to \\text{IsDynNetIn } T\\, F\\, U\\, n\\, s$$$

Lean4

theorem monotone_subset {T : X → X} {F G : Set X} (F_G : F ⊆ G) {U : Set (X × X)} {n : ℕ} {s : Set X}
    (h : IsDynNetIn T F U n s) : IsDynNetIn T G U n s :=
  ⟨h.1.trans F_G, h.2⟩

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