mulIndicator_eventuallyLE_mulIndicator

English

If f ≤ᶠ g (eventually less or equal), then the indicator of s preserves the order: mulIndicator s f ≤ᶠ mulIndicator s g along the filter.

Русский

Если f ≤ᶠ g, то индикатор множителя s сохраняет порядок: mulIndicator s f ≤ᶠ mulIndicator s g вдоль фильтра.

LaTeX

$$$\\text{mulIndicator}(s, f) \\le^ᶠ_l \\text{mulIndicator}(s, g)$ whenever $f \\le^ᶠ_l g$$$

Lean4

@[to_additive]
theorem mulIndicator_eventuallyLE_mulIndicator (h : f ≤ᶠ[l ⊓ 𝓟 s] g) : mulIndicator s f ≤ᶠ[l] mulIndicator s g :=
  (eventually_inf_principal.1 h).mono fun _ => mulIndicator_rel_mulIndicator le_rfl

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