diff — Mathlib

English

If s =^l t and s' =^l t', then s \\ s' =^l t \\ t'.

Русский

Если s =^l t и s' =^l t', то s \\ s' =^l t \\ t'.

LaTeX

$$$\\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall s,t,s',t' \\\\subseteq α, \\\\ (s =^l t) \\\\land \\\\ (s' =^l t') \\\\Rightarrow \\\\bigl((s \\\\setminus s') =^l (t \\\\setminus t')\\\\bigr)$$$

Lean4

@[gcongr]
theorem diff {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
    (s \ s' : Set α) =ᶠ[l] (t \ t' : Set α) :=
  h.inter h'.compl

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