_aux_Mathlib_Dynamics_OmegaLimit___macroRules_omegaLimit_termω_1

English

If ϕ changes with t but is consistent with a map g, then the ω-limit of the image of s under g equals the ω-limit of the transformed s under ϕ.

Русский

Если ϕ меняется с t, но согласована с отображением g, то ω-предел образа s под g совпадает с ω-пределом преобразованного s под ϕ.

LaTeX

$$$$\omega f\,\varphi\ (g''s) = \omega f\ (\lambda t\ x.\varphi t (g x))\ s.$$$

Lean4

@[scoped macro omegaLimit.termω]
public meta def _aux_Mathlib_Dynamics_OmegaLimit___macroRules_omegaLimit_termω_1 : Macro✝ := fun
  | `(ω) => ``(omegaLimit)
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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