mulSupport — Mathlib

English

If two functions are eventually equal, their multiplicative supports coincide eventually.

Русский

Если две функции равны вплоть до предела, то их множества поддержки совпадают вплоть до предела.

LaTeX

$$$\\text{l.E EventuallyEq}(f,g) \\Rightarrow \\text{l.EventuallyEq}(\\mathrm{mulSupport}(f), \\mathrm{mulSupport}(g))$$$

Lean4

@[to_additive]
protected theorem mulSupport [One β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
    Function.mulSupport f =ᶠ[l] Function.mulSupport g :=
  h.preimage ({ 1 }ᶜ : Set β)

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