idRel_subset_dynEntourage — Mathlib

English

If idRel ⊆ U, then idRel ⊆ dynEntourage T U n for every n.

Русский

Если idRel ⊆ U, то idRel ⊆ dynEntourage T U n для любого n.

LaTeX

$$$\text{idRel} \subseteq U \Rightarrow \text{idRel} \subseteq \operatorname{dynEntourage}(T,U,n)\; (\forall n).$$$

Lean4

theorem idRel_subset_dynEntourage (T : X → X) {U : Set (X × X)} (h : idRel ⊆ U) (n : ℕ) :
    idRel ⊆ (dynEntourage T U n) :=
  by
  simp only [dynEntourage, map_iterate, subset_iInter_iff, idRel_subset, mem_preimage, map_apply]
  exact fun _ _ _ ↦ h rfl

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