of_le — Mathlib

English

If m ≤ n and s is a dynamical cover of order n, then s is also a dynamical cover of order m with the same sets, i.e., IsDynCoverOf T F U n s → IsDynCoverOf T F U m s.

Русский

Если m ≤ n и s является (U, n)-динамическим покрытием, то оно также является (U, m)-покрытием для того же множества.

LaTeX

$$$m \le n \Rightarrow \big( \text{IsDynCoverOf } T F U n s \Rightarrow \text{IsDynCoverOf } T F U m s \big)$$$

Lean4

theorem of_le {T : X → X} {F : Set X} {U : Set (X × X)} {m n : ℕ} (m_n : m ≤ n) {s : Set X}
    (h : IsDynCoverOf T F U n s) : IsDynCoverOf T F U m s :=
  h.trans (iUnion₂_mono fun x _ ↦ ball_mono (dynEntourage_antitone T U m_n) x)

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