# mathlib3documentation

order.filter.pointwise

# Pointwise operations on filters #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines pointwise operations on filters. This is useful because usual algebraic operations distribute over pointwise operations. For example,

• `(f₁ * f₂).map m = f₁.map m * f₂.map m`
• `𝓝 (x * y) = 𝓝 x * 𝓝 y`

## Main declarations #

• `0` (`filter.has_zero`): Pure filter at `0 : α`, or alternatively principal filter at `0 : set α`.
• `1` (`filter.has_one`): Pure filter at `1 : α`, or alternatively principal filter at `1 : set α`.
• `f + g` (`filter.has_add`): Addition, filter generated by all `s + t` where `s ∈ f` and `t ∈ g`.
• `f * g` (`filter.has_mul`): Multiplication, filter generated by all `s * t` where `s ∈ f` and `t ∈ g`.
• `-f` (`filter.has_neg`): Negation, filter of all `-s` where `s ∈ f`.
• `f⁻¹` (`filter.has_inv`): Inversion, filter of all `s⁻¹` where `s ∈ f`.
• `f - g` (`filter.has_sub`): Subtraction, filter generated by all `s - t` where `s ∈ f` and `t ∈ g`.
• `f / g` (`filter.has_div`): Division, filter generated by all `s / t` where `s ∈ f` and `t ∈ g`.
• `f +ᵥ g` (`filter.has_vadd`): Scalar addition, filter generated by all `s +ᵥ t` where `s ∈ f` and `t ∈ g`.
• `f -ᵥ g` (`filter.has_vsub`): Scalar subtraction, filter generated by all `s -ᵥ t` where `s ∈ f` and `t ∈ g`.
• `f • g` (`filter.has_smul`): Scalar multiplication, filter generated by all `s • t` where `s ∈ f` and `t ∈ g`.
• `a +ᵥ f` (`filter.has_vadd_filter`): Translation, filter of all `a +ᵥ s` where `s ∈ f`.
• `a • f` (`filter.has_smul_filter`): Scaling, filter of all `a • s` where `s ∈ f`.

For `α` a semigroup/monoid, `filter α` is a semigroup/monoid. As an unfortunate side effect, this means that `n • f`, where `n : ℕ`, is ambiguous between pointwise scaling and repeated pointwise addition. See note [pointwise nat action].

## Implementation notes #

We put all instances in the locale `pointwise`, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior of `simp`.

## Tags #

filter multiplication, filter addition, pointwise addition, pointwise multiplication,

### `0`/`1` as filters #

@[protected]
def filter.has_zero {α : Type u_2} [has_zero α] :

`0 : filter α` is defined as the filter of sets containing `0 : α` in locale `pointwise`.

Equations
@[protected]
def filter.has_one {α : Type u_2} [has_one α] :

`1 : filter α` is defined as the filter of sets containing `1 : α` in locale `pointwise`.

Equations
@[simp]
theorem filter.mem_zero {α : Type u_2} [has_zero α] {s : set α} :
s 0 0 s
@[simp]
theorem filter.mem_one {α : Type u_2} [has_one α] {s : set α} :
s 1 1 s
theorem filter.zero_mem_zero {α : Type u_2} [has_zero α] :
0 0
theorem filter.one_mem_one {α : Type u_2} [has_one α] :
1 1
@[simp]
theorem filter.pure_zero {α : Type u_2} [has_zero α] :
@[simp]
theorem filter.pure_one {α : Type u_2} [has_one α] :
@[simp]
theorem filter.principal_one {α : Type u_2} [has_one α] :
@[simp]
theorem filter.principal_zero {α : Type u_2} [has_zero α] :
theorem filter.one_ne_bot {α : Type u_2} [has_one α] :
theorem filter.zero_ne_bot {α : Type u_2} [has_zero α] :
@[protected, simp]
theorem filter.map_one' {α : Type u_2} {β : Type u_3} [has_one α] (f : α β) :
1 = has_pure.pure (f 1)
@[protected, simp]
theorem filter.map_zero' {α : Type u_2} {β : Type u_3} [has_zero α] (f : α β) :
0 = has_pure.pure (f 0)
@[simp]
theorem filter.nonpos_iff {α : Type u_2} [has_zero α] {f : filter α} :
f 0 0 f
@[simp]
theorem filter.le_one_iff {α : Type u_2} [has_one α] {f : filter α} :
f 1 1 f
@[protected]
theorem filter.ne_bot.le_one_iff {α : Type u_2} [has_one α] {f : filter α} (h : f.ne_bot) :
f 1 f = 1
@[protected]
theorem filter.ne_bot.nonpos_iff {α : Type u_2} [has_zero α] {f : filter α} (h : f.ne_bot) :
f 0 f = 0
@[simp]
theorem filter.eventually_one {α : Type u_2} [has_one α] {p : α Prop} :
(∀ᶠ (x : α) in 1, p x) p 1
@[simp]
theorem filter.eventually_zero {α : Type u_2} [has_zero α] {p : α Prop} :
(∀ᶠ (x : α) in 0, p x) p 0
@[simp]
theorem filter.tendsto_one {α : Type u_2} {β : Type u_3} [has_one α] {a : filter β} {f : β α} :
1 ∀ᶠ (x : β) in a, f x = 1
@[simp]
theorem filter.tendsto_zero {α : Type u_2} {β : Type u_3} [has_zero α] {a : filter β} {f : β α} :
0 ∀ᶠ (x : β) in a, f x = 0
@[simp]
theorem filter.one_prod_one {α : Type u_2} {β : Type u_3} [has_one α] [has_one β] :
1.prod 1 = 1
@[simp]
theorem filter.zero_sum_zero {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] :
0.prod 0 = 0
def filter.pure_zero_hom {α : Type u_2} [has_zero α] :
(filter α)

`pure` as a `zero_hom`.

Equations
def filter.pure_one_hom {α : Type u_2} [has_one α] :
(filter α)

`pure` as a `one_hom`.

Equations
@[simp]
theorem filter.coe_pure_zero_hom {α : Type u_2} [has_zero α] :
@[simp]
theorem filter.coe_pure_one_hom {α : Type u_2} [has_one α] :
@[simp]
theorem filter.pure_zero_hom_apply {α : Type u_2} [has_zero α] (a : α) :
@[simp]
theorem filter.pure_one_hom_apply {α : Type u_2} [has_one α] (a : α) :
@[protected, simp]
theorem filter.map_one {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_one α] [has_one β] [ β] (φ : F) :
1 = 1
@[protected, simp]
theorem filter.map_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] (φ : F) :
0 = 0

### Filter negation/inversion #

@[protected, instance]
def filter.has_inv {α : Type u_2} [has_inv α] :

The inverse of a filter is the pointwise preimage under `⁻¹` of its sets.

Equations
@[protected, instance]
def filter.has_neg {α : Type u_2} [has_neg α] :

The negation of a filter is the pointwise preimage under `-` of its sets.

Equations
@[protected, simp]
theorem filter.map_neg {α : Type u_2} [has_neg α] {f : filter α} :
@[protected, simp]
theorem filter.map_inv {α : Type u_2} [has_inv α] {f : filter α} :
theorem filter.mem_inv {α : Type u_2} [has_inv α] {f : filter α} {s : set α} :
theorem filter.mem_neg {α : Type u_2} [has_neg α] {f : filter α} {s : set α} :
s -f f
@[protected]
theorem filter.neg_le_neg {α : Type u_2} [has_neg α] {f g : filter α} (hf : f g) :
-f -g
@[protected]
theorem filter.inv_le_inv {α : Type u_2} [has_inv α] {f g : filter α} (hf : f g) :
@[simp]
theorem filter.inv_pure {α : Type u_2} [has_inv α] {a : α} :
@[simp]
theorem filter.neg_pure {α : Type u_2} [has_neg α] {a : α} :
@[simp]
theorem filter.neg_eq_bot_iff {α : Type u_2} [has_neg α] {f : filter α} :
-f = f =
@[simp]
theorem filter.inv_eq_bot_iff {α : Type u_2} [has_inv α] {f : filter α} :
@[simp]
theorem filter.ne_bot_inv_iff {α : Type u_2} [has_inv α] {f : filter α} :
@[simp]
theorem filter.ne_bot_neg_iff {α : Type u_2} [has_neg α] {f : filter α} :
theorem filter.ne_bot.neg {α : Type u_2} [has_neg α] {f : filter α} :
theorem filter.ne_bot.inv {α : Type u_2} [has_inv α] {f : filter α} :
theorem filter.neg_mem_neg {α : Type u_2} {f : filter α} {s : set α} (hs : s f) :
-s -f
theorem filter.inv_mem_inv {α : Type u_2} {f : filter α} {s : set α} (hs : s f) :
@[protected]
def filter.has_involutive_neg {α : Type u_2}  :

Negation is involutive on `filter α` if it is on `α`.

Equations
@[protected]
def filter.has_involutive_inv {α : Type u_2}  :

Inversion is involutive on `filter α` if it is on `α`.

Equations
@[protected, simp]
theorem filter.neg_le_neg_iff {α : Type u_2} {f g : filter α} :
-f -g f g
@[protected, simp]
theorem filter.inv_le_inv_iff {α : Type u_2} {f g : filter α} :
theorem filter.inv_le_iff_le_inv {α : Type u_2} {f g : filter α} :
theorem filter.neg_le_iff_le_neg {α : Type u_2} {f g : filter α} :
-f g f -g
@[simp]
theorem filter.inv_le_self {α : Type u_2} {f : filter α} :
@[simp]
theorem filter.neg_le_self {α : Type u_2} {f : filter α} :
-f f -f = f

### Filter addition/multiplication #

@[protected]
def filter.has_add {α : Type u_2} [has_add α] :

The filter `f + g` is generated by `{s + t | s ∈ f, t ∈ g}` in locale `pointwise`.

Equations
@[protected]
def filter.has_mul {α : Type u_2} [has_mul α] :

The filter `f * g` is generated by `{s * t | s ∈ f, t ∈ g}` in locale `pointwise`.

Equations
@[simp]
theorem filter.map₂_mul {α : Type u_2} [has_mul α] {f g : filter α} :
= f * g
@[simp]
theorem filter.map₂_add {α : Type u_2} [has_add α] {f g : filter α} :
= f + g
theorem filter.mem_mul {α : Type u_2} [has_mul α] {f g : filter α} {s : set α} :
s f * g (t₁ t₂ : set α), t₁ f t₂ g t₁ * t₂ s
theorem filter.mem_add {α : Type u_2} [has_add α] {f g : filter α} {s : set α} :
s f + g (t₁ t₂ : set α), t₁ f t₂ g t₁ + t₂ s
theorem filter.mul_mem_mul {α : Type u_2} [has_mul α] {f g : filter α} {s t : set α} :
s f t g s * t f * g
theorem filter.add_mem_add {α : Type u_2} [has_add α] {f g : filter α} {s t : set α} :
s f t g s + t f + g
@[simp]
theorem filter.bot_add {α : Type u_2} [has_add α] {g : filter α} :
@[simp]
theorem filter.bot_mul {α : Type u_2} [has_mul α] {g : filter α} :
@[simp]
theorem filter.add_bot {α : Type u_2} [has_add α] {f : filter α} :
@[simp]
theorem filter.mul_bot {α : Type u_2} [has_mul α] {f : filter α} :
@[simp]
theorem filter.add_eq_bot_iff {α : Type u_2} [has_add α] {f g : filter α} :
f + g = f = g =
@[simp]
theorem filter.mul_eq_bot_iff {α : Type u_2} [has_mul α] {f g : filter α} :
f * g = f = g =
@[simp]
theorem filter.mul_ne_bot_iff {α : Type u_2} [has_mul α] {f g : filter α} :
@[simp]
theorem filter.add_ne_bot_iff {α : Type u_2} [has_add α] {f g : filter α} :
theorem filter.ne_bot.mul {α : Type u_2} [has_mul α] {f g : filter α} :
theorem filter.ne_bot.add {α : Type u_2} [has_add α] {f g : filter α} :
theorem filter.ne_bot.of_add_left {α : Type u_2} [has_add α] {f g : filter α} :
(f + g).ne_bot f.ne_bot
theorem filter.ne_bot.of_mul_left {α : Type u_2} [has_mul α] {f g : filter α} :
(f * g).ne_bot f.ne_bot
theorem filter.ne_bot.of_add_right {α : Type u_2} [has_add α] {f g : filter α} :
(f + g).ne_bot g.ne_bot
theorem filter.ne_bot.of_mul_right {α : Type u_2} [has_mul α] {f g : filter α} :
(f * g).ne_bot g.ne_bot
@[simp]
theorem filter.pure_mul {α : Type u_2} [has_mul α] {g : filter α} {a : α} :
= g
@[simp]
theorem filter.pure_add {α : Type u_2} [has_add α] {g : filter α} {a : α} :
= g
@[simp]
theorem filter.add_pure {α : Type u_2} [has_add α] {f : filter α} {b : α} :
= filter.map (λ (_x : α), _x + b) f
@[simp]
theorem filter.mul_pure {α : Type u_2} [has_mul α] {f : filter α} {b : α} :
= filter.map (λ (_x : α), _x * b) f
@[simp]
theorem filter.pure_mul_pure {α : Type u_2} [has_mul α] {a b : α} :
@[simp]
theorem filter.pure_add_pure {α : Type u_2} [has_add α] {a b : α} :
@[simp]
theorem filter.le_mul_iff {α : Type u_2} [has_mul α] {f g h : filter α} :
h f * g ⦃s : set α⦄, s f ⦃t : set α⦄, t g s * t h
@[simp]
theorem filter.le_add_iff {α : Type u_2} [has_add α] {f g h : filter α} :
h f + g ⦃s : set α⦄, s f ⦃t : set α⦄, t g s + t h
@[protected, instance]
def filter.covariant_add {α : Type u_2} [has_add α] :
@[protected, instance]
def filter.covariant_mul {α : Type u_2} [has_mul α] :
@[protected, instance]
def filter.covariant_swap_add {α : Type u_2} [has_add α] :
@[protected, instance]
def filter.covariant_swap_mul {α : Type u_2} [has_mul α] :
@[protected]
theorem filter.map_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_mul β] {f₁ f₂ : filter α} [ β] (m : F) :
(f₁ * f₂) = f₁ * f₂
@[protected]
theorem filter.map_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_add α] [has_add β] {f₁ f₂ : filter α} [ β] (m : F) :
(f₁ + f₂) = f₁ + f₂
def filter.pure_add_hom {α : Type u_2} [has_add α] :
(filter α)

The singleton operation as an `add_hom`.

Equations
def filter.pure_mul_hom {α : Type u_2} [has_mul α] :

`pure` operation as a `mul_hom`.

Equations
@[simp]
theorem filter.coe_pure_add_hom {α : Type u_2} [has_add α] :
@[simp]
theorem filter.coe_pure_mul_hom {α : Type u_2} [has_mul α] :
@[simp]
theorem filter.pure_mul_hom_apply {α : Type u_2} [has_mul α] (a : α) :
@[simp]
theorem filter.pure_add_hom_apply {α : Type u_2} [has_add α] (a : α) :

### Filter subtraction/division #

@[protected]
def filter.has_sub {α : Type u_2} [has_sub α] :

The filter `f - g` is generated by `{s - t | s ∈ f, t ∈ g}` in locale `pointwise`.

Equations
@[protected]
def filter.has_div {α : Type u_2} [has_div α] :

The filter `f / g` is generated by `{s / t | s ∈ f, t ∈ g}` in locale `pointwise`.

Equations
@[simp]
theorem filter.map₂_sub {α : Type u_2} [has_sub α] {f g : filter α} :
= f - g
@[simp]
theorem filter.map₂_div {α : Type u_2} [has_div α] {f g : filter α} :
= f / g
theorem filter.mem_sub {α : Type u_2} [has_sub α] {f g : filter α} {s : set α} :
s f - g (t₁ t₂ : set α), t₁ f t₂ g t₁ - t₂ s
theorem filter.mem_div {α : Type u_2} [has_div α] {f g : filter α} {s : set α} :
s f / g (t₁ t₂ : set α), t₁ f t₂ g t₁ / t₂ s
theorem filter.div_mem_div {α : Type u_2} [has_div α] {f g : filter α} {s t : set α} :
s f t g s / t f / g
theorem filter.sub_mem_sub {α : Type u_2} [has_sub α] {f g : filter α} {s t : set α} :
s f t g s - t f - g
@[simp]
theorem filter.bot_sub {α : Type u_2} [has_sub α] {g : filter α} :
@[simp]
theorem filter.bot_div {α : Type u_2} [has_div α] {g : filter α} :
@[simp]
theorem filter.div_bot {α : Type u_2} [has_div α] {f : filter α} :
@[simp]
theorem filter.sub_bot {α : Type u_2} [has_sub α] {f : filter α} :
@[simp]
theorem filter.sub_eq_bot_iff {α : Type u_2} [has_sub α] {f g : filter α} :
f - g = f = g =
@[simp]
theorem filter.div_eq_bot_iff {α : Type u_2} [has_div α] {f g : filter α} :
f / g = f = g =
@[simp]
theorem filter.div_ne_bot_iff {α : Type u_2} [has_div α] {f g : filter α} :
@[simp]
theorem filter.sub_ne_bot_iff {α : Type u_2} [has_sub α] {f g : filter α} :
theorem filter.ne_bot.sub {α : Type u_2} [has_sub α] {f g : filter α} :
theorem filter.ne_bot.div {α : Type u_2} [has_div α] {f g : filter α} :
theorem filter.ne_bot.of_div_left {α : Type u_2} [has_div α] {f g : filter α} :
(f / g).ne_bot f.ne_bot
theorem filter.ne_bot.of_sub_left {α : Type u_2} [has_sub α] {f g : filter α} :
(f - g).ne_bot f.ne_bot
theorem filter.ne_bot.of_div_right {α : Type u_2} [has_div α] {f g : filter α} :
(f / g).ne_bot g.ne_bot
theorem filter.ne_bot.of_sub_right {α : Type u_2} [has_sub α] {f g : filter α} :
(f - g).ne_bot g.ne_bot
@[simp]
theorem filter.pure_div {α : Type u_2} [has_div α] {g : filter α} {a : α} :
= g
@[simp]
theorem filter.pure_sub {α : Type u_2} [has_sub α] {g : filter α} {a : α} :
= g
@[simp]
theorem filter.div_pure {α : Type u_2} [has_div α] {f : filter α} {b : α} :
= filter.map (λ (_x : α), _x / b) f
@[simp]
theorem filter.sub_pure {α : Type u_2} [has_sub α] {f : filter α} {b : α} :
= filter.map (λ (_x : α), _x - b) f
@[simp]
theorem filter.pure_sub_pure {α : Type u_2} [has_sub α] {a b : α} :
@[simp]
theorem filter.pure_div_pure {α : Type u_2} [has_div α] {a b : α} :
@[protected]
theorem filter.div_le_div {α : Type u_2} [has_div α] {f₁ f₂ g₁ g₂ : filter α} :
f₁ f₂ g₁ g₂ f₁ / g₁ f₂ / g₂
@[protected]
theorem filter.sub_le_sub {α : Type u_2} [has_sub α] {f₁ f₂ g₁ g₂ : filter α} :
f₁ f₂ g₁ g₂ f₁ - g₁ f₂ - g₂
@[protected]
theorem filter.div_le_div_left {α : Type u_2} [has_div α] {f g₁ g₂ : filter α} :
g₁ g₂ f / g₁ f / g₂
@[protected]
theorem filter.sub_le_sub_left {α : Type u_2} [has_sub α] {f g₁ g₂ : filter α} :
g₁ g₂ f - g₁ f - g₂
@[protected]
theorem filter.div_le_div_right {α : Type u_2} [has_div α] {f₁ f₂ g : filter α} :
f₁ f₂ f₁ / g f₂ / g
@[protected]
theorem filter.sub_le_sub_right {α : Type u_2} [has_sub α] {f₁ f₂ g : filter α} :
f₁ f₂ f₁ - g f₂ - g
@[protected, simp]
theorem filter.le_sub_iff {α : Type u_2} [has_sub α] {f g h : filter α} :
h f - g ⦃s : set α⦄, s f ⦃t : set α⦄, t g s - t h
@[protected, simp]
theorem filter.le_div_iff {α : Type u_2} [has_div α] {f g h : filter α} :
h f / g ⦃s : set α⦄, s f ⦃t : set α⦄, t g s / t h
@[protected, instance]
def filter.covariant_sub {α : Type u_2} [has_sub α] :
@[protected, instance]
def filter.covariant_div {α : Type u_2} [has_div α] :
@[protected, instance]
def filter.covariant_swap_sub {α : Type u_2} [has_sub α] :
@[protected, instance]
def filter.covariant_swap_div {α : Type u_2} [has_div α] :
@[protected]
def filter.has_nsmul {α : Type u_2} [has_zero α] [has_add α] :
(filter α)

Repeated pointwise addition (not the same as pointwise repeated addition!) of a `filter`. See Note [pointwise nat action].

Equations
@[protected]
def filter.has_npow {α : Type u_2} [has_one α] [has_mul α] :

Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a `filter`. See Note [pointwise nat action].

Equations
@[protected]
def filter.has_zsmul {α : Type u_2} [has_zero α] [has_add α] [has_neg α] :
(filter α)

Repeated pointwise addition/subtraction (not the same as pointwise repeated addition/subtraction!) of a `filter`. See Note [pointwise nat action].

Equations
@[protected]
def filter.has_zpow {α : Type u_2} [has_one α] [has_mul α] [has_inv α] :

Repeated pointwise multiplication/division (not the same as pointwise repeated multiplication/division!) of a `filter`. See Note [pointwise nat action].

Equations
@[protected]
def filter.semigroup {α : Type u_2} [semigroup α] :

`filter α` is a `semigroup` under pointwise operations if `α` is.

Equations
@[protected]
def filter.add_semigroup {α : Type u_2}  :

`filter α` is an `add_semigroup` under pointwise operations if `α` is.

Equations
@[protected]
def filter.comm_semigroup {α : Type u_2}  :

`filter α` is a `comm_semigroup` under pointwise operations if `α` is.

Equations
@[protected]
def filter.add_comm_semigroup {α : Type u_2}  :

`filter α` is an `add_comm_semigroup` under pointwise operations if `α` is.

Equations
@[protected]
def filter.add_zero_class {α : Type u_2}  :

`filter α` is an `add_zero_class` under pointwise operations if `α` is.

Equations
@[protected]
def filter.mul_one_class {α : Type u_2}  :

`filter α` is a `mul_one_class` under pointwise operations if `α` is.

Equations
def filter.map_add_monoid_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (φ : F) :

If `φ : α →+ β` then `map_add_monoid_hom φ` is the monoid homomorphism `filter α →+ filter β` induced by `map φ`.

Equations
def filter.map_monoid_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (φ : F) :

If `φ : α →* β` then `map_monoid_hom φ` is the monoid homomorphism `filter α →* filter β` induced by `map φ`.

Equations
theorem filter.comap_add_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (m : F) {f g : filter β} :
+ (f + g)
theorem filter.comap_mul_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (m : F) {f g : filter β} :
* (f * g)
theorem filter.tendsto.add_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (m : F) {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
f₁ f₂ g₁ g₂ (f₁ + g₁) (f₂ + g₂)
theorem filter.tendsto.mul_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (m : F) {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
f₁ f₂ g₁ g₂ (f₁ * g₁) (f₂ * g₂)
def filter.pure_monoid_hom {α : Type u_2}  :
α →*

`pure` as a `monoid_hom`.

Equations
def filter.pure_add_monoid_hom {α : Type u_2}  :
α →+

`pure` as an `add_monoid_hom`.

Equations
@[simp]
theorem filter.coe_pure_add_monoid_hom {α : Type u_2}  :
@[simp]
theorem filter.coe_pure_monoid_hom {α : Type u_2}  :
@[simp]
theorem filter.pure_monoid_hom_apply {α : Type u_2} (a : α) :
@[simp]
theorem filter.pure_add_monoid_hom_apply {α : Type u_2} (a : α) :
@[protected]
def filter.add_monoid {α : Type u_2} [add_monoid α] :

`filter α` is an `add_monoid` under pointwise operations if `α` is.

Equations
@[protected]
def filter.monoid {α : Type u_2} [monoid α] :

`filter α` is a `monoid` under pointwise operations if `α` is.

Equations
theorem filter.pow_mem_pow {α : Type u_2} [monoid α] {f : filter α} {s : set α} (hs : s f) (n : ) :
s ^ n f ^ n
theorem filter.nsmul_mem_nsmul {α : Type u_2} [add_monoid α] {f : filter α} {s : set α} (hs : s f) (n : ) :
n s n f
@[simp]
theorem filter.nsmul_bot {α : Type u_2} [add_monoid α] {n : } (hn : n 0) :
@[simp]
theorem filter.bot_pow {α : Type u_2} [monoid α] {n : } (hn : n 0) :
theorem filter.mul_top_of_one_le {α : Type u_2} [monoid α] {f : filter α} (hf : 1 f) :
theorem filter.add_top_of_nonneg {α : Type u_2} [add_monoid α] {f : filter α} (hf : 0 f) :
theorem filter.top_mul_of_one_le {α : Type u_2} [monoid α] {f : filter α} (hf : 1 f) :
theorem filter.top_add_of_nonneg {α : Type u_2} [add_monoid α] {f : filter α} (hf : 0 f) :
@[simp]
theorem filter.top_mul_top {α : Type u_2} [monoid α] :
@[simp]
theorem filter.top_add_top {α : Type u_2} [add_monoid α] :
theorem filter.nsmul_top {α : Type u_1} [add_monoid α] {n : } :
n 0 n =
theorem filter.top_pow {α : Type u_2} [monoid α] {n : } :
n 0 ^ n =
@[protected]
theorem is_unit.filter {α : Type u_2} [monoid α] {a : α} :
@[protected]
theorem is_add_unit.filter {α : Type u_2} [add_monoid α] {a : α} :
@[protected]
def filter.comm_monoid {α : Type u_2} [comm_monoid α] :

`filter α` is a `comm_monoid` under pointwise operations if `α` is.

Equations
@[protected]
def filter.add_comm_monoid {α : Type u_2}  :

`filter α` is an `add_comm_monoid` under pointwise operations if `α` is.

Equations
@[protected]
theorem filter.mul_eq_one_iff {α : Type u_2} {f g : filter α} :
f * g = 1 (a b : α), a * b = 1
@[protected]
theorem filter.add_eq_zero_iff {α : Type u_2} {f g : filter α} :
f + g = 0 (a b : α), a + b = 0
@[protected]
def filter.division_monoid {α : Type u_2}  :

`filter α` is a division monoid under pointwise operations if `α` is.

Equations
@[protected]
def filter.subtraction_monoid {α : Type u_2}  :

`filter α` is a subtraction monoid under pointwise operations if `α` is.

Equations
theorem filter.is_unit_iff {α : Type u_2} {f : filter α} :
(a : α),
theorem filter.is_add_unit_iff {α : Type u_2} {f : filter α} :
(a : α),
@[protected]
def filter.division_comm_monoid {α : Type u_2}  :

`filter α` is a commutative division monoid under pointwise operations if `α` is.

Equations
@[protected]

`filter α` is a commutative subtraction monoid under pointwise operations if `α` is.

Equations
@[protected]
def filter.has_distrib_neg {α : Type u_2} [has_mul α]  :

`filter α` has distributive negation if `α` has.

Equations

Note that `filter α` is not a `distrib` because `f * g + f * h` has cross terms that `f * (g + h)` lacks.

theorem filter.mul_add_subset {α : Type u_2} [distrib α] {f g h : filter α} :
f * (g + h) f * g + f * h
theorem filter.add_mul_subset {α : Type u_2} [distrib α] {f g h : filter α} :
(f + g) * h f * h + g * h

Note that `filter` is not a `mul_zero_class` because `0 * ⊥ ≠ 0`.

theorem filter.ne_bot.mul_zero_nonneg {α : Type u_2} {f : filter α} (hf : f.ne_bot) :
0 f * 0
theorem filter.ne_bot.zero_mul_nonneg {α : Type u_2} {g : filter α} (hg : g.ne_bot) :
0 0 * g

Note that `filter α` is not a group because `f / f ≠ 1` in general

@[protected, simp]
theorem filter.nonneg_sub_iff {α : Type u_2} [add_group α] {f g : filter α} :
0 f - g ¬ g
@[protected, simp]
theorem filter.one_le_div_iff {α : Type u_2} [group α] {f g : filter α} :
1 f / g ¬ g
theorem filter.not_nonneg_sub_iff {α : Type u_2} [add_group α] {f g : filter α} :
¬0 f - g g
theorem filter.not_one_le_div_iff {α : Type u_2} [group α] {f g : filter α} :
¬1 f / g g
theorem filter.ne_bot.one_le_div {α : Type u_2} [group α] {f : filter α} (h : f.ne_bot) :
1 f / f
theorem filter.ne_bot.nonneg_sub {α : Type u_2} [add_group α] {f : filter α} (h : f.ne_bot) :
0 f - f
theorem filter.is_unit_pure {α : Type u_2} [group α] (a : α) :
theorem filter.is_add_unit_pure {α : Type u_2} [add_group α] (a : α) :
@[simp]
theorem filter.is_unit_iff_singleton {α : Type u_2} [group α] {f : filter α} :
(a : α),
theorem filter.map_neg' {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [ β] (m : F) {f : filter α} :
(-f) = - f
theorem filter.map_inv' {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [ β] (m : F) {f : filter α} :
= f)⁻¹
theorem filter.tendsto.neg_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [ β] (m : F) {f₁ : filter α} {f₂ : filter β} :
f₁ f₂ (-f₁) (-f₂)
theorem filter.tendsto.inv_inv {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [ β] (m : F) {f₁ : filter α} {f₂ : filter β} :
f₁ f₂ f₂⁻¹
@[protected]
theorem filter.map_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [ β] (m : F) {f g : filter α} :
(f - g) = f - g
@[protected]
theorem filter.map_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [ β] (m : F) {f g : filter α} :
(f / g) = f / g
theorem filter.tendsto.div_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [ β] (m : F) {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
f₁ f₂ g₁ g₂ (f₁ / g₁) (f₂ / g₂)
theorem filter.tendsto.sub_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [ β] (m : F) {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
f₁ f₂ g₁ g₂ (f₁ - g₁) (f₂ - g₂)
theorem filter.ne_bot.div_zero_nonneg {α : Type u_2} {f : filter α} (hf : f.ne_bot) :
0 f / 0
theorem filter.ne_bot.zero_div_nonneg {α : Type u_2} {g : filter α} (hg : g.ne_bot) :
0 0 / g

### Scalar addition/multiplication of filters #

@[protected]
def filter.has_smul {α : Type u_2} {β : Type u_3} [ β] :

The filter `f • g` is generated by `{s • t | s ∈ f, t ∈ g}` in locale `pointwise`.

Equations
@[protected]
def filter.has_vadd {α : Type u_2} {β : Type u_3} [ β] :

The filter `f +ᵥ g` is generated by `{s +ᵥ t | s ∈ f, t ∈ g}` in locale `pointwise`.

Equations
@[simp]
theorem filter.map₂_smul {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
= f g
@[simp]
theorem filter.map₂_vadd {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
= f +ᵥ g
theorem filter.mem_smul {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} {t : set β} :
t f g (t₁ : set α) (t₂ : set β), t₁ f t₂ g t₁ t₂ t
theorem filter.mem_vadd {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} {t : set β} :
t f +ᵥ g (t₁ : set α) (t₂ : set β), t₁ f t₂ g t₁ +ᵥ t₂ t
theorem filter.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} {s : set α} {t : set β} :
s f t g s +ᵥ t f +ᵥ g
theorem filter.smul_mem_smul {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} {s : set α} {t : set β} :
s f t g s t f g
@[simp]
theorem filter.bot_smul {α : Type u_2} {β : Type u_3} [ β] {g : filter β} :
@[simp]
theorem filter.bot_vadd {α : Type u_2} {β : Type u_3} [ β] {g : filter β} :
@[simp]
theorem filter.vadd_bot {α : Type u_2} {β : Type u_3} [ β] {f : filter α} :
@[simp]
theorem filter.smul_bot {α : Type u_2} {β : Type u_3} [ β] {f : filter α} :
@[simp]
theorem filter.smul_eq_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
f g = f = g =
@[simp]
theorem filter.vadd_eq_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
f +ᵥ g = f = g =
@[simp]
theorem filter.smul_ne_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
@[simp]
theorem filter.vadd_ne_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
theorem filter.ne_bot.smul {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
theorem filter.ne_bot.vadd {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
theorem filter.ne_bot.of_smul_left {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
theorem filter.ne_bot.of_vadd_left {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
theorem filter.ne_bot.of_vadd_right {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
theorem filter.ne_bot.of_smul_right {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g : filter β} :
@[simp]
theorem filter.pure_vadd {α : Type u_2} {β : Type u_3} [ β] {g : filter β} {a : α} :
= g
@[simp]
theorem filter.pure_smul {α : Type u_2} {β : Type u_3} [ β] {g : filter β} {a : α} :
= g
@[simp]
theorem filter.smul_pure {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {b : β} :
= filter.map (λ (_x : α), _x b) f
@[simp]
theorem filter.vadd_pure {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {b : β} :
= filter.map (λ (_x : α), _x +ᵥ b) f
@[simp]
theorem filter.pure_vadd_pure {α : Type u_2} {β : Type u_3} [ β] {a : α} {b : β} :
@[simp]
theorem filter.pure_smul_pure {α : Type u_2} {β : Type u_3} [ β] {a : α} {b : β} :
theorem filter.smul_le_smul {α : Type u_2} {β : Type u_3} [ β] {f₁ f₂ : filter α} {g₁ g₂ : filter β} :
f₁ f₂ g₁ g₂ f₁ g₁ f₂ g₂
theorem filter.vadd_le_vadd {α : Type u_2} {β : Type u_3} [ β] {f₁ f₂ : filter α} {g₁ g₂ : filter β} :
f₁ f₂ g₁ g₂ f₁ +ᵥ g₁ f₂ +ᵥ g₂
theorem filter.vadd_le_vadd_left {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g₁ g₂ : filter β} :
g₁ g₂ f +ᵥ g₁ f +ᵥ g₂
theorem filter.smul_le_smul_left {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g₁ g₂ : filter β} :
g₁ g₂ f g₁ f g₂
theorem filter.smul_le_smul_right {α : Type u_2} {β : Type u_3} [ β] {f₁ f₂ : filter α} {g : filter β} :
f₁ f₂ f₁ g f₂ g
theorem filter.vadd_le_vadd_right {α : Type u_2} {β : Type u_3} [ β] {f₁ f₂ : filter α} {g : filter β} :
f₁ f₂ f₁ +ᵥ g f₂ +ᵥ g
@[simp]
theorem filter.le_vadd_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g h : filter β} :
h f +ᵥ g ⦃s : set α⦄, s f ⦃t : set β⦄, t g s +ᵥ t h
@[simp]
theorem filter.le_smul_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter α} {g h : filter β} :
h f g ⦃s : set α⦄, s f ⦃t : set β⦄, t g s t h
@[protected, instance]
def filter.covariant_vadd {α : Type u_2} {β : Type u_3} [ β] :
@[protected, instance]
def filter.covariant_smul {α : Type u_2} {β : Type u_3} [ β] :

### Scalar subtraction of filters #

@[protected]
def filter.has_vsub {α : Type u_2} {β : Type u_3} [ β] :

The filter `f -ᵥ g` is generated by `{s -ᵥ t | s ∈ f, t ∈ g}` in locale `pointwise`.

Equations
@[simp]
theorem filter.map₂_vsub {α : Type u_2} {β : Type u_3} [ β] {f g : filter β} :
= f -ᵥ g
theorem filter.mem_vsub {α : Type u_2} {β : Type u_3} [ β] {f g : filter β} {s : set α} :
s f -ᵥ g (t₁ t₂ : set β), t₁ f t₂ g t₁ -ᵥ t₂ s
theorem filter.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [ β] {f g : filter β} {s t : set β} :
s f t g s -ᵥ t f -ᵥ g
@[simp]
theorem filter.bot_vsub {α : Type u_2} {β : Type u_3} [ β] {g : filter β} :
@[simp]
theorem filter.vsub_bot {α : Type u_2} {β : Type u_3} [ β] {f : filter β} :
@[simp]
theorem filter.vsub_eq_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f g : filter β} :
f -ᵥ g = f = g =
@[simp]
theorem filter.vsub_ne_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f g : filter β} :
theorem filter.ne_bot.vsub {α : Type u_2} {β : Type u_3} [ β] {f g : filter β} :
theorem filter.ne_bot.of_vsub_left {α : Type u_2} {β : Type u_3} [ β] {f g : filter β} :
theorem filter.ne_bot.of_vsub_right {α : Type u_2} {β : Type u_3} [ β] {f g : filter β} :
@[simp]
theorem filter.pure_vsub {α : Type u_2} {β : Type u_3} [ β] {g : filter β} {a : β} :
= g
@[simp]
theorem filter.vsub_pure {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {b : β} :
= filter.map (λ (_x : β), _x -ᵥ b) f
@[simp]
theorem filter.pure_vsub_pure {α : Type u_2} {β : Type u_3} [ β] {a b : β} :
theorem filter.vsub_le_vsub {α : Type u_2} {β : Type u_3} [ β] {f₁ f₂ g₁ g₂ : filter β} :
f₁ f₂ g₁ g₂ f₁ -ᵥ g₁ f₂ -ᵥ g₂
theorem filter.vsub_le_vsub_left {α : Type u_2} {β : Type u_3} [ β] {f g₁ g₂ : filter β} :
g₁ g₂ f -ᵥ g₁ f -ᵥ g₂
theorem filter.vsub_le_vsub_right {α : Type u_2} {β : Type u_3} [ β] {f₁ f₂ g : filter β} :
f₁ f₂ f₁ -ᵥ g f₂ -ᵥ g
@[simp]
theorem filter.le_vsub_iff {α : Type u_2} {β : Type u_3} [ β] {f g : filter β} {h : filter α} :
h f -ᵥ g ⦃s : set β⦄, s f ⦃t : set β⦄, t g s -ᵥ t h

### Translation/scaling of filters #

@[protected]
def filter.has_smul_filter {α : Type u_2} {β : Type u_3} [ β] :
(filter β)

`a • f` is the map of `f` under `a •` in locale `pointwise`.

Equations
@[protected]
def filter.has_vadd_filter {α : Type u_2} {β : Type u_3} [ β] :
(filter β)

`a +ᵥ f` is the map of `f` under `a +ᵥ` in locale `pointwise`.

Equations
@[simp]
theorem filter.map_smul {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
filter.map (λ (b : β), a b) f = a f
@[simp]
theorem filter.map_vadd {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
filter.map (λ (b : β), a +ᵥ b) f = a +ᵥ f
theorem filter.mem_smul_filter {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {s : set β} {a : α} :
s a f f
theorem filter.mem_vadd_filter {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {s : set β} {a : α} :
s a +ᵥ f f
theorem filter.vadd_set_mem_vadd_filter {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {s : set β} {a : α} :
s f a +ᵥ s a +ᵥ f
theorem filter.smul_set_mem_smul_filter {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {s : set β} {a : α} :
s f a s a f
@[simp]
theorem filter.smul_filter_bot {α : Type u_2} {β : Type u_3} [ β] {a : α} :
@[simp]
theorem filter.vadd_filter_bot {α : Type u_2} {β : Type u_3} [ β] {a : α} :
@[simp]
theorem filter.vadd_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
a +ᵥ f = f =
@[simp]
theorem filter.smul_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
a f = f =
@[simp]
theorem filter.smul_filter_ne_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
@[simp]
theorem filter.vadd_filter_ne_bot_iff {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
theorem filter.ne_bot.vadd_filter {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
theorem filter.ne_bot.smul_filter {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
theorem filter.ne_bot.of_smul_filter {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
theorem filter.ne_bot.of_vadd_filter {α : Type u_2} {β : Type u_3} [ β] {f : filter β} {a : α} :
theorem filter.smul_filter_le_smul_filter {α : Type u_2} {β : Type u_3} [ β] {f₁ f₂ : filter β} {a : α} (hf : f₁ f₂) :
a f₁ a f₂
theorem filter.vadd_filter_le_vadd_filter {α : Type u_2} {β : Type u_3} [ β] {f₁ f₂ : filter β} {a : α} (hf : f₁ f₂) :
a +ᵥ f₁ a +ᵥ f₂
@[protected, instance]
def filter.covariant_smul_filter {α : Type u_2} {β : Type u_3} [ β] :
@[protected, instance]
def filter.covariant_vadd_filter {α : Type u_2} {β : Type u_3} [ β] :
@[protected, instance]
def filter.smul_comm_class_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(filter γ)
@[protected, instance]
def filter.vadd_comm_class_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(filter γ)
@[protected, instance]
def filter.smul_comm_class_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(filter β) (filter γ)
@[protected, instance]
def filter.vadd_comm_class_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(filter β) (filter γ)
@[protected, instance]
def filter.vadd_comm_class_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
β (filter γ)
@[protected, instance]
def filter.smul_comm_class_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
β (filter γ)
@[protected, instance]
def filter.vadd_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(filter β) (filter γ)
@[protected, instance]
def filter.smul_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(filter β) (filter γ)
@[protected, instance]
def filter.vadd_assoc_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(filter γ)
@[protected, instance]
def filter.is_scalar_tower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(filter γ)
@[protected, instance]
def filter.vadd_assoc_class' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(filter β) (filter γ)
@[protected, instance]
def filter.is_scalar_tower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(filter β) (filter γ)
@[protected, instance]
def filter.vadd_assoc_class'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(filter β) (filter γ)
@[protected, instance]
def filter.is_scalar_tower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(filter β) (filter γ)
@[protected, instance]
def filter.is_central_vadd {α : Type u_2} {β : Type u_3} [ β] [ β] [ β] :
(filter β)
@[protected, instance]
def filter.is_central_scalar {α : Type u_2} {β : Type u_3} [ β] [ β] [ β] :
(filter β)
@[protected]
def filter.add_action {α : Type u_2} {β : Type u_3} [add_monoid α] [ β] :

An additive action of an additive monoid `α` on a type `β` gives an additive action of `filter α` on `filter β`

Equations
@[protected]
def filter.mul_action {α : Type u_2} {β : Type u_3} [monoid α] [ β] :

A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of `filter α` on `filter β`.

Equations
@[protected]
def filter.mul_action_filter {α : Type u_2} {β : Type u_3} [monoid α] [ β] :
(filter β)

A multiplicative action of a monoid on a type `β` gives a multiplicative action on `filter β`.

Equations
@[protected]
def filter.add_action_filter {α : Type u_2} {β : Type u_3} [add_monoid α] [ β] :
(filter β)

An additive action of an additive monoid on a type `β` gives an additive action on `filter β`.

Equations
@[protected]
def filter.distrib_mul_action_filter {α : Type u_2} {β : Type u_3} [monoid α] [add_monoid β] [ β] :
(filter β)

A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive multiplicative action on `filter β`.

Equations
@[protected]
def filter.mul_distrib_mul_action_filter {α : Type u_2} {β : Type u_3} [monoid α] [monoid β]  :

A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `set β`.

Equations

Note that we have neither `smul_with_zero α (filter β)` nor `smul_with_zero (filter α) (filter β)` because `0 * ⊥ ≠ 0`.

theorem filter.ne_bot.smul_zero_nonneg {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] {f : filter α} (hf : f.ne_bot) :
0 f 0
theorem filter.ne_bot.zero_smul_nonneg {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] {g : filter β} (hg : g.ne_bot) :
0 0 g
theorem filter.zero_smul_filter_nonpos {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] {g : filter β} :
0 g 0
theorem filter.zero_smul_filter {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] {g : filter β} (hg : g.ne_bot) :
0 g = 0