# Pointwise operations on filters #

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.instZero`): Pure filter at `0 : α`, or alternatively principal filter at `0 : Set α`.
- `1` (`Filter.instOne`): Pure filter at `1 : α`, or alternatively principal filter at `1 : Set α`.
- `f + g` (`Filter.instAdd`): Addition, filter generated by all `s + t` where `s ∈ f` and `t ∈ g`.
- `f * g` (`Filter.instMul`): Multiplication, filter generated by all `s * t` where `s ∈ f` and `t ∈ g`.
- `-f` (`Filter.instNeg`): Negation, filter of all `-s` where `s ∈ f`.
- `f⁻¹` (`Filter.instInv`): Inversion, filter of all `s⁻¹` where `s ∈ f`.
- `f - g` (`Filter.instSub`): Subtraction, filter generated by all `s - t` where `s ∈ f` and `t ∈ g`.
- `f / g` (`Filter.instDiv`): Division, filter generated by all `s / t` where `s ∈ f` and `t ∈ g`.
- `f +ᵥ g` (`Filter.instVAdd`): Scalar addition, filter generated by all `s +ᵥ t` where `s ∈ f` and `t ∈ g`.
- `f -ᵥ g` (`Filter.instVSub`): Scalar subtraction, filter generated by all `s -ᵥ t` where `s ∈ f` and `t ∈ g`.
- `f • g` (`Filter.instSMul`): Scalar multiplication, filter generated by all `s • t` where `s ∈ f` and `t ∈ g`.
- `a +ᵥ f` (`Filter.instVAddFilter`): Translation, filter of all `a +ᵥ s` where `s ∈ f`.
- `a • f` (`Filter.instSMulFilter`): 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 scope `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 scope 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 #

source
def Filter.instOne {α : Type u_2} [One α] :
One (Filter α)

`1 : Filter α` is defined as the filter of sets containing `1 : α` in scope `Pointwise`.

Equations

- Filter.instOne = { one := pure 1 }

Instances For

source
def Filter.instZero {α : Type u_2} [Zero α] :
Zero (Filter α)

`0 : Filter α` is defined as the filter of sets containing `0 : α` in scope `Pointwise`.

Equations

- Filter.instZero = { zero := pure 0 }

Instances For

source
@[simp]
theorem Filter.mem_one {α : Type u_2} [One α] {s : Set α} :
s ∈ 1 ↔ 1 ∈ s
source
@[simp]
theorem Filter.mem_zero {α : Type u_2} [Zero α] {s : Set α} :
s ∈ 0 ↔ 0 ∈ s
source
theorem Filter.one_mem_one {α : Type u_2} [One α] :
1 ∈ 1
source
theorem Filter.zero_mem_zero {α : Type u_2} [Zero α] :
0 ∈ 0
source
@[simp]
theorem Filter.pure_one {α : Type u_2} [One α] :
pure 1 = 1
source
@[simp]
theorem Filter.pure_zero {α : Type u_2} [Zero α] :
pure 0 = 0
source
@[simp]
theorem Filter.one_prod {α : Type u_2} {β : Type u_3} [One α] {l : Filter β} :
1 ×ˢ l = map (fun (x : β) => (1, x)) l
source
@[simp]
theorem Filter.zero_prod {α : Type u_2} {β : Type u_3} [Zero α] {l : Filter β} :
0 ×ˢ l = map (fun (x : β) => (0, x)) l
source
@[simp]
theorem Filter.prod_one {α : Type u_2} {β : Type u_3} [One α] {l : Filter β} :
l ×ˢ 1 = map (fun (x : β) => (x, 1)) l
source
@[simp]
theorem Filter.prod_zero {α : Type u_2} {β : Type u_3} [Zero α] {l : Filter β} :
l ×ˢ 0 = map (fun (x : β) => (x, 0)) l
source
@[simp]
theorem Filter.principal_one {α : Type u_2} [One α] :
principal 1 = 1
source
@[simp]
theorem Filter.principal_zero {α : Type u_2} [Zero α] :
principal 0 = 0
source
theorem Filter.one_neBot {α : Type u_2} [One α] :
NeBot 1
source
theorem Filter.zero_neBot {α : Type u_2} [Zero α] :
NeBot 0
source
@[simp]
theorem Filter.map_one' {α : Type u_2} {β : Type u_3} [One α] (f : α → β) :
map f 1 = pure (f 1)
source
@[simp]
theorem Filter.map_zero' {α : Type u_2} {β : Type u_3} [Zero α] (f : α → β) :
map f 0 = pure (f 0)
source
@[simp]
theorem Filter.le_one_iff {α : Type u_2} [One α] {f : Filter α} :
f ≤ 1 ↔ 1 ∈ f
source
@[simp]
theorem Filter.nonpos_iff {α : Type u_2} [Zero α] {f : Filter α} :
f ≤ 0 ↔ 0 ∈ f
source
theorem Filter.NeBot.le_one_iff {α : Type u_2} [One α] {f : Filter α} (h : f.NeBot) :
f ≤ 1 ↔ f = 1
source
theorem Filter.NeBot.nonpos_iff {α : Type u_2} [Zero α] {f : Filter α} (h : f.NeBot) :
f ≤ 0 ↔ f = 0
source
@[simp]
theorem Filter.eventually_one {α : Type u_2} [One α] {p : α → Prop} :
(∀ᶠ (x : α) in 1, p x) ↔ p 1
source
@[simp]
theorem Filter.eventually_zero {α : Type u_2} [Zero α] {p : α → Prop} :
(∀ᶠ (x : α) in 0, p x) ↔ p 0
source
@[simp]
theorem Filter.tendsto_one {α : Type u_2} {β : Type u_3} [One α] {a : Filter β} {f : β → α} :
Tendsto f a 1 ↔ ∀ᶠ (x : β) in a, f x = 1
source
@[simp]
theorem Filter.tendsto_zero {α : Type u_2} {β : Type u_3} [Zero α] {a : Filter β} {f : β → α} :
Tendsto f a 0 ↔ ∀ᶠ (x : β) in a, f x = 0
source
theorem Filter.one_prod_one {α : Type u_2} {β : Type u_3} [One α] [One β] :
1 ×ˢ 1 = 1
source
theorem Filter.zero_prod_zero {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] :
0 ×ˢ 0 = 0
source
def Filter.pureOneHom {α : Type u_2} [One α] :
OneHom α (Filter α)

`pure` as a `OneHom`.

Equations

- Filter.pureOneHom = { toFun := pure, map_one' := ⋯ }

Instances For

source
def Filter.pureZeroHom {α : Type u_2} [Zero α] :
ZeroHom α (Filter α)

`pure` as a `ZeroHom`.

Equations

- Filter.pureZeroHom = { toFun := pure, map_zero' := ⋯ }

Instances For

source
@[simp]
theorem Filter.coe_pureOneHom {α : Type u_2} [One α] :
⇑pureOneHom = pure
source
@[simp]
theorem Filter.coe_pureZeroHom {α : Type u_2} [Zero α] :
⇑pureZeroHom = pure
source
@[simp]
theorem Filter.pureOneHom_apply {α : Type u_2} [One α] (a : α) :
pureOneHom a = pure a
source
@[simp]
theorem Filter.pureZeroHom_apply {α : Type u_2} [Zero α] (a : α) :
pureZeroHom a = pure a
source
theorem Filter.map_one {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [One β] [FunLike F α β] [OneHomClass F α β] (φ : F) :
map (⇑φ) 1 = 1
source
theorem Filter.map_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [FunLike F α β] [ZeroHomClass F α β] (φ : F) :
map (⇑φ) 0 = 0

### Filter negation/inversion #

source
def Filter.instInv {α : Type u_2} [Inv α] :
Inv (Filter α)

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

Equations

- Filter.instInv = { inv := Filter.map Inv.inv }

Instances For

source
def Filter.instNeg {α : Type u_2} [Neg α] :
Neg (Filter α)

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

Equations

- Filter.instNeg = { neg := Filter.map Neg.neg }

Instances For

source
@[simp]
theorem Filter.map_inv {α : Type u_2} [Inv α] {f : Filter α} :
map Inv.inv f = f⁻¹
source
@[simp]
theorem Filter.map_neg {α : Type u_2} [Neg α] {f : Filter α} :
map Neg.neg f = -f
source
theorem Filter.mem_inv {α : Type u_2} [Inv α] {f : Filter α} {s : Set α} :
s ∈ f⁻¹ ↔ Inv.inv ⁻¹' s ∈ f
source
theorem Filter.mem_neg {α : Type u_2} [Neg α] {f : Filter α} {s : Set α} :
s ∈ -f ↔ Neg.neg ⁻¹' s ∈ f
source
theorem Filter.inv_le_inv {α : Type u_2} [Inv α] {f g : Filter α} (hf : f ≤ g) :
f⁻¹ ≤ g⁻¹
source
theorem Filter.neg_le_neg {α : Type u_2} [Neg α] {f g : Filter α} (hf : f ≤ g) :
-f ≤ -g
source
@[simp]
theorem Filter.inv_pure {α : Type u_2} [Inv α] {a : α} :
(pure a)⁻¹ = pure a⁻¹
source
@[simp]
theorem Filter.neg_pure {α : Type u_2} [Neg α] {a : α} :
-pure a = pure (-a)
source
@[simp]
theorem Filter.inv_eq_bot_iff {α : Type u_2} [Inv α] {f : Filter α} :
f⁻¹ = ⊥ ↔ f = ⊥
source
@[simp]
theorem Filter.neg_eq_bot_iff {α : Type u_2} [Neg α] {f : Filter α} :
-f = ⊥ ↔ f = ⊥
source
@[simp]
theorem Filter.neBot_inv_iff {α : Type u_2} [Inv α] {f : Filter α} :
f⁻¹.NeBot ↔ f.NeBot
source
@[simp]
theorem Filter.neBot_neg_iff {α : Type u_2} [Neg α] {f : Filter α} :
(-f).NeBot ↔ f.NeBot
source
theorem Filter.NeBot.inv {α : Type u_2} [Inv α] {f : Filter α} :
f.NeBot → f⁻¹.NeBot
source
theorem Filter.NeBot.neg {α : Type u_2} [Neg α] {f : Filter α} :
f.NeBot → (-f).NeBot
source
theorem Filter.inv.instNeBot {α : Type u_2} [Inv α] {f : Filter α} [f.NeBot] :
f⁻¹.NeBot
source
theorem Filter.neg.instNeBot {α : Type u_2} [Neg α] {f : Filter α} [f.NeBot] :
(-f).NeBot
source
@[simp]
theorem Filter.comap_inv {α : Type u_2} [InvolutiveInv α] {f : Filter α} :
comap Inv.inv f = f⁻¹
source
@[simp]
theorem Filter.comap_neg {α : Type u_2} [InvolutiveNeg α] {f : Filter α} :
comap Neg.neg f = -f
source
theorem Filter.inv_mem_inv {α : Type u_2} [InvolutiveInv α] {f : Filter α} {s : Set α} (hs : s ∈ f) :
s⁻¹ ∈ f⁻¹
source
theorem Filter.neg_mem_neg {α : Type u_2} [InvolutiveNeg α] {f : Filter α} {s : Set α} (hs : s ∈ f) :
-s ∈ -f
source
theorem Filter.HasBasis.inv {α : Type u_2} [InvolutiveInv α] {f : Filter α} {ι : Sort u_7} {p : ι → Prop} {s : ι → Set α} (h : f.HasBasis p s) :
f⁻¹.HasBasis p fun (i : ι) => (s i)⁻¹
source
theorem Filter.HasBasis.neg {α : Type u_2} [InvolutiveNeg α] {f : Filter α} {ι : Sort u_7} {p : ι → Prop} {s : ι → Set α} (h : f.HasBasis p s) :
(-f).HasBasis p fun (i : ι) => -s i
source
def Filter.instInvolutiveInv {α : Type u_2} [InvolutiveInv α] :
InvolutiveInv (Filter α)

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

Equations

- Filter.instInvolutiveInv = { toInv := Filter.instInv, inv_inv := ⋯ }

Instances For

source
def Filter.instInvolutiveNeg {α : Type u_2} [InvolutiveNeg α] :
InvolutiveNeg (Filter α)

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

Equations

- Filter.instInvolutiveNeg = { toNeg := Filter.instNeg, neg_neg := ⋯ }

Instances For

source
@[simp]
theorem Filter.inv_le_inv_iff {α : Type u_2} [InvolutiveInv α] {f g : Filter α} :
f⁻¹ ≤ g⁻¹ ↔ f ≤ g
source
@[simp]
theorem Filter.neg_le_neg_iff {α : Type u_2} [InvolutiveNeg α] {f g : Filter α} :
-f ≤ -g ↔ f ≤ g
source
theorem Filter.inv_le_iff_le_inv {α : Type u_2} [InvolutiveInv α] {f g : Filter α} :
f⁻¹ ≤ g ↔ f ≤ g⁻¹
source
theorem Filter.neg_le_iff_le_neg {α : Type u_2} [InvolutiveNeg α] {f g : Filter α} :
-f ≤ g ↔ f ≤ -g
source
@[simp]
theorem Filter.inv_le_self {α : Type u_2} [InvolutiveInv α] {f : Filter α} :
f⁻¹ ≤ f ↔ f⁻¹ = f
source
@[simp]
theorem Filter.neg_le_self {α : Type u_2} [InvolutiveNeg α] {f : Filter α} :
-f ≤ f ↔ -f = f
source
@[simp]
theorem Filter.inv_atTop {G : Type u_7} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] :
atTop⁻¹ = atBot
source
@[simp]
theorem Filter.neg_atTop {G : Type u_7} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] :
-atTop = atBot

### Filter addition/multiplication #

source
def Filter.instMul {α : Type u_2} [Mul α] :
Mul (Filter α)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Filter.instAdd {α : Type u_2} [Add α] :
Add (Filter α)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Filter.HasBasis.mul {α : Type u_2} [Mul α] {f g : Filter α} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α} {pg : ιg → Prop} {sg : ιg → Set α} (hf : f.HasBasis pf sf) (hg : g.HasBasis pg sg) :
(f * g).HasBasis (fun (i : ιf × ιg) => pf i.1 ∧ pg i.2) fun (i : ιf × ιg) => sf i.1 * sg i.2
source
theorem Filter.HasBasis.add {α : Type u_2} [Add α] {f g : Filter α} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α} {pg : ιg → Prop} {sg : ιg → Set α} (hf : f.HasBasis pf sf) (hg : g.HasBasis pg sg) :
(f + g).HasBasis (fun (i : ιf × ιg) => pf i.1 ∧ pg i.2) fun (i : ιf × ιg) => sf i.1 + sg i.2
source
@[simp]
theorem Filter.map₂_mul {α : Type u_2} [Mul α] {f g : Filter α} :
map₂ (fun (x1 x2 : α) => x1 * x2) f g = f * g
source
@[simp]
theorem Filter.map₂_add {α : Type u_2} [Add α] {f g : Filter α} :
map₂ (fun (x1 x2 : α) => x1 + x2) f g = f + g
source
theorem Filter.mem_mul {α : Type u_2} [Mul α] {f g : Filter α} {s : Set α} :
s ∈ f * g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s
source
theorem Filter.mem_add {α : Type u_2} [Add α] {f g : Filter α} {s : Set α} :
s ∈ f + g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ + t₂ ⊆ s
source
theorem Filter.mul_mem_mul {α : Type u_2} [Mul α] {f g : Filter α} {s t : Set α} :
s ∈ f → t ∈ g → s * t ∈ f * g
source
theorem Filter.add_mem_add {α : Type u_2} [Add α] {f g : Filter α} {s t : Set α} :
s ∈ f → t ∈ g → s + t ∈ f + g
source
@[simp]
theorem Filter.bot_mul {α : Type u_2} [Mul α] {g : Filter α} :
⊥ * g = ⊥
source
@[simp]
theorem Filter.bot_add {α : Type u_2} [Add α] {g : Filter α} :
⊥ + g = ⊥
source
@[simp]
theorem Filter.mul_bot {α : Type u_2} [Mul α] {f : Filter α} :
f * ⊥ = ⊥
source
@[simp]
theorem Filter.add_bot {α : Type u_2} [Add α] {f : Filter α} :
f + ⊥ = ⊥
source
@[simp]
theorem Filter.mul_eq_bot_iff {α : Type u_2} [Mul α] {f g : Filter α} :
f * g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem Filter.add_eq_bot_iff {α : Type u_2} [Add α] {f g : Filter α} :
f + g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem Filter.mul_neBot_iff {α : Type u_2} [Mul α] {f g : Filter α} :
(f * g).NeBot ↔ f.NeBot ∧ g.NeBot
source
@[simp]
theorem Filter.add_neBot_iff {α : Type u_2} [Add α] {f g : Filter α} :
(f + g).NeBot ↔ f.NeBot ∧ g.NeBot
source
theorem Filter.NeBot.mul {α : Type u_2} [Mul α] {f g : Filter α} :
f.NeBot → g.NeBot → (f * g).NeBot
source
theorem Filter.NeBot.add {α : Type u_2} [Add α] {f g : Filter α} :
f.NeBot → g.NeBot → (f + g).NeBot
source
theorem Filter.NeBot.of_mul_left {α : Type u_2} [Mul α] {f g : Filter α} :
(f * g).NeBot → f.NeBot
source
theorem Filter.NeBot.of_add_left {α : Type u_2} [Add α] {f g : Filter α} :
(f + g).NeBot → f.NeBot
source
theorem Filter.NeBot.of_mul_right {α : Type u_2} [Mul α] {f g : Filter α} :
(f * g).NeBot → g.NeBot
source
theorem Filter.NeBot.of_add_right {α : Type u_2} [Add α] {f g : Filter α} :
(f + g).NeBot → g.NeBot
source
theorem Filter.mul.instNeBot {α : Type u_2} [Mul α] {f g : Filter α} [f.NeBot] [g.NeBot] :
(f * g).NeBot
source
theorem Filter.add.instNeBot {α : Type u_2} [Add α] {f g : Filter α} [f.NeBot] [g.NeBot] :
(f + g).NeBot
source
@[simp]
theorem Filter.pure_mul {α : Type u_2} [Mul α] {g : Filter α} {a : α} :
pure a * g = map (fun (x : α) => a * x) g
source
@[simp]
theorem Filter.pure_add {α : Type u_2} [Add α] {g : Filter α} {a : α} :
pure a + g = map (fun (x : α) => a + x) g
source
@[simp]
theorem Filter.mul_pure {α : Type u_2} [Mul α] {f : Filter α} {b : α} :
f * pure b = map (fun (x : α) => x * b) f
source
@[simp]
theorem Filter.add_pure {α : Type u_2} [Add α] {f : Filter α} {b : α} :
f + pure b = map (fun (x : α) => x + b) f
source
theorem Filter.pure_mul_pure {α : Type u_2} [Mul α] {a b : α} :
pure a * pure b = pure (a * b)
source
theorem Filter.pure_add_pure {α : Type u_2} [Add α] {a b : α} :
pure a + pure b = pure (a + b)
source
@[simp]
theorem Filter.le_mul_iff {α : Type u_2} [Mul α] {f g h : Filter α} :
h ≤ f * g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s * t ∈ h
source
@[simp]
theorem Filter.le_add_iff {α : Type u_2} [Add α] {f g h : Filter α} :
h ≤ f + g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s + t ∈ h
source
instance Filter.mulLeftMono {α : Type u_2} [Mul α] :
MulLeftMono (Filter α)
source
instance Filter.addLeftMono {α : Type u_2} [Add α] :
AddLeftMono (Filter α)
source
instance Filter.mulRightMono {α : Type u_2} [Mul α] :
MulRightMono (Filter α)
source
instance Filter.addRightMono {α : Type u_2} [Add α] :
AddRightMono (Filter α)
source
theorem Filter.map_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] {f₁ f₂ : Filter α} [FunLike F α β] [MulHomClass F α β] (m : F) :
map (⇑m) (f₁ * f₂) = map (⇑m) f₁ * map (⇑m) f₂
source
theorem Filter.map_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] {f₁ f₂ : Filter α} [FunLike F α β] [AddHomClass F α β] (m : F) :
map (⇑m) (f₁ + f₂) = map (⇑m) f₁ + map (⇑m) f₂
source
def Filter.pureMulHom {α : Type u_2} [Mul α] :
α →ₙ* Filter α

`pure` operation as a `MulHom`.

Equations

- Filter.pureMulHom = { toFun := pure, map_mul' := ⋯ }

Instances For

source
def Filter.pureAddHom {α : Type u_2} [Add α] :
α →ₙ+ Filter α

The singleton operation as an `AddHom`.

Equations

- Filter.pureAddHom = { toFun := pure, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Filter.coe_pureMulHom {α : Type u_2} [Mul α] :
⇑pureMulHom = pure
source
@[simp]
theorem Filter.coe_pureAddHom {α : Type u_2} [Add α] :
⇑pureAddHom = pure
source
@[simp]
theorem Filter.pureMulHom_apply {α : Type u_2} [Mul α] (a : α) :
pureMulHom a = pure a
source
@[simp]
theorem Filter.pureAddHom_apply {α : Type u_2} [Add α] (a : α) :
pureAddHom a = pure a

### Filter subtraction/division #

source
def Filter.instDiv {α : Type u_2} [Div α] :
Div (Filter α)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Filter.instSub {α : Type u_2} [Sub α] :
Sub (Filter α)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Filter.HasBasis.div {α : Type u_2} [Div α] {f g : Filter α} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α} {pg : ιg → Prop} {sg : ιg → Set α} (hf : f.HasBasis pf sf) (hg : g.HasBasis pg sg) :
(f / g).HasBasis (fun (i : ιf × ιg) => pf i.1 ∧ pg i.2) fun (i : ιf × ιg) => sf i.1 / sg i.2
source
theorem Filter.HasBasis.sub {α : Type u_2} [Sub α] {f g : Filter α} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α} {pg : ιg → Prop} {sg : ιg → Set α} (hf : f.HasBasis pf sf) (hg : g.HasBasis pg sg) :
(f - g).HasBasis (fun (i : ιf × ιg) => pf i.1 ∧ pg i.2) fun (i : ιf × ιg) => sf i.1 - sg i.2
source
@[simp]
theorem Filter.map₂_div {α : Type u_2} [Div α] {f g : Filter α} :
map₂ (fun (x1 x2 : α) => x1 / x2) f g = f / g
source
@[simp]
theorem Filter.map₂_sub {α : Type u_2} [Sub α] {f g : Filter α} :
map₂ (fun (x1 x2 : α) => x1 - x2) f g = f - g
source
theorem Filter.mem_div {α : Type u_2} [Div α] {f g : Filter α} {s : Set α} :
s ∈ f / g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s
source
theorem Filter.mem_sub {α : Type u_2} [Sub α] {f g : Filter α} {s : Set α} :
s ∈ f - g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ - t₂ ⊆ s
source
theorem Filter.div_mem_div {α : Type u_2} [Div α] {f g : Filter α} {s t : Set α} :
s ∈ f → t ∈ g → s / t ∈ f / g
source
theorem Filter.sub_mem_sub {α : Type u_2} [Sub α] {f g : Filter α} {s t : Set α} :
s ∈ f → t ∈ g → s - t ∈ f - g
source
@[simp]
theorem Filter.bot_div {α : Type u_2} [Div α] {g : Filter α} :
⊥ / g = ⊥
source
@[simp]
theorem Filter.bot_sub {α : Type u_2} [Sub α] {g : Filter α} :
⊥ - g = ⊥
source
@[simp]
theorem Filter.div_bot {α : Type u_2} [Div α] {f : Filter α} :
f / ⊥ = ⊥
source
@[simp]
theorem Filter.sub_bot {α : Type u_2} [Sub α] {f : Filter α} :
f - ⊥ = ⊥
source
@[simp]
theorem Filter.div_eq_bot_iff {α : Type u_2} [Div α] {f g : Filter α} :
f / g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem Filter.sub_eq_bot_iff {α : Type u_2} [Sub α] {f g : Filter α} :
f - g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem Filter.div_neBot_iff {α : Type u_2} [Div α] {f g : Filter α} :
(f / g).NeBot ↔ f.NeBot ∧ g.NeBot
source
@[simp]
theorem Filter.sub_neBot_iff {α : Type u_2} [Sub α] {f g : Filter α} :
(f - g).NeBot ↔ f.NeBot ∧ g.NeBot
source
theorem Filter.NeBot.div {α : Type u_2} [Div α] {f g : Filter α} :
f.NeBot → g.NeBot → (f / g).NeBot
source
theorem Filter.NeBot.sub {α : Type u_2} [Sub α] {f g : Filter α} :
f.NeBot → g.NeBot → (f - g).NeBot
source
theorem Filter.NeBot.of_div_left {α : Type u_2} [Div α] {f g : Filter α} :
(f / g).NeBot → f.NeBot
source
theorem Filter.NeBot.of_sub_left {α : Type u_2} [Sub α] {f g : Filter α} :
(f - g).NeBot → f.NeBot
source
theorem Filter.NeBot.of_div_right {α : Type u_2} [Div α] {f g : Filter α} :
(f / g).NeBot → g.NeBot
source
theorem Filter.NeBot.of_sub_right {α : Type u_2} [Sub α] {f g : Filter α} :
(f - g).NeBot → g.NeBot
source
theorem Filter.div.instNeBot {α : Type u_2} [Div α] {f g : Filter α} [f.NeBot] [g.NeBot] :
(f / g).NeBot
source
theorem Filter.sub.instNeBot {α : Type u_2} [Sub α] {f g : Filter α} [f.NeBot] [g.NeBot] :
(f - g).NeBot
source
@[simp]
theorem Filter.pure_div {α : Type u_2} [Div α] {g : Filter α} {a : α} :
pure a / g = map (fun (x : α) => a / x) g
source
@[simp]
theorem Filter.pure_sub {α : Type u_2} [Sub α] {g : Filter α} {a : α} :
pure a - g = map (fun (x : α) => a - x) g
source
@[simp]
theorem Filter.div_pure {α : Type u_2} [Div α] {f : Filter α} {b : α} :
f / pure b = map (fun (x : α) => x / b) f
source
@[simp]
theorem Filter.sub_pure {α : Type u_2} [Sub α] {f : Filter α} {b : α} :
f - pure b = map (fun (x : α) => x - b) f
source
theorem Filter.pure_div_pure {α : Type u_2} [Div α] {a b : α} :
pure a / pure b = pure (a / b)
source
theorem Filter.pure_sub_pure {α : Type u_2} [Sub α] {a b : α} :
pure a - pure b = pure (a - b)
source
theorem Filter.div_le_div {α : Type u_2} [Div α] {f₁ f₂ g₁ g₂ : Filter α} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ / g₁ ≤ f₂ / g₂
source
theorem Filter.sub_le_sub {α : Type u_2} [Sub α] {f₁ f₂ g₁ g₂ : Filter α} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ - g₁ ≤ f₂ - g₂
source
theorem Filter.div_le_div_left {α : Type u_2} [Div α] {f g₁ g₂ : Filter α} :
g₁ ≤ g₂ → f / g₁ ≤ f / g₂
source
theorem Filter.sub_le_sub_left {α : Type u_2} [Sub α] {f g₁ g₂ : Filter α} :
g₁ ≤ g₂ → f - g₁ ≤ f - g₂
source
theorem Filter.div_le_div_right {α : Type u_2} [Div α] {f₁ f₂ g : Filter α} :
f₁ ≤ f₂ → f₁ / g ≤ f₂ / g
source
theorem Filter.sub_le_sub_right {α : Type u_2} [Sub α] {f₁ f₂ g : Filter α} :
f₁ ≤ f₂ → f₁ - g ≤ f₂ - g
source
@[simp]
theorem Filter.le_div_iff {α : Type u_2} [Div α] {f g h : Filter α} :
h ≤ f / g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s / t ∈ h
source
@[simp]
theorem Filter.le_sub_iff {α : Type u_2} [Sub α] {f g h : Filter α} :
h ≤ f - g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s - t ∈ h
source
instance Filter.covariant_div {α : Type u_2} [Div α] :
CovariantClass (Filter α) (Filter α) (fun (x1 x2 : Filter α) => x1 / x2) fun (x1 x2 : Filter α) => x1 ≤ x2
source
instance Filter.covariant_sub {α : Type u_2} [Sub α] :
CovariantClass (Filter α) (Filter α) (fun (x1 x2 : Filter α) => x1 - x2) fun (x1 x2 : Filter α) => x1 ≤ x2
source
instance Filter.covariant_swap_div {α : Type u_2} [Div α] :
CovariantClass (Filter α) (Filter α) (Function.swap fun (x1 x2 : Filter α) => x1 / x2) fun (x1 x2 : Filter α) => x1 ≤ x2
source
instance Filter.covariant_swap_sub {α : Type u_2} [Sub α] :
CovariantClass (Filter α) (Filter α) (Function.swap fun (x1 x2 : Filter α) => x1 - x2) fun (x1 x2 : Filter α) => x1 ≤ x2
source
def Filter.instNSMul {α : Type u_2} [Zero α] [Add α] :
SMul ℕ (Filter α)

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

Equations

- Filter.instNSMul = { smul := nsmulRec }

Instances For

source
def Filter.instNPow {α : Type u_2} [One α] [Mul α] :
Pow (Filter α) ℕ

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

Equations

- Filter.instNPow = { pow := fun (s : Filter α) (n : ℕ) => npowRec n s }

Instances For

source
def Filter.instZSMul {α : Type u_2} [Zero α] [Add α] [Neg α] :
SMul ℤ (Filter α)

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

Equations

- Filter.instZSMul = { smul := zsmulRec }

Instances For

source
def Filter.instZPow {α : Type u_2} [One α] [Mul α] [Inv α] :
Pow (Filter α) ℤ

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

Equations

- Filter.instZPow = { pow := fun (s : Filter α) (n : ℤ) => zpowRec npowRec n s }

Instances For

source
def Filter.semigroup {α : Type u_2} [Semigroup α] :
Semigroup (Filter α)

`Filter α` is a `Semigroup` under pointwise operations if `α` is.

Equations

- Filter.semigroup = { toMul := Filter.instMul, mul_assoc := ⋯ }

Instances For

source
def Filter.addSemigroup {α : Type u_2} [AddSemigroup α] :
AddSemigroup (Filter α)

`Filter α` is an `AddSemigroup` under pointwise operations if `α` is.

Equations

- Filter.addSemigroup = { toAdd := Filter.instAdd, add_assoc := ⋯ }

Instances For

source
def Filter.commSemigroup {α : Type u_2} [CommSemigroup α] :
CommSemigroup (Filter α)

`Filter α` is a `CommSemigroup` under pointwise operations if `α` is.

Equations

- Filter.commSemigroup = { toSemigroup := Filter.semigroup, mul_comm := ⋯ }

Instances For

source
def Filter.addCommSemigroup {α : Type u_2} [AddCommSemigroup α] :
AddCommSemigroup (Filter α)

`Filter α` is an `AddCommSemigroup` under pointwise operations if `α` is.

Equations

- Filter.addCommSemigroup = { toAddSemigroup := Filter.addSemigroup, add_comm := ⋯ }

Instances For

source
def Filter.mulOneClass {α : Type u_2} [MulOneClass α] :
MulOneClass (Filter α)

`Filter α` is a `MulOneClass` under pointwise operations if `α` is.

Equations

- Filter.mulOneClass = { toOne := Filter.instOne, toMul := Filter.instMul, one_mul := ⋯, mul_one := ⋯ }

Instances For

source
def Filter.addZeroClass {α : Type u_2} [AddZeroClass α] :
AddZeroClass (Filter α)

`Filter α` is an `AddZeroClass` under pointwise operations if `α` is.

Equations

- Filter.addZeroClass = { toZero := Filter.instZero, toAdd := Filter.instAdd, zero_add := ⋯, add_zero := ⋯ }

Instances For

source
def Filter.mapMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] (φ : F) :
Filter α →* Filter β

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

Equations

- Filter.mapMonoidHom φ = { toFun := Filter.map ⇑φ, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
def Filter.mapAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] (φ : F) :
Filter α →+ Filter β

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

Equations

- Filter.mapAddMonoidHom φ = { toFun := Filter.map ⇑φ, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
theorem Filter.comap_mul_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [FunLike F α β] [MulHomClass F α β] (m : F) {f g : Filter β} :
comap (⇑m) f * comap (⇑m) g ≤ comap (⇑m) (f * g)
source
theorem Filter.comap_add_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddHomClass F α β] (m : F) {f g : Filter β} :
comap (⇑m) f + comap (⇑m) g ≤ comap (⇑m) (f + g)
source
theorem Filter.Tendsto.mul_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [FunLike F α β] [MulHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β} :
Tendsto (⇑m) f₁ f₂ → Tendsto (⇑m) g₁ g₂ → Tendsto (⇑m) (f₁ * g₁) (f₂ * g₂)
source
theorem Filter.Tendsto.add_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β} :
Tendsto (⇑m) f₁ f₂ → Tendsto (⇑m) g₁ g₂ → Tendsto (⇑m) (f₁ + g₁) (f₂ + g₂)
source
def Filter.pureMonoidHom {α : Type u_2} [MulOneClass α] :
α →* Filter α

`pure` as a `MonoidHom`.

Equations

- Filter.pureMonoidHom = { toFun := Filter.pureMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
def Filter.pureAddMonoidHom {α : Type u_2} [AddZeroClass α] :
α →+ Filter α

`pure` as an `AddMonoidHom`.

Equations

- Filter.pureAddMonoidHom = { toFun := Filter.pureAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Filter.coe_pureMonoidHom {α : Type u_2} [MulOneClass α] :
⇑pureMonoidHom = pure
source
@[simp]
theorem Filter.coe_pureAddMonoidHom {α : Type u_2} [AddZeroClass α] :
⇑pureAddMonoidHom = pure
source
@[simp]
theorem Filter.pureMonoidHom_apply {α : Type u_2} [MulOneClass α] (a : α) :
pureMonoidHom a = pure a
source
@[simp]
theorem Filter.pureAddMonoidHom_apply {α : Type u_2} [AddZeroClass α] (a : α) :
pureAddMonoidHom a = pure a
source
def Filter.monoid {α : Type u_2} [Monoid α] :
Monoid (Filter α)

`Filter α` is a `Monoid` under pointwise operations if `α` is.

Equations

- Filter.monoid = { toMul := Filter.mulOneClass.toMul, mul_assoc := ⋯, toOne := Filter.mulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

Instances For

source
def Filter.addMonoid {α : Type u_2} [AddMonoid α] :
AddMonoid (Filter α)

`Filter α` is an `AddMonoid` under pointwise operations if `α` is.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Filter.pow_mem_pow {α : Type u_2} [Monoid α] {f : Filter α} {s : Set α} (hs : s ∈ f) (n : ℕ) :
s ^ n ∈ f ^ n
source
theorem Filter.nsmul_mem_nsmul {α : Type u_2} [AddMonoid α] {f : Filter α} {s : Set α} (hs : s ∈ f) (n : ℕ) :
n • s ∈ n • f
source
@[simp]
theorem Filter.bot_pow {α : Type u_2} [Monoid α] {n : ℕ} (hn : n ≠ 0) :
⊥ ^ n = ⊥
source
@[simp]
theorem Filter.nsmul_bot {α : Type u_2} [AddMonoid α] {n : ℕ} (hn : n ≠ 0) :
n • ⊥ = ⊥
source
theorem Filter.mul_top_of_one_le {α : Type u_2} [Monoid α] {f : Filter α} (hf : 1 ≤ f) :
f * ⊤ = ⊤
source
theorem Filter.add_top_of_nonneg {α : Type u_2} [AddMonoid α] {f : Filter α} (hf : 0 ≤ f) :
f + ⊤ = ⊤
source
theorem Filter.top_mul_of_one_le {α : Type u_2} [Monoid α] {f : Filter α} (hf : 1 ≤ f) :
⊤ * f = ⊤
source
theorem Filter.top_add_of_nonneg {α : Type u_2} [AddMonoid α] {f : Filter α} (hf : 0 ≤ f) :
⊤ + f = ⊤
source
@[simp]
theorem Filter.top_mul_top {α : Type u_2} [Monoid α] :
⊤ * ⊤ = ⊤
source
@[simp]
theorem Filter.top_add_top {α : Type u_2} [AddMonoid α] :
⊤ + ⊤ = ⊤
source
theorem Filter.top_pow {α : Type u_2} [Monoid α] {n : ℕ} :
n ≠ 0 → ⊤ ^ n = ⊤
source
theorem Filter.nsmul_top {α : Type u_2} [AddMonoid α] {n : ℕ} :
n ≠ 0 → n • ⊤ = ⊤
source
theorem IsUnit.filter {α : Type u_2} [Monoid α] {a : α} :
IsUnit a → IsUnit (pure a)
source
theorem IsAddUnit.filter {α : Type u_2} [AddMonoid α] {a : α} :
IsAddUnit a → IsAddUnit (pure a)
source
def Filter.commMonoid {α : Type u_2} [CommMonoid α] :
CommMonoid (Filter α)

`Filter α` is a `CommMonoid` under pointwise operations if `α` is.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Filter.addCommMonoid {α : Type u_2} [AddCommMonoid α] :
AddCommMonoid (Filter α)

`Filter α` is an `AddCommMonoid` under pointwise operations if `α` is.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Filter.mul_eq_one_iff {α : Type u_2} [DivisionMonoid α] {f g : Filter α} :
f * g = 1 ↔ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
source
theorem Filter.add_eq_zero_iff {α : Type u_2} [SubtractionMonoid α] {f g : Filter α} :
f + g = 0 ↔ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a + b = 0
source
def Filter.divisionMonoid {α : Type u_2} [DivisionMonoid α] :
DivisionMonoid (Filter α)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Filter.subtractionMonoid {α : Type u_2} [SubtractionMonoid α] :
SubtractionMonoid (Filter α)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Filter.isUnit_iff {α : Type u_2} [DivisionMonoid α] {f : Filter α} :
IsUnit f ↔ ∃ (a : α), f = pure a ∧ IsUnit a
source
theorem Filter.isAddUnit_iff {α : Type u_2} [SubtractionMonoid α] {f : Filter α} :
IsAddUnit f ↔ ∃ (a : α), f = pure a ∧ IsAddUnit a
source
def Filter.divisionCommMonoid {α : Type u_2} [DivisionCommMonoid α] :
DivisionCommMonoid (Filter α)

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

Equations

- Filter.divisionCommMonoid = { toDivisionMonoid := Filter.divisionMonoid, mul_comm := ⋯ }

Instances For

source
def Filter.subtractionCommMonoid {α : Type u_2} [SubtractionCommMonoid α] :
SubtractionCommMonoid (Filter α)

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

Equations

- Filter.subtractionCommMonoid = { toSubtractionMonoid := Filter.subtractionMonoid, add_comm := ⋯ }

Instances For

source
def Filter.instDistribNeg {α : Type u_2} [Mul α] [HasDistribNeg α] :
HasDistribNeg (Filter α)

`Filter α` has distributive negation if `α` has.

Equations

- Filter.instDistribNeg = { toInvolutiveNeg := Filter.instInvolutiveNeg, neg_mul := ⋯, mul_neg := ⋯ }

Instances For

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

source
theorem Filter.mul_add_subset {α : Type u_2} [Distrib α] {f g h : Filter α} :
f * (g + h) ≤ f * g + f * h
source
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 `MulZeroClass` because `0 * ⊥ ≠ 0`.

source
theorem Filter.NeBot.mul_zero_nonneg {α : Type u_2} [MulZeroClass α] {f : Filter α} (hf : f.NeBot) :
0 ≤ f * 0
source
theorem Filter.NeBot.zero_mul_nonneg {α : Type u_2} [MulZeroClass α] {g : Filter α} (hg : g.NeBot) :
0 ≤ 0 * g

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

source
@[simp]
theorem Filter.one_le_div_iff {α : Type u_2} [Group α] {f g : Filter α} :
1 ≤ f / g ↔ ¬Disjoint f g
source
@[simp]
theorem Filter.nonneg_sub_iff {α : Type u_2} [AddGroup α] {f g : Filter α} :
0 ≤ f - g ↔ ¬Disjoint f g
source
theorem Filter.not_one_le_div_iff {α : Type u_2} [Group α] {f g : Filter α} :
¬1 ≤ f / g ↔ Disjoint f g
source
theorem Filter.not_nonneg_sub_iff {α : Type u_2} [AddGroup α] {f g : Filter α} :
¬0 ≤ f - g ↔ Disjoint f g
source
theorem Filter.NeBot.one_le_div {α : Type u_2} [Group α] {f : Filter α} (h : f.NeBot) :
1 ≤ f / f
source
theorem Filter.NeBot.nonneg_sub {α : Type u_2} [AddGroup α] {f : Filter α} (h : f.NeBot) :
0 ≤ f - f
source
theorem Filter.isUnit_pure {α : Type u_2} [Group α] (a : α) :
IsUnit (pure a)
source
theorem Filter.isAddUnit_pure {α : Type u_2} [AddGroup α] (a : α) :
IsAddUnit (pure a)
source
@[simp]
theorem Filter.isUnit_iff_singleton {α : Type u_2} [Group α] {f : Filter α} :
IsUnit f ↔ ∃ (a : α), f = pure a
source
theorem Filter.map_inv' {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {f : Filter α} :
map (⇑m) f⁻¹ = (map (⇑m) f)⁻¹
source
theorem Filter.map_neg' {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {f : Filter α} :
map (⇑m) (-f) = -map (⇑m) f
source
theorem Filter.Tendsto.inv_inv {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {f₁ : Filter α} {f₂ : Filter β} :
Tendsto (⇑m) f₁ f₂ → Tendsto (⇑m) f₁⁻¹ f₂⁻¹
source
theorem Filter.Tendsto.neg_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {f₁ : Filter α} {f₂ : Filter β} :
Tendsto (⇑m) f₁ f₂ → Tendsto (⇑m) (-f₁) (-f₂)
source
theorem Filter.map_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {f g : Filter α} :
map (⇑m) (f / g) = map (⇑m) f / map (⇑m) g
source
theorem Filter.map_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {f g : Filter α} :
map (⇑m) (f - g) = map (⇑m) f - map (⇑m) g
source
theorem Filter.Tendsto.div_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β} (hf : Tendsto (⇑m) f₁ f₂) (hg : Tendsto (⇑m) g₁ g₂) :
Tendsto (⇑m) (f₁ / g₁) (f₂ / g₂)
source
theorem Filter.Tendsto.sub_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β} (hf : Tendsto (⇑m) f₁ f₂) (hg : Tendsto (⇑m) g₁ g₂) :
Tendsto (⇑m) (f₁ - g₁) (f₂ - g₂)
source
theorem Filter.NeBot.div_zero_nonneg {α : Type u_2} [GroupWithZero α] {f : Filter α} (hf : f.NeBot) :
0 ≤ f / 0
source
theorem Filter.NeBot.zero_div_nonneg {α : Type u_2} [GroupWithZero α] {g : Filter α} (hg : g.NeBot) :
0 ≤ 0 / g

### Scalar addition/multiplication of filters #

source
def Filter.instSMul {α : Type u_2} {β : Type u_3} [SMul α β] :
SMul (Filter α) (Filter β)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Filter.instVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] :
VAdd (Filter α) (Filter β)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Filter.HasBasis.smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α} {pg : ιg → Prop} {sg : ιg → Set β} (hf : f.HasBasis pf sf) (hg : g.HasBasis pg sg) :
(f • g).HasBasis (fun (i : ιf × ιg) => pf i.1 ∧ pg i.2) fun (i : ιf × ιg) => sf i.1 • sg i.2
source
theorem Filter.HasBasis.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α} {pg : ιg → Prop} {sg : ιg → Set β} (hf : f.HasBasis pf sf) (hg : g.HasBasis pg sg) :
(f +ᵥ g).HasBasis (fun (i : ιf × ιg) => pf i.1 ∧ pg i.2) fun (i : ιf × ιg) => sf i.1 +ᵥ sg i.2
source
@[simp]
theorem Filter.map₂_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
map₂ (fun (x1 : α) (x2 : β) => x1 • x2) f g = f • g
source
@[simp]
theorem Filter.map₂_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
map₂ (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) f g = f +ᵥ g
source
theorem Filter.mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} {t : Set β} :
t ∈ f • g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ t
source
theorem Filter.mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} {t : Set β} :
t ∈ f +ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ +ᵥ t₂ ⊆ t
source
theorem Filter.smul_mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} {s : Set α} {t : Set β} :
s ∈ f → t ∈ g → s • t ∈ f • g
source
theorem Filter.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} {s : Set α} {t : Set β} :
s ∈ f → t ∈ g → s +ᵥ t ∈ f +ᵥ g
source
@[simp]
theorem Filter.bot_smul {α : Type u_2} {β : Type u_3} [SMul α β] {g : Filter β} :
⊥ • g = ⊥
source
@[simp]
theorem Filter.bot_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {g : Filter β} :
⊥ +ᵥ g = ⊥
source
@[simp]
theorem Filter.smul_bot {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} :
f • ⊥ = ⊥
source
@[simp]
theorem Filter.vadd_bot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} :
f +ᵥ ⊥ = ⊥
source
@[simp]
theorem Filter.smul_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem Filter.vadd_eq_bot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
f +ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem Filter.smul_neBot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
(f • g).NeBot ↔ f.NeBot ∧ g.NeBot
source
@[simp]
theorem Filter.vadd_neBot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
(f +ᵥ g).NeBot ↔ f.NeBot ∧ g.NeBot
source
theorem Filter.NeBot.smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
f.NeBot → g.NeBot → (f • g).NeBot
source
theorem Filter.NeBot.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
f.NeBot → g.NeBot → (f +ᵥ g).NeBot
source
theorem Filter.NeBot.of_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
(f • g).NeBot → f.NeBot
source
theorem Filter.NeBot.of_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
(f +ᵥ g).NeBot → f.NeBot
source
theorem Filter.NeBot.of_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
(f • g).NeBot → g.NeBot
source
theorem Filter.NeBot.of_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
(f +ᵥ g).NeBot → g.NeBot
source
theorem Filter.smul.instNeBot {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} [f.NeBot] [g.NeBot] :
(f • g).NeBot
source
theorem Filter.vadd.instNeBot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} [f.NeBot] [g.NeBot] :
(f +ᵥ g).NeBot
source
@[simp]
theorem Filter.pure_smul {α : Type u_2} {β : Type u_3} [SMul α β] {g : Filter β} {a : α} :
pure a • g = map (fun (x : β) => a • x) g
source
@[simp]
theorem Filter.pure_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {g : Filter β} {a : α} :
pure a +ᵥ g = map (fun (x : β) => a +ᵥ x) g
source
@[simp]
theorem Filter.smul_pure {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {b : β} :
f • pure b = map (fun (x : α) => x • b) f
source
@[simp]
theorem Filter.vadd_pure {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {b : β} :
f +ᵥ pure b = map (fun (x : α) => x +ᵥ b) f
source
theorem Filter.pure_smul_pure {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} :
pure a • pure b = pure (a • b)
source
theorem Filter.pure_vadd_pure {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} :
pure a +ᵥ pure b = pure (a +ᵥ b)
source
theorem Filter.smul_le_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ • g₁ ≤ f₂ • g₂
source
theorem Filter.vadd_le_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ +ᵥ g₁ ≤ f₂ +ᵥ g₂
source
theorem Filter.smul_le_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g₁ g₂ : Filter β} :
g₁ ≤ g₂ → f • g₁ ≤ f • g₂
source
theorem Filter.vadd_le_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g₁ g₂ : Filter β} :
g₁ ≤ g₂ → f +ᵥ g₁ ≤ f +ᵥ g₂
source
theorem Filter.smul_le_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ f₂ : Filter α} {g : Filter β} :
f₁ ≤ f₂ → f₁ • g ≤ f₂ • g
source
theorem Filter.vadd_le_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ f₂ : Filter α} {g : Filter β} :
f₁ ≤ f₂ → f₁ +ᵥ g ≤ f₂ +ᵥ g
source
@[simp]
theorem Filter.le_smul_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g h : Filter β} :
h ≤ f • g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s • t ∈ h
source
@[simp]
theorem Filter.le_vadd_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g h : Filter β} :
h ≤ f +ᵥ g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s +ᵥ t ∈ h
source
instance Filter.covariant_smul {α : Type u_2} {β : Type u_3} [SMul α β] :
CovariantClass (Filter α) (Filter β) (fun (x1 : Filter α) (x2 : Filter β) => x1 • x2) fun (x1 x2 : Filter β) => x1 ≤ x2
source
instance Filter.covariant_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] :
CovariantClass (Filter α) (Filter β) (fun (x1 : Filter α) (x2 : Filter β) => x1 +ᵥ x2) fun (x1 x2 : Filter β) => x1 ≤ x2

### Scalar subtraction of filters #

source
def Filter.instVSub {α : Type u_2} {β : Type u_3} [VSub α β] :
VSub (Filter α) (Filter β)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Filter.map₂_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} :
map₂ (fun (x1 x2 : β) => x1 -ᵥ x2) f g = f -ᵥ g
source
theorem Filter.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} {s : Set α} :
s ∈ f -ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s
source
theorem Filter.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} {s t : Set β} :
s ∈ f → t ∈ g → s -ᵥ t ∈ f -ᵥ g
source
@[simp]
theorem Filter.bot_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {g : Filter β} :
⊥ -ᵥ g = ⊥
source
@[simp]
theorem Filter.vsub_bot {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} :
f -ᵥ ⊥ = ⊥
source
@[simp]
theorem Filter.vsub_eq_bot_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} :
f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem Filter.vsub_neBot_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} :
(f -ᵥ g).NeBot ↔ f.NeBot ∧ g.NeBot
source
theorem Filter.NeBot.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} :
f.NeBot → g.NeBot → (f -ᵥ g).NeBot
source
theorem Filter.NeBot.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} :
(f -ᵥ g).NeBot → f.NeBot
source
theorem Filter.NeBot.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} :
(f -ᵥ g).NeBot → g.NeBot
source
theorem Filter.vsub.instNeBot {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} [f.NeBot] [g.NeBot] :
(f -ᵥ g).NeBot
source
@[simp]
theorem Filter.pure_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {g : Filter β} {a : β} :
pure a -ᵥ g = map (fun (x : β) => a -ᵥ x) g
source
@[simp]
theorem Filter.vsub_pure {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {b : β} :
f -ᵥ pure b = map (fun (x : β) => x -ᵥ b) f
source
theorem Filter.pure_vsub_pure {α : Type u_2} {β : Type u_3} [VSub α β] {a b : β} :
pure a -ᵥ pure b = pure (a -ᵥ b)
source
theorem Filter.vsub_le_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f₁ f₂ g₁ g₂ : Filter β} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ -ᵥ g₁ ≤ f₂ -ᵥ g₂
source
theorem Filter.vsub_le_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {f g₁ g₂ : Filter β} :
g₁ ≤ g₂ → f -ᵥ g₁ ≤ f -ᵥ g₂
source
theorem Filter.vsub_le_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {f₁ f₂ g : Filter β} :
f₁ ≤ f₂ → f₁ -ᵥ g ≤ f₂ -ᵥ g
source
@[simp]
theorem Filter.le_vsub_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} {h : Filter α} :
h ≤ f -ᵥ g ↔ ∀ ⦃s : Set β⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s -ᵥ t ∈ h

### Translation/scaling of filters #

source
def Filter.instSMulFilter {α : Type u_2} {β : Type u_3} [SMul α β] :
SMul α (Filter β)

`a • f` is the map of `f` under `a •` in scope `Pointwise`.

Equations

- Filter.instSMulFilter = { smul := fun (a : α) => Filter.map fun (x : β) => a • x }

Instances For

source
def Filter.instVAddFilter {α : Type u_2} {β : Type u_3} [VAdd α β] :
VAdd α (Filter β)

`a +ᵥ f` is the map of `f` under `a +ᵥ` in scope `Pointwise`.

Equations

- Filter.instVAddFilter = { vadd := fun (a : α) => Filter.map fun (x : β) => a +ᵥ x }

Instances For

source
@[simp]
theorem Filter.map_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
map (fun (b : β) => a • b) f = a • f
source
@[simp]
theorem Filter.map_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
map (fun (b : β) => a +ᵥ b) f = a +ᵥ f
source
theorem Filter.mem_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {s : Set β} {a : α} :
s ∈ a • f ↔ (fun (x : β) => a • x) ⁻¹' s ∈ f
source
theorem Filter.mem_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {s : Set β} {a : α} :
s ∈ a +ᵥ f ↔ (fun (x : β) => a +ᵥ x) ⁻¹' s ∈ f
source
theorem Filter.smul_set_mem_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {s : Set β} {a : α} :
s ∈ f → a • s ∈ a • f
source
theorem Filter.vadd_set_mem_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {s : Set β} {a : α} :
s ∈ f → a +ᵥ s ∈ a +ᵥ f
source
@[simp]
theorem Filter.smul_filter_bot {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} :
a • ⊥ = ⊥
source
@[simp]
theorem Filter.vadd_filter_bot {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} :
a +ᵥ ⊥ = ⊥
source
@[simp]
theorem Filter.smul_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
a • f = ⊥ ↔ f = ⊥
source
@[simp]
theorem Filter.vadd_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
a +ᵥ f = ⊥ ↔ f = ⊥
source
@[simp]
theorem Filter.smul_filter_neBot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
(a • f).NeBot ↔ f.NeBot
source
@[simp]
theorem Filter.vadd_filter_neBot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
(a +ᵥ f).NeBot ↔ f.NeBot
source
theorem Filter.NeBot.smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
f.NeBot → (a • f).NeBot
source
theorem Filter.NeBot.vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
f.NeBot → (a +ᵥ f).NeBot
source
theorem Filter.NeBot.of_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
(a • f).NeBot → f.NeBot
source
theorem Filter.NeBot.of_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
(a +ᵥ f).NeBot → f.NeBot
source
theorem Filter.smul_filter.instNeBot {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} [f.NeBot] :
(a • f).NeBot
source
theorem Filter.vadd_filter.instNeBot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} [f.NeBot] :
(a +ᵥ f).NeBot
source
theorem Filter.smul_filter_le_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ f₂ : Filter β} {a : α} (hf : f₁ ≤ f₂) :
a • f₁ ≤ a • f₂
source
theorem Filter.vadd_filter_le_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ f₂ : Filter β} {a : α} (hf : f₁ ≤ f₂) :
a +ᵥ f₁ ≤ a +ᵥ f₂
source
instance Filter.covariant_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] :
CovariantClass α (Filter β) (fun (x1 : α) (x2 : Filter β) => x1 • x2) fun (x1 x2 : Filter β) => x1 ≤ x2
source
instance Filter.covariant_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] :
CovariantClass α (Filter β) (fun (x1 : α) (x2 : Filter β) => x1 +ᵥ x2) fun (x1 x2 : Filter β) => x1 ≤ x2
source
instance Filter.smulCommClass_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
SMulCommClass α β (Filter γ)
source
instance Filter.vaddCommClass_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
VAddCommClass α β (Filter γ)
source
instance Filter.smulCommClass_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
SMulCommClass α (Filter β) (Filter γ)
source
instance Filter.vaddCommClass_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
VAddCommClass α (Filter β) (Filter γ)
source
instance Filter.smulCommClass_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
SMulCommClass (Filter α) β (Filter γ)
source
instance Filter.vaddCommClass_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
VAddCommClass (Filter α) β (Filter γ)
source
instance Filter.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
SMulCommClass (Filter α) (Filter β) (Filter γ)
source
instance Filter.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
VAddCommClass (Filter α) (Filter β) (Filter γ)
source
instance Filter.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
IsScalarTower α β (Filter γ)
source
instance Filter.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
VAddAssocClass α β (Filter γ)
source
instance Filter.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
IsScalarTower α (Filter β) (Filter γ)
source
instance Filter.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
VAddAssocClass α (Filter β) (Filter γ)
source
instance Filter.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
IsScalarTower (Filter α) (Filter β) (Filter γ)
source
instance Filter.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
VAddAssocClass (Filter α) (Filter β) (Filter γ)
source
instance Filter.isCentralScalar {α : Type u_2} {β : Type u_3} [SMul α β] [SMul α ᵐᵒᵖ β] [IsCentralScalar α β] :
IsCentralScalar α (Filter β)
source
instance Filter.isCentralVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] [VAdd α ᵃᵒᵖ β] [IsCentralVAdd α β] :
IsCentralVAdd α (Filter β)
source
def Filter.mulAction {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] :
MulAction (Filter α) (Filter β)

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

Equations

- Filter.mulAction = { toSMul := Filter.instSMul, one_smul := ⋯, mul_smul := ⋯ }

Instances For

source
def Filter.addAction {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] :
AddAction (Filter α) (Filter β)

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

Equations

- Filter.addAction = { toVAdd := Filter.instVAdd, zero_vadd := ⋯, add_vadd := ⋯ }

Instances For

source
def Filter.mulActionFilter {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] :
MulAction α (Filter β)

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

Equations

- Filter.mulActionFilter = { toSMul := Filter.instSMulFilter, one_smul := ⋯, mul_smul := ⋯ }

Instances For

source
def Filter.addActionFilter {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] :
AddAction α (Filter β)

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

Equations

- Filter.addActionFilter = { toVAdd := Filter.instVAddFilter, zero_vadd := ⋯, add_vadd := ⋯ }

Instances For

source
def Filter.distribMulActionFilter {α : Type u_2} {β : Type u_3} [Monoid α] [AddMonoid β] [DistribMulAction α β] :
DistribMulAction α (Filter β)

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

Equations

- Filter.distribMulActionFilter = { toMulAction := Filter.mulActionFilter, smul_zero := ⋯, smul_add := ⋯ }

Instances For

source
noncomputable def Filter.mulDistribMulActionFilter {α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] [MulDistribMulAction α β] :
MulDistribMulAction α (Set β)

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

Equations

- Filter.mulDistribMulActionFilter = { toMulAction := Set.mulActionSet, smul_mul := ⋯, smul_one := ⋯ }

Instances For

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

source
theorem Filter.NeBot.smul_zero_nonneg {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {f : Filter α} (hf : f.NeBot) :
0 ≤ f • 0
source
theorem Filter.NeBot.zero_smul_nonneg {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} (hg : g.NeBot) :
0 ≤ 0 • g
source
theorem Filter.zero_smul_filter_nonpos {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} :
0 • g ≤ 0
source
theorem Filter.zero_smul_filter {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} (hg : g.NeBot) :
0 • g = 0
source
theorem IsUnit.smul_tendsto_smul_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Monoid γ] [MulAction γ β] {m : α → β} {c : γ} {f : Filter α} {g : Filter β} (hc : IsUnit c) :
Filter.Tendsto (c • m) f (c • g) ↔ Filter.Tendsto m f g
source
theorem IsAddUnit.vadd_tendsto_vadd_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddMonoid γ] [AddAction γ β] {m : α → β} {c : γ} {f : Filter α} {g : Filter β} (hc : IsAddUnit c) :
Filter.Tendsto (c +ᵥ m) f (c +ᵥ g) ↔ Filter.Tendsto m f g
source
@[simp]
theorem Filter.smul_tendsto_smul_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Group γ] [MulAction γ β] {m : α → β} {c : γ} {f : Filter α} {g : Filter β} :
Tendsto (c • m) f (c • g) ↔ Tendsto m f g
source
@[simp]
theorem Filter.vadd_tendsto_vadd_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddGroup γ] [AddAction γ β] {m : α → β} {c : γ} {f : Filter α} {g : Filter β} :
Tendsto (c +ᵥ m) f (c +ᵥ g) ↔ Tendsto m f g
source
theorem Filter.smul_tendsto_smul_iff₀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [GroupWithZero γ] [MulAction γ β] {m : α → β} {c : γ} {f : Filter α} {g : Filter β} (hc : c ≠ 0) :
Tendsto (c • m) f (c • g) ↔ Tendsto m f g