_aux_Mathlib_Dynamics_OmegaLimit___macroRules_omegaLimit_termω⁺_1

English

For a map g, the ω-limit of a preimage under g is contained in the ω-limit of the original set.

Русский

Для отображения g ω-предел прообраза множества содержится в ω-пределе исходного множества.

LaTeX

$$$$\omega f\ (\lambda t, x.\varphi t (g x))\ (g^{-1} s) \subseteq \omega f\ \varphi\ s.$$$$

Lean4

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

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