of_entourage_subset — Mathlib

English

For any T, any U, and any n, the empty set is a (U, n)-dynamical cover of the empty set: IsDynCoverOf T ∅ U n ∅.

Русский

Для любых T, U и n пустое множество является (U, n)-динамическим покрытием пустого множества: IsDynCoverOf T ∅ U n ∅.

LaTeX

$$$\text{IsDynCoverOf}(T, \emptyset, U, n, \emptyset)$$$

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 : IsDynCoverOf T F U n s) : IsDynCoverOf T F V n s :=
  h.trans (iUnion₂_mono fun x _ ↦ ball_mono (dynEntourage_monotone T n U_V) x)

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