_aux_Mathlib_Dynamics_OmegaLimit___macroRules_omegaLimit_termω⁻_1

English

If s1 ⊆ s2, then ω f ϕ s1 ⊆ ω f ϕ s2.

Русский

Если s1 ⊆ s2, то ω-предел для s1 вложен в ω-предел для s2.

LaTeX

$$$$\omega f ϕ s_1 \subseteq \omega f ϕ s_2 \quad\text{если } s_1 \subseteq s_2.$$$$

Lean4

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

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