isDynCoverOf_univ — Mathlib

English

For any T, F, and n, if s is a nonempty subset, then s is a (univ, n)-dynamical cover of F.

Русский

Для любых T, F, n и непустого s, s является (univ, n)-динамическим покрытием F.

LaTeX

$$$\text{IsDynCoverOf}(T, F, \mathrm{univ}, n, s)$$$

Lean4

theorem isDynCoverOf_univ (T : X → X) (F : Set X) (n : ℕ) {s : Set X} (h : s.Nonempty) : IsDynCoverOf T F univ n s :=
  by
  simp only [IsDynCoverOf, ball, dynEntourage, Prod.map_iterate, preimage_univ, iInter_univ]
  obtain ⟨x, x_s⟩ := h
  exact subset_iUnion₂_of_subset x x_s (subset_univ F)

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