English
The filter difference operation f -ᵥ g is generated by all sums t₁ -ᵥ t₂ with t₁ ∈ f and t₂ ∈ g.
Русский
Разность фильтров по пересечению во взятии векторной разности порождается всеми t₁ -ᵥ t₂, где t₁ ∈ f и t₂ ∈ g.
LaTeX
$$$\mathrm{instVSub}.sets := \{ s \mid \exists t_1 \in f, \exists t_2 \in g, t_1 -\tfrac{v}{ } t_2 \subseteq s\}$$$
Lean4
/-- The filter `f -ᵥ g` is generated by `{s -ᵥ t | s ∈ f, t ∈ g}` in scope `Pointwise`. -/
protected def instVSub : VSub (Filter α) (Filter β) :=
⟨ /- This is defeq to `map₂ (-ᵥ) f g`, but the hypothesis unfolds to `t₁ -ᵥ t₂ ⊆ s` rather than all
the way to `Set.image2 (-ᵥ) t₁ t₂ ⊆ s`. -/
fun f g => { map₂ (· -ᵥ ·) f g with sets := {s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s} }⟩
