English
The division of two filters f and g is defined as the filter generated by all quotients t1 / t2 with t1 ∈ f and t2 ∈ g.
Русский
Разделение двух фильтров f и g определяется как фильтр, порождаемый всеми частями t1 / t2, где t1 ∈ f и t2 ∈ g.
LaTeX
$$$f / g = \\operatorname{map}_2 (\\cdot / \\cdot) f g,$ i.e. generated by $\\{ s \\mid \\exists t_1 \\in f, \\exists t_2 \\in g, t_1 / t_2 \\subseteq s \\}$.$$
Lean4
/-- The filter `f / g` is generated by `{s / t | s ∈ f, t ∈ g}` in scope `Pointwise`. -/
@[to_additive /-- The filter `f - g` is generated by `{s - t | s ∈ f, t ∈ g}` in scope `Pointwise`. -/
]
protected def instDiv : Div (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} }⟩
