doc(Filter/Pointwise): fix comments (#9202)

leanprover-community · Dec 22, 2023 · 3b841d1 · 3b841d1
1 parent 21e45c8
commit 3b841d1
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/Mathlib/Order/Filter/Pointwise.lean b/Mathlib/Order/Filter/Pointwise.lean
@@ -290,8 +290,8 @@ variable [Mul α] [Mul β] {f f₁ f₂ g g₁ g₂ h : Filter α} {s t : Set α
 /-- The filter `f * g` is generated by `{s * t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
 @[to_additive "The filter `f + g` is generated by `{s + t | s ∈ f, t ∈ g}` in locale `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`. -/
+  ⟨/- 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₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ * t₂ ⊆ s } }⟩
 #align filter.has_mul Filter.instMul
 #align filter.has_add Filter.instAdd
@@ -435,8 +435,8 @@ variable [Div α] {f f₁ f₂ g g₁ g₂ h : Filter α} {s t : Set α} {a b :
 /-- The filter `f / g` is generated by `{s / t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
 @[to_additive "The filter `f - g` is generated by `{s - t | s ∈ f, t ∈ g}` in locale `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`. -/
+  ⟨/- 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₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ / t₂ ⊆ s } }⟩
 #align filter.has_div Filter.instDiv
 #align filter.has_sub Filter.instSub
@@ -963,8 +963,8 @@ variable [SMul α β] {f f₁ f₂ : Filter α} {g g₁ g₂ h : Filter β} {s :
 @[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`. -/
+  ⟨/- 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₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ • t₂ ⊆ s } }⟩
 #align filter.has_smul Filter.instSMul
 #align filter.has_vadd Filter.instVAdd