sub_eq — Mathlib

English

If f and g are eventually equal along l, then their pointwise difference f - g is eventually equal to 0 (assuming an additive group structure on β).

Русский

Если f и g совпадают вдоль фильтра l, то их по точкам разность f − g эквивалентна нулю вдоль l (при условии существования группы сложения в β).

LaTeX

$$$ f =ᶠ[l] g \\Rightarrow f - g =ᶠ[l] 0 $$$

Lean4

theorem sub_eq [AddGroup β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) : f - g =ᶠ[l] 0 := by
  simpa using ((EventuallyEq.refl l f).sub h).symm

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