dynEntourage — Mathlib

English

If U is a symmetric relation, then for every n, the dynamical entourage dynEntourage T U n is symmetric.

Русский

Если U симметрична, то для каждого n окрестность dynEntourage T U n симметрична.

LaTeX

$$$\text{IsSymmetricRel}(\operatorname{dynEntourage}(T,U,n))$ for all n, given IsSymmetricRel(U).$$

Lean4

theorem _root_.IsSymmetricRel.dynEntourage (T : X → X) {U : Set (X × X)} (h : IsSymmetricRel U) (n : ℕ) :
    IsSymmetricRel (dynEntourage T U n) := by
  ext xy
  simp only [Dynamics.dynEntourage, map_iterate, mem_preimage, mem_iInter]
  refine forall₂_congr fun k _ ↦ ?_
  exact map_apply' _ _ _ ▸ IsSymmetricRel.mk_mem_comm h

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