symmDiff — Mathlib

English

If s is eventually equal to t along l and s' is eventually equal to t' along l, then the symmetric differences s Δ s' and t Δ t' are again eventually equal along l.

Русский

Если s асимптотически равно t по фильтру l и s' асимптотически равен t' по l, то симметрические различия s Δ s' и t Δ t' тоже асимптотически равны по l.

LaTeX

$$$ (s =ᶠ[l] t) ∧ (s' =ᶠ[l] t') \\Rightarrow (s \\Delta s' : Set α) =ᶠ[l] (t \\Delta t' : Set α) $$$

Lean4

@[gcongr]
protected theorem symmDiff {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
    (s ∆ s' : Set α) =ᶠ[l] (t ∆ t' : Set α) :=
  (h.diff h').union (h'.diff h)

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