English
The product f * g of two filters is defined as the filter generated by all products 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. $$$$
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 instMul : Mul (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} }⟩
