of_entourage_subset — Mathlib

English

If U ⊆ V, then IsDynNetIn(T,F,V,n,s) implies IsDynNetIn(T,F,U,n,s).

Русский

Если U ⊆ V, то из IsDynNetIn(T,F,V,n,s) следует IsDynNetIn(T,F,U,n,s).

LaTeX

$$$U\subseteq V \Rightarrow IsDynNetIn(T,F,V,n,s) \Rightarrow IsDynNetIn(T,F,U,n,s).$$$

Lean4

theorem of_entourage_subset {T : X → X} {F : Set X} {U V : Set (X × X)} (U_V : U ⊆ V) {n : ℕ} {s : Set X}
    (h : IsDynNetIn T F V n s) : IsDynNetIn T F U n s :=
  ⟨h.1, PairwiseDisjoint.mono h.2 fun x ↦ ball_mono (dynEntourage_monotone T n U_V) x⟩

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