isDynCoverOf_zero — Mathlib

English

There is a trivial (U,0)-dynamical cover consisting of a single point that covers a given nonempty F.

Русский

Существуют тривиальные покрытия (U,0) состоящие из одного элемента, покрывающие непустое F.

LaTeX

$$$\exists s: \text{Finset } X, IsDynCoverOf T F U 0 s$$$

Lean4

theorem isDynCoverOf_zero (T : X → X) (F : Set X) (U : Set (X × X)) {s : Set X} (h : s.Nonempty) :
    IsDynCoverOf T F U 0 s :=
  by
  simp only [IsDynCoverOf, ball, dynEntourage, not_lt_zero', Prod.map_iterate, iInter_of_empty, iInter_univ,
    preimage_univ]
  obtain ⟨x, x_s⟩ := h
  exact subset_iUnion₂_of_subset x x_s (subset_univ F)

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