English
The smul operation on filters is defined by generating sets {s • t | s ∈ f, t ∈ g}.
Русский
Операция смул на фильтрах задаётся как порождение множеств {s • t | s ∈ f, t ∈ g}.
LaTeX
$$SMul( Filter α )( Filter β ) defined by sets := { s | ∃ t1 ∈ f, ∃ t2 ∈ g, t1 • t2 ⊆ 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 locale
`Pointwise`. -/
]
protected def instSMul : SMul (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} }⟩
