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 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 #

0/1 as filters #

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

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

Equations
• Filter.instZero = { zero := pure 0 }
Instances For
def Filter.instOne {α : Type u_2} [One α] :
One ()

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

Equations
• Filter.instOne = { one := pure 1 }
Instances For
@[simp]
theorem Filter.mem_zero {α : Type u_2} [Zero α] {s : Set α} :
s 0 0 s
@[simp]
theorem Filter.mem_one {α : Type u_2} [One α] {s : Set α} :
s 1 1 s
theorem Filter.zero_mem_zero {α : Type u_2} [Zero α] :
0 0
theorem Filter.one_mem_one {α : Type u_2} [One α] :
1 1
@[simp]
theorem Filter.pure_zero {α : Type u_2} [Zero α] :
pure 0 = 0
@[simp]
theorem Filter.pure_one {α : Type u_2} [One α] :
pure 1 = 1
@[simp]
theorem Filter.principal_zero {α : Type u_2} [Zero α] :
@[simp]
theorem Filter.principal_one {α : Type u_2} [One α] :
theorem Filter.zero_neBot {α : Type u_2} [Zero α] :
theorem Filter.one_neBot {α : Type u_2} [One α] :
@[simp]
theorem Filter.map_zero' {α : Type u_2} {β : Type u_3} [Zero α] (f : αβ) :
= pure (f 0)
@[simp]
theorem Filter.map_one' {α : Type u_2} {β : Type u_3} [One α] (f : αβ) :
= pure (f 1)
@[simp]
theorem Filter.nonpos_iff {α : Type u_2} [Zero α] {f : } :
f 0 0 f
@[simp]
theorem Filter.le_one_iff {α : Type u_2} [One α] {f : } :
f 1 1 f
theorem Filter.NeBot.nonpos_iff {α : Type u_2} [Zero α] {f : } (h : f.NeBot) :
f 0 f = 0
theorem Filter.NeBot.le_one_iff {α : Type u_2} [One α] {f : } (h : f.NeBot) :
f 1 f = 1
@[simp]
theorem Filter.eventually_zero {α : Type u_2} [Zero α] {p : αProp} :
(∀ᶠ (x : α) in 0, p x) p 0
@[simp]
theorem Filter.eventually_one {α : Type u_2} [One α] {p : αProp} :
(∀ᶠ (x : α) in 1, p x) p 1
@[simp]
theorem Filter.tendsto_zero {α : Type u_2} {β : Type u_3} [Zero α] {a : } {f : βα} :
∀ᶠ (x : β) in a, f x = 0
@[simp]
theorem Filter.tendsto_one {α : Type u_2} {β : Type u_3} [One α] {a : } {f : βα} :
∀ᶠ (x : β) in a, f x = 1
@[simp]
theorem Filter.zero_sum_zero {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] :
0 ×ˢ 0 = 0
@[simp]
theorem Filter.one_prod_one {α : Type u_2} {β : Type u_3} [One α] [One β] :
1 ×ˢ 1 = 1
def Filter.pureZeroHom {α : Type u_2} [Zero α] :
ZeroHom α ()

pure as a ZeroHom.

Equations
• Filter.pureZeroHom = { toFun := pure, map_zero' := }
Instances For
def Filter.pureOneHom {α : Type u_2} [One α] :
OneHom α ()

pure as a OneHom.

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

Filter negation/inversion #

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

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

Equations
instance Filter.instInv {α : Type u_2} [Inv α] :
Inv ()

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

Equations
@[simp]
theorem Filter.map_neg {α : Type u_2} [Neg α] {f : } :
Filter.map Neg.neg f = -f
@[simp]
theorem Filter.map_inv {α : Type u_2} [Inv α] {f : } :
Filter.map Inv.inv f = f⁻¹
theorem Filter.mem_neg {α : Type u_2} [Neg α] {f : } {s : Set α} :
s -f Neg.neg ⁻¹' s f
theorem Filter.mem_inv {α : Type u_2} [Inv α] {f : } {s : Set α} :
s f⁻¹ Inv.inv ⁻¹' s f
theorem Filter.neg_le_neg {α : Type u_2} [Neg α] {f : } {g : } (hf : f g) :
-f -g
theorem Filter.inv_le_inv {α : Type u_2} [Inv α] {f : } {g : } (hf : f g) :
@[simp]
theorem Filter.neg_pure {α : Type u_2} [Neg α] {a : α} :
-pure a = pure (-a)
@[simp]
theorem Filter.inv_pure {α : Type u_2} [Inv α] {a : α} :
@[simp]
theorem Filter.neg_eq_bot_iff {α : Type u_2} [Neg α] {f : } :
-f = f =
@[simp]
theorem Filter.inv_eq_bot_iff {α : Type u_2} [Inv α] {f : } :
@[simp]
theorem Filter.neBot_neg_iff {α : Type u_2} [Neg α] {f : } :
(-f).NeBot f.NeBot
@[simp]
theorem Filter.neBot_inv_iff {α : Type u_2} [Inv α] {f : } :
f⁻¹.NeBot f.NeBot
theorem Filter.NeBot.neg {α : Type u_2} [Neg α] {f : } :
f.NeBot(-f).NeBot
theorem Filter.NeBot.inv {α : Type u_2} [Inv α] {f : } :
f.NeBotf⁻¹.NeBot
theorem Filter.neg.instNeBot {α : Type u_2} [Neg α] {f : } [f.NeBot] :
(-f).NeBot
theorem Filter.inv.instNeBot {α : Type u_2} [Inv α] {f : } [f.NeBot] :
f⁻¹.NeBot
@[simp]
theorem Filter.comap_neg {α : Type u_2} [] {f : } :
Filter.comap Neg.neg f = -f
@[simp]
theorem Filter.comap_inv {α : Type u_2} [] {f : } :
Filter.comap Inv.inv f = f⁻¹
theorem Filter.neg_mem_neg {α : Type u_2} [] {f : } {s : Set α} (hs : s f) :
-s -f
theorem Filter.inv_mem_inv {α : Type u_2} [] {f : } {s : Set α} (hs : s f) :
theorem Filter.instInvolutiveNeg.proof_1 {α : Type u_1} [] (f : ) :
Filter.map Neg.neg (Filter.map Neg.neg f) = f
def Filter.instInvolutiveNeg {α : Type u_2} [] :

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

Equations
• Filter.instInvolutiveNeg = let __src := Filter.instNeg;
Instances For
def Filter.instInvolutiveInv {α : Type u_2} [] :

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

Equations
• Filter.instInvolutiveInv = let __src := Filter.instInv;
Instances For
@[simp]
theorem Filter.neg_le_neg_iff {α : Type u_2} [] {f : } {g : } :
-f -g f g
@[simp]
theorem Filter.inv_le_inv_iff {α : Type u_2} [] {f : } {g : } :
theorem Filter.neg_le_iff_le_neg {α : Type u_2} [] {f : } {g : } :
-f g f -g
theorem Filter.inv_le_iff_le_inv {α : Type u_2} [] {f : } {g : } :
@[simp]
theorem Filter.neg_le_self {α : Type u_2} [] {f : } :
-f f -f = f
@[simp]
theorem Filter.inv_le_self {α : Type u_2} [] {f : } :
@[simp]
theorem Filter.neg_atTop {G : Type u_7} :
-Filter.atTop = Filter.atBot
@[simp]
theorem Filter.inv_atTop {G : Type u_7} [] :
Filter.atTop⁻¹ = Filter.atBot

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
def Filter.instMul {α : Type u_2} [Mul α] :
Mul ()

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
@[simp]
theorem Filter.map₂_add {α : Type u_2} [Add α] {f : } {g : } :
Filter.map₂ (fun (x x_1 : α) => x + x_1) f g = f + g
@[simp]
theorem Filter.map₂_mul {α : Type u_2} [Mul α] {f : } {g : } :
Filter.map₂ (fun (x x_1 : α) => x * x_1) f g = f * g
theorem Filter.mem_add {α : Type u_2} [Add α] {f : } {g : } {s : Set α} :
s f + g t₁f, t₂g, t₁ + t₂ s
theorem Filter.mem_mul {α : Type u_2} [Mul α] {f : } {g : } {s : Set α} :
s f * g t₁f, t₂g, t₁ * t₂ s
theorem Filter.add_mem_add {α : Type u_2} [Add α] {f : } {g : } {s : Set α} {t : Set α} :
s ft gs + t f + g
theorem Filter.mul_mem_mul {α : Type u_2} [Mul α] {f : } {g : } {s : Set α} {t : Set α} :
s ft gs * t f * g
@[simp]
theorem Filter.bot_add {α : Type u_2} [Add α] {g : } :
@[simp]
theorem Filter.bot_mul {α : Type u_2} [Mul α] {g : } :
@[simp]
theorem Filter.add_bot {α : Type u_2} [Add α] {f : } :
@[simp]
theorem Filter.mul_bot {α : Type u_2} [Mul α] {f : } :
@[simp]
theorem Filter.add_eq_bot_iff {α : Type u_2} [Add α] {f : } {g : } :
f + g = f = g =
@[simp]
theorem Filter.mul_eq_bot_iff {α : Type u_2} [Mul α] {f : } {g : } :
f * g = f = g =
@[simp]
theorem Filter.add_neBot_iff {α : Type u_2} [Add α] {f : } {g : } :
(f + g).NeBot f.NeBot g.NeBot
@[simp]
theorem Filter.mul_neBot_iff {α : Type u_2} [Mul α] {f : } {g : } :
(f * g).NeBot f.NeBot g.NeBot
theorem Filter.NeBot.add {α : Type u_2} [Add α] {f : } {g : } :
f.NeBotg.NeBot(f + g).NeBot
theorem Filter.NeBot.mul {α : Type u_2} [Mul α] {f : } {g : } :
f.NeBotg.NeBot(f * g).NeBot
theorem Filter.NeBot.of_add_left {α : Type u_2} [Add α] {f : } {g : } :
(f + g).NeBotf.NeBot
theorem Filter.NeBot.of_mul_left {α : Type u_2} [Mul α] {f : } {g : } :
(f * g).NeBotf.NeBot
theorem Filter.NeBot.of_add_right {α : Type u_2} [Add α] {f : } {g : } :
(f + g).NeBotg.NeBot
theorem Filter.NeBot.of_mul_right {α : Type u_2} [Mul α] {f : } {g : } :
(f * g).NeBotg.NeBot
theorem Filter.add.instNeBot {α : Type u_2} [Add α] {f : } {g : } [f.NeBot] [g.NeBot] :
(f + g).NeBot
theorem Filter.mul.instNeBot {α : Type u_2} [Mul α] {f : } {g : } [f.NeBot] [g.NeBot] :
(f * g).NeBot
@[simp]
theorem Filter.pure_add {α : Type u_2} [Add α] {g : } {a : α} :
pure a + g = Filter.map (fun (x : α) => a + x) g
@[simp]
theorem Filter.pure_mul {α : Type u_2} [Mul α] {g : } {a : α} :
pure a * g = Filter.map (fun (x : α) => a * x) g
@[simp]
theorem Filter.add_pure {α : Type u_2} [Add α] {f : } {b : α} :
f + pure b = Filter.map (fun (x : α) => x + b) f
@[simp]
theorem Filter.mul_pure {α : Type u_2} [Mul α] {f : } {b : α} :
f * pure b = Filter.map (fun (x : α) => x * b) f
theorem Filter.pure_add_pure {α : Type u_2} [Add α] {a : α} {b : α} :
pure a + pure b = pure (a + b)
theorem Filter.pure_mul_pure {α : Type u_2} [Mul α] {a : α} {b : α} :
pure a * pure b = pure (a * b)
@[simp]
theorem Filter.le_add_iff {α : Type u_2} [Add α] {f : } {g : } {h : } :
h f + g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set α⦄, t gs + t h
@[simp]
theorem Filter.le_mul_iff {α : Type u_2} [Mul α] {f : } {g : } {h : } :
h f * g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set α⦄, t gs * t h
CovariantClass () () (fun (x x_1 : ) => x + x_1) fun (x x_1 : ) => x x_1
Equations
• =
instance Filter.covariant_mul {α : Type u_2} [Mul α] :
CovariantClass () () (fun (x x_1 : ) => x * x_1) fun (x x_1 : ) => x x_1
Equations
• =
CovariantClass () () (Function.swap fun (x x_1 : ) => x + x_1) fun (x x_1 : ) => x x_1
Equations
• =
instance Filter.covariant_swap_mul {α : Type u_2} [Mul α] :
CovariantClass () () (Function.swap fun (x x_1 : ) => x * x_1) fun (x x_1 : ) => x x_1
Equations
• =
theorem Filter.map_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] {f₁ : } {f₂ : } [FunLike F α β] [AddHomClass F α β] (m : F) :
Filter.map (m) (f₁ + f₂) = Filter.map (m) f₁ + Filter.map (m) f₂
theorem Filter.map_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] {f₁ : } {f₂ : } [FunLike F α β] [MulHomClass F α β] (m : F) :
Filter.map (m) (f₁ * f₂) = Filter.map (m) f₁ * Filter.map (m) f₂
∀ (x x_1 : α), pure (x + x_1) = pure x + pure x_1

The singleton operation as an AddHom.

Equations
Instances For
def Filter.pureMulHom {α : Type u_2} [Mul α] :

pure operation as a MulHom.

Equations
• Filter.pureMulHom = { toFun := pure, map_mul' := }
Instances For
@[simp]
@[simp]
theorem Filter.coe_pureMulHom {α : Type u_2} [Mul α] :
Filter.pureMulHom = pure
@[simp]
theorem Filter.pureAddHom_apply {α : Type u_2} [Add α] (a : α) :
@[simp]
theorem Filter.pureMulHom_apply {α : Type u_2} [Mul α] (a : α) :
Filter.pureMulHom a = pure a

Filter subtraction/division #

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

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
def Filter.instDiv {α : Type u_2} [Div α] :
Div ()

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
@[simp]
theorem Filter.map₂_sub {α : Type u_2} [Sub α] {f : } {g : } :
Filter.map₂ (fun (x x_1 : α) => x - x_1) f g = f - g
@[simp]
theorem Filter.map₂_div {α : Type u_2} [Div α] {f : } {g : } :
Filter.map₂ (fun (x x_1 : α) => x / x_1) f g = f / g
theorem Filter.mem_sub {α : Type u_2} [Sub α] {f : } {g : } {s : Set α} :
s f - g t₁f, t₂g, t₁ - t₂ s
theorem Filter.mem_div {α : Type u_2} [Div α] {f : } {g : } {s : Set α} :
s f / g t₁f, t₂g, t₁ / t₂ s
theorem Filter.sub_mem_sub {α : Type u_2} [Sub α] {f : } {g : } {s : Set α} {t : Set α} :
s ft gs - t f - g
theorem Filter.div_mem_div {α : Type u_2} [Div α] {f : } {g : } {s : Set α} {t : Set α} :
s ft gs / t f / g
@[simp]
theorem Filter.bot_sub {α : Type u_2} [Sub α] {g : } :
@[simp]
theorem Filter.bot_div {α : Type u_2} [Div α] {g : } :
@[simp]
theorem Filter.sub_bot {α : Type u_2} [Sub α] {f : } :
@[simp]
theorem Filter.div_bot {α : Type u_2} [Div α] {f : } :
@[simp]
theorem Filter.sub_eq_bot_iff {α : Type u_2} [Sub α] {f : } {g : } :
f - g = f = g =
@[simp]
theorem Filter.div_eq_bot_iff {α : Type u_2} [Div α] {f : } {g : } :
f / g = f = g =
@[simp]
theorem Filter.sub_neBot_iff {α : Type u_2} [Sub α] {f : } {g : } :
(f - g).NeBot f.NeBot g.NeBot
@[simp]
theorem Filter.div_neBot_iff {α : Type u_2} [Div α] {f : } {g : } :
(f / g).NeBot f.NeBot g.NeBot
theorem Filter.NeBot.sub {α : Type u_2} [Sub α] {f : } {g : } :
f.NeBotg.NeBot(f - g).NeBot
theorem Filter.NeBot.div {α : Type u_2} [Div α] {f : } {g : } :
f.NeBotg.NeBot(f / g).NeBot
theorem Filter.NeBot.of_sub_left {α : Type u_2} [Sub α] {f : } {g : } :
(f - g).NeBotf.NeBot
theorem Filter.NeBot.of_div_left {α : Type u_2} [Div α] {f : } {g : } :
(f / g).NeBotf.NeBot
theorem Filter.NeBot.of_sub_right {α : Type u_2} [Sub α] {f : } {g : } :
(f - g).NeBotg.NeBot
theorem Filter.NeBot.of_div_right {α : Type u_2} [Div α] {f : } {g : } :
(f / g).NeBotg.NeBot
theorem Filter.sub.instNeBot {α : Type u_2} [Sub α] {f : } {g : } [f.NeBot] [g.NeBot] :
(f - g).NeBot
theorem Filter.div.instNeBot {α : Type u_2} [Div α] {f : } {g : } [f.NeBot] [g.NeBot] :
(f / g).NeBot
@[simp]
theorem Filter.pure_sub {α : Type u_2} [Sub α] {g : } {a : α} :
pure a - g = Filter.map (fun (x : α) => a - x) g
@[simp]
theorem Filter.pure_div {α : Type u_2} [Div α] {g : } {a : α} :
pure a / g = Filter.map (fun (x : α) => a / x) g
@[simp]
theorem Filter.sub_pure {α : Type u_2} [Sub α] {f : } {b : α} :
f - pure b = Filter.map (fun (x : α) => x - b) f
@[simp]
theorem Filter.div_pure {α : Type u_2} [Div α] {f : } {b : α} :
f / pure b = Filter.map (fun (x : α) => x / b) f
theorem Filter.pure_sub_pure {α : Type u_2} [Sub α] {a : α} {b : α} :
pure a - pure b = pure (a - b)
theorem Filter.pure_div_pure {α : Type u_2} [Div α] {a : α} {b : α} :
pure a / pure b = pure (a / b)
theorem Filter.sub_le_sub {α : Type u_2} [Sub α] {f₁ : } {f₂ : } {g₁ : } {g₂ : } :
f₁ f₂g₁ g₂f₁ - g₁ f₂ - g₂
theorem Filter.div_le_div {α : Type u_2} [Div α] {f₁ : } {f₂ : } {g₁ : } {g₂ : } :
f₁ f₂g₁ g₂f₁ / g₁ f₂ / g₂
theorem Filter.sub_le_sub_left {α : Type u_2} [Sub α] {f : } {g₁ : } {g₂ : } :
g₁ g₂f - g₁ f - g₂
theorem Filter.div_le_div_left {α : Type u_2} [Div α] {f : } {g₁ : } {g₂ : } :
g₁ g₂f / g₁ f / g₂
theorem Filter.sub_le_sub_right {α : Type u_2} [Sub α] {f₁ : } {f₂ : } {g : } :
f₁ f₂f₁ - g f₂ - g
theorem Filter.div_le_div_right {α : Type u_2} [Div α] {f₁ : } {f₂ : } {g : } :
f₁ f₂f₁ / g f₂ / g
@[simp]
theorem Filter.le_sub_iff {α : Type u_2} [Sub α] {f : } {g : } {h : } :
h f - g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set α⦄, t gs - t h
@[simp]
theorem Filter.le_div_iff {α : Type u_2} [Div α] {f : } {g : } {h : } :
h f / g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set α⦄, t gs / t h
instance Filter.covariant_sub {α : Type u_2} [Sub α] :
CovariantClass () () (fun (x x_1 : ) => x - x_1) fun (x x_1 : ) => x x_1
Equations
• =
instance Filter.covariant_div {α : Type u_2} [Div α] :
CovariantClass () () (fun (x x_1 : ) => x / x_1) fun (x x_1 : ) => x x_1
Equations
• =
instance Filter.covariant_swap_sub {α : Type u_2} [Sub α] :
CovariantClass () () (Function.swap fun (x x_1 : ) => x - x_1) fun (x x_1 : ) => x x_1
Equations
• =
instance Filter.covariant_swap_div {α : Type u_2} [Div α] :
CovariantClass () () (Function.swap fun (x x_1 : ) => x / x_1) fun (x x_1 : ) => x x_1
Equations
• =
def Filter.instNSMul {α : Type u_2} [Zero α] [Add α] :

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
def Filter.instNPow {α : Type u_2} [One α] [Mul α] :
Pow ()

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

Equations
• Filter.instNPow = { pow := fun (s : ) (n : ) => npowRec n s }
Instances For
def Filter.instZSMul {α : Type u_2} [Zero α] [Add α] [Neg α] :

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
def Filter.instZPow {α : Type u_2} [One α] [Mul α] [Inv α] :
Pow ()

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 : ) (n : ) => zpowRec npowRec n s }
Instances For
theorem Filter.addSemigroup.proof_1 {α : Type u_1} [] :
∀ (x x_1 x_2 : ), Filter.map₂ (fun (x x_3 : α) => x + x_3) (Filter.map₂ (fun (x x_3 : α) => x + x_3) x x_1) x_2 = Filter.map₂ (fun (x x_3 : α) => x + x_3) x (Filter.map₂ (fun (x x_3 : α) => x + x_3) x_1 x_2)
def Filter.addSemigroup {α : Type u_2} [] :

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

Equations
Instances For
def Filter.semigroup {α : Type u_2} [] :

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

Equations
• Filter.semigroup =
Instances For
def Filter.addCommSemigroup {α : Type u_2} [] :

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

Equations
Instances For
theorem Filter.addCommSemigroup.proof_1 {α : Type u_1} [] :
∀ (x x_1 : ), Filter.map₂ (fun (x x_2 : α) => x + x_2) x x_1 = Filter.map₂ (fun (x x_2 : α) => x + x_2) x_1 x
def Filter.commSemigroup {α : Type u_2} [] :

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

Equations
• Filter.commSemigroup = let __src := Filter.semigroup;
Instances For
theorem Filter.addZeroClass.proof_1 {α : Type u_1} [] (l : ) :
Filter.map₂ (fun (x x_1 : α) => x + x_1) (pure 0) l = l
theorem Filter.addZeroClass.proof_2 {α : Type u_1} [] (l : ) :
Filter.map₂ (fun (x x_1 : α) => x + x_1) l (pure 0) = l
def Filter.addZeroClass {α : Type u_2} [] :

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

Equations
Instances For
def Filter.mulOneClass {α : Type u_2} [] :

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

Equations
• Filter.mulOneClass =
Instances For
def Filter.mapAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (φ : F) :

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

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
theorem Filter.mapAddMonoidHom.proof_1 {F : Type u_3} {α : Type u_2} {β : Type u_1} [] [] [FunLike F α β] [] (φ : F) :
Filter.map (φ) 0 = 0
theorem Filter.mapAddMonoidHom.proof_2 {F : Type u_3} {α : Type u_1} {β : Type u_2} [] [] [FunLike F α β] [] (φ : F) :
∀ (x x_1 : ), Filter.map (φ) (x + x_1) = Filter.map (φ) x + Filter.map (φ) x_1
def Filter.mapMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (φ : F) :

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

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
theorem Filter.comap_add_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [AddHomClass F α β] (m : F) {f : } {g : } :
Filter.comap (m) f + Filter.comap (m) g Filter.comap (m) (f + g)
abbrev Filter.comap_add_comap_le.match_1 {F : Type u_3} {α : Type u_1} {β : Type u_2} [] [FunLike F α β] (m : F) {f : } {g : } :
∀ (x : Set α) (motive : x Filter.comap (m) (f + g)Prop) (x_1 : x Filter.comap (m) (f + g)), (∀ (w t₁ : Set β) (ht₁ : t₁ f) (t₂ : Set β) (ht₂ : t₂ g) (t₁t₂ : t₁ + t₂ w) (mt : m ⁻¹' w x), motive )motive x_1
Equations
• =
Instances For
theorem Filter.comap_mul_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [MulHomClass F α β] (m : F) {f : } {g : } :
Filter.comap (m) f * Filter.comap (m) g Filter.comap (m) (f * g)
theorem Filter.Tendsto.add_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [AddHomClass F α β] (m : F) {f₁ : } {g₁ : } {f₂ : } {g₂ : } :
Filter.Tendsto (m) f₁ f₂Filter.Tendsto (m) g₁ g₂Filter.Tendsto (m) (f₁ + g₁) (f₂ + g₂)
theorem Filter.Tendsto.mul_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [MulHomClass F α β] (m : F) {f₁ : } {g₁ : } {f₂ : } {g₂ : } :
Filter.Tendsto (m) f₁ f₂Filter.Tendsto (m) g₁ g₂Filter.Tendsto (m) (f₁ * g₁) (f₂ * g₂)
theorem Filter.pureAddMonoidHom.proof_2 {α : Type u_1} [] (x : α) (y : α) :
theorem Filter.pureAddMonoidHom.proof_1 {α : Type u_1} [] :
Filter.pureZeroHom.toFun 0 = 0
def Filter.pureAddMonoidHom {α : Type u_2} [] :
α →+

pure as an AddMonoidHom.

Equations
• Filter.pureAddMonoidHom = let __src := Filter.pureAddHom; let __src_1 := Filter.pureZeroHom; { toFun := __src.toFun, map_zero' := , map_add' := }
Instances For
def Filter.pureMonoidHom {α : Type u_2} [] :
α →*

pure as a MonoidHom.

Equations
• Filter.pureMonoidHom = let __src := Filter.pureMulHom; let __src_1 := Filter.pureOneHom; { toFun := __src.toFun, map_one' := , map_mul' := }
Instances For
@[simp]
theorem Filter.coe_pureAddMonoidHom {α : Type u_2} [] :
@[simp]
theorem Filter.coe_pureMonoidHom {α : Type u_2} [] :
Filter.pureMonoidHom = pure
@[simp]
theorem Filter.pureAddMonoidHom_apply {α : Type u_2} [] (a : α) :
@[simp]
theorem Filter.pureMonoidHom_apply {α : Type u_2} [] (a : α) :
Filter.pureMonoidHom a = pure a
theorem Filter.addMonoid.proof_4 {α : Type u_1} [] :
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x
def Filter.addMonoid {α : Type u_2} [] :

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

Equations
Instances For
theorem Filter.addMonoid.proof_2 {α : Type u_1} [] (a : ) :
0 + a = a
theorem Filter.addMonoid.proof_1 {α : Type u_1} [] (a : ) (b : ) (c : ) :
a + b + c = a + (b + c)
theorem Filter.addMonoid.proof_3 {α : Type u_1} [] (a : ) :
a + 0 = a
theorem Filter.addMonoid.proof_5 {α : Type u_1} [] :
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
def Filter.monoid {α : Type u_2} [] :

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

Equations
• Filter.monoid = let __src := Filter.mulOneClass; let __src_1 := Filter.semigroup; let __src_2 := Filter.instNPow; Monoid.mk npowRec
Instances For
abbrev Filter.nsmul_mem_nsmul.match_1 (motive : ) :
∀ (x : ), (Unitmotive 0)(∀ (n : ), motive n.succ)motive x
Equations
• =
Instances For
theorem Filter.nsmul_mem_nsmul {α : Type u_2} [] {f : } {s : Set α} (hs : s f) (n : ) :
n s n f
theorem Filter.pow_mem_pow {α : Type u_2} [] {f : } {s : Set α} (hs : s f) (n : ) :
s ^ n f ^ n
@[simp]
theorem Filter.nsmul_bot {α : Type u_2} [] {n : } (hn : n 0) :
@[simp]
theorem Filter.bot_pow {α : Type u_2} [] {n : } (hn : n 0) :
theorem Filter.add_top_of_nonneg {α : Type u_2} [] {f : } (hf : 0 f) :
theorem Filter.mul_top_of_one_le {α : Type u_2} [] {f : } (hf : 1 f) :
theorem Filter.top_add_of_nonneg {α : Type u_2} [] {f : } (hf : 0 f) :
theorem Filter.top_mul_of_one_le {α : Type u_2} [] {f : } (hf : 1 f) :
@[simp]
theorem Filter.top_add_top {α : Type u_2} [] :
@[simp]
theorem Filter.top_mul_top {α : Type u_2} [] :
theorem Filter.nsmul_top {α : Type u_2} [] {n : } :
n 0n =
abbrev Filter.nsmul_top.match_1 (motive : ) :
∀ (x : ), (Unitmotive 0)(Unitmotive 1)(∀ (n : ), motive n.succ.succ)motive x
Equations
• =
Instances For
theorem Filter.top_pow {α : Type u_2} [] {n : } :
n 0 ^ n =
theorem IsAddUnit.filter {α : Type u_2} [] {a : α} :
theorem IsUnit.filter {α : Type u_2} [] {a : α} :
IsUnit (pure a)
theorem Filter.addCommMonoid.proof_6 {α : Type u_1} [] (a : ) (b : ) :
a + b = b + a
theorem Filter.addCommMonoid.proof_1 {α : Type u_1} [] (a : ) (b : ) (c : ) :
a + b + c = a + (b + c)
theorem Filter.addCommMonoid.proof_3 {α : Type u_1} [] (a : ) :
a + 0 = a
def Filter.addCommMonoid {α : Type u_2} [] :

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

Equations
Instances For
theorem Filter.addCommMonoid.proof_5 {α : Type u_1} [] :
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
theorem Filter.addCommMonoid.proof_4 {α : Type u_1} [] :
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x
theorem Filter.addCommMonoid.proof_2 {α : Type u_1} [] (a : ) :
0 + a = a
def Filter.commMonoid {α : Type u_2} [] :

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

Equations
• Filter.commMonoid = let __src := Filter.mulOneClass; let __src_1 := Filter.commSemigroup;
Instances For
theorem Filter.add_eq_zero_iff {α : Type u_2} {f : } {g : } :
f + g = 0 ∃ (a : α) (b : α), f = pure a g = pure b a + b = 0
theorem Filter.mul_eq_one_iff {α : Type u_2} [] {f : } {g : } :
f * g = 1 ∃ (a : α) (b : α), f = pure a g = pure b a * b = 1

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

Equations
• Filter.subtractionMonoid = let __src := Filter.addMonoid; let __src_1 := Filter.instInvolutiveNeg; let __src_2 := Filter.instSub; let __src_3 := Filter.instZSMul;
Instances For
theorem Filter.subtractionMonoid.proof_6 {α : Type u_1} (s : ) (t : ) :
Filter.map Neg.neg (Filter.map₂ (fun (x x_1 : α) => x + x_1) s t) = Filter.map₂ (fun (x x_1 : α) => x + x_1) (Filter.map Neg.neg t) (Filter.map Neg.neg s)
theorem Filter.subtractionMonoid.proof_7 {α : Type u_1} (s : ) (t : ) (h : s + t = 0) :
-s = t
theorem Filter.subtractionMonoid.proof_2 {α : Type u_1} :
∀ (a : ), zsmulRec 0 a = zsmulRec 0 a
theorem Filter.subtractionMonoid.proof_1 {α : Type u_1} (f : ) (g : ) :
Filter.map (fun (x : α) => x) (Filter.map₂ (fun (x x_1 : α) => x - x_1) f g) = Filter.map₂ (fun (x x_1 : α) => x + x_1) f (Filter.map Neg.neg g)
theorem Filter.subtractionMonoid.proof_3 {α : Type u_1} :
∀ (n : ) (a : ), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
theorem Filter.subtractionMonoid.proof_4 {α : Type u_1} :
∀ (n : ) (a : ), zsmulRec () a = zsmulRec () a
theorem Filter.subtractionMonoid.proof_5 {α : Type u_1} (x : ) :
- -x = x
def Filter.divisionMonoid {α : Type u_2} [] :

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

Equations
• Filter.divisionMonoid = let __src := Filter.monoid; let __src_1 := Filter.instInvolutiveInv; let __src_2 := Filter.instDiv; let __src_3 := Filter.instZPow;
Instances For
theorem Filter.isAddUnit_iff {α : Type u_2} {f : } :
∃ (a : α), f = pure a
theorem Filter.isUnit_iff {α : Type u_2} [] {f : } :
∃ (a : α), f = pure a

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

Equations
• Filter.subtractionCommMonoid = let __src := Filter.subtractionMonoid; let __src_1 := Filter.addCommSemigroup;
Instances For
theorem Filter.subtractionCommMonoid.proof_1 {α : Type u_1} (a : ) (b : ) :
a + b = b + a

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

Equations
• Filter.divisionCommMonoid = let __src := Filter.divisionMonoid; let __src_1 := Filter.commSemigroup;
Instances For
def Filter.instDistribNeg {α : Type u_2} [Mul α] [] :

Filter α has distributive negation if α has.

Equations
• Filter.instDistribNeg = let __src := Filter.instInvolutiveNeg;
Instances For

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} [] {f : } {g : } {h : } :
f * (g + h) f * g + f * h
theorem Filter.add_mul_subset {α : Type u_2} [] {f : } {g : } {h : } :
(f + g) * h f * h + g * h

Note that Filter is not a MulZeroClass because 0 * ⊥ ≠ 0.

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

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

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

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

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
def Filter.instSMul {α : Type u_2} {β : Type u_3} [SMul α β] :
SMul () ()

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
@[simp]
theorem Filter.map₂_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } :
Filter.map₂ (fun (x : α) (x_1 : β) => x +ᵥ x_1) f g = f +ᵥ g
@[simp]
theorem Filter.map₂_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } :
Filter.map₂ (fun (x : α) (x_1 : β) => x x_1) f g = f g
theorem Filter.mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } {t : Set β} :
t f +ᵥ g t₁f, t₂g, t₁ +ᵥ t₂ t
theorem Filter.mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } {t : Set β} :
t f g t₁f, t₂g, t₁ t₂ t
theorem Filter.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } {s : Set α} {t : Set β} :
s ft gs +ᵥ t f +ᵥ g
theorem Filter.smul_mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } {s : Set α} {t : Set β} :
s ft gs t f g
@[simp]
theorem Filter.bot_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {g : } :
@[simp]
theorem Filter.bot_smul {α : Type u_2} {β : Type u_3} [SMul α β] {g : } :
@[simp]
theorem Filter.vadd_bot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } :
@[simp]
theorem Filter.smul_bot {α : Type u_2} {β : Type u_3} [SMul α β] {f : } :
@[simp]
theorem Filter.vadd_eq_bot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } :
f +ᵥ g = f = g =
@[simp]
theorem Filter.smul_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } :
f g = f = g =
@[simp]
theorem Filter.vadd_neBot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } :
(f +ᵥ g).NeBot f.NeBot g.NeBot
@[simp]
theorem Filter.smul_neBot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } :
(f g).NeBot f.NeBot g.NeBot
theorem Filter.NeBot.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } :
f.NeBotg.NeBot(f +ᵥ g).NeBot
theorem Filter.NeBot.smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } :
f.NeBotg.NeBot(f g).NeBot
theorem Filter.NeBot.of_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } :
(f +ᵥ g).NeBotf.NeBot
theorem Filter.NeBot.of_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } :
(f g).NeBotf.NeBot
theorem Filter.NeBot.of_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } :
(f +ᵥ g).NeBotg.NeBot
theorem Filter.NeBot.of_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } :
(f g).NeBotg.NeBot
theorem Filter.vadd.instNeBot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } [f.NeBot] [g.NeBot] :
(f +ᵥ g).NeBot
theorem Filter.smul.instNeBot {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } [f.NeBot] [g.NeBot] :
(f g).NeBot
@[simp]
theorem Filter.pure_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {g : } {a : α} :
pure a +ᵥ g = Filter.map (fun (x : β) => a +ᵥ x) g
@[simp]
theorem Filter.pure_smul {α : Type u_2} {β : Type u_3} [SMul α β] {g : } {a : α} :
pure a g = Filter.map (fun (x : β) => a x) g
@[simp]
theorem Filter.vadd_pure {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {b : β} :
f +ᵥ pure b = Filter.map (fun (x : α) => x +ᵥ b) f
@[simp]
theorem Filter.smul_pure {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {b : β} :
f pure b = Filter.map (fun (x : α) => x b) f
theorem Filter.pure_vadd_pure {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} :
pure a +ᵥ pure b = pure (a +ᵥ b)
theorem Filter.pure_smul_pure {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} :
pure a pure b = pure (a b)
theorem Filter.vadd_le_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ : } {f₂ : } {g₁ : } {g₂ : } :
f₁ f₂g₁ g₂f₁ +ᵥ g₁ f₂ +ᵥ g₂
theorem Filter.smul_le_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ : } {f₂ : } {g₁ : } {g₂ : } :
f₁ f₂g₁ g₂f₁ g₁ f₂ g₂
theorem Filter.vadd_le_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g₁ : } {g₂ : } :
g₁ g₂f +ᵥ g₁ f +ᵥ g₂
theorem Filter.smul_le_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g₁ : } {g₂ : } :
g₁ g₂f g₁ f g₂
theorem Filter.vadd_le_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ : } {f₂ : } {g : } :
f₁ f₂f₁ +ᵥ g f₂ +ᵥ g
theorem Filter.smul_le_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ : } {f₂ : } {g : } :
f₁ f₂f₁ g f₂ g
@[simp]
theorem Filter.le_vadd_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {g : } {h : } :
h f +ᵥ g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set β⦄, t gs +ᵥ t h
@[simp]
theorem Filter.le_smul_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {g : } {h : } :
h f g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set β⦄, t gs t h
instance Filter.covariant_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] :
CovariantClass () () (fun (x : ) (x_1 : ) => x +ᵥ x_1) fun (x x_1 : ) => x x_1
Equations
• =
instance Filter.covariant_smul {α : Type u_2} {β : Type u_3} [SMul α β] :
CovariantClass () () (fun (x : ) (x_1 : ) => x x_1) fun (x x_1 : ) => x x_1
Equations
• =

Scalar subtraction of filters #

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

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
@[simp]
theorem Filter.map₂_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } :
Filter.map₂ (fun (x x_1 : β) => x -ᵥ x_1) f g = f -ᵥ g
theorem Filter.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } {s : Set α} :
s f -ᵥ g t₁f, t₂g, t₁ -ᵥ t₂ s
theorem Filter.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } {s : Set β} {t : Set β} :
s ft gs -ᵥ t f -ᵥ g
@[simp]
theorem Filter.bot_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {g : } :
@[simp]
theorem Filter.vsub_bot {α : Type u_2} {β : Type u_3} [VSub α β] {f : } :
@[simp]
theorem Filter.vsub_eq_bot_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } :
f -ᵥ g = f = g =
@[simp]
theorem Filter.vsub_neBot_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } :
(f -ᵥ g).NeBot f.NeBot g.NeBot
theorem Filter.NeBot.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } :
f.NeBotg.NeBot(f -ᵥ g).NeBot
theorem Filter.NeBot.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } :
(f -ᵥ g).NeBotf.NeBot
theorem Filter.NeBot.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } :
(f -ᵥ g).NeBotg.NeBot
theorem Filter.vsub.instNeBot {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } [f.NeBot] [g.NeBot] :
(f -ᵥ g).NeBot
@[simp]
theorem Filter.pure_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {g : } {a : β} :
pure a -ᵥ g = Filter.map (fun (x : β) => a -ᵥ x) g
@[simp]
theorem Filter.vsub_pure {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {b : β} :
f -ᵥ pure b = Filter.map (fun (x : β) => x -ᵥ b) f
theorem Filter.pure_vsub_pure {α : Type u_2} {β : Type u_3} [VSub α β] {a : β} {b : β} :
pure a -ᵥ pure b = pure (a -ᵥ b)
theorem Filter.vsub_le_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f₁ : } {f₂ : } {g₁ : } {g₂ : } :
f₁ f₂g₁ g₂f₁ -ᵥ g₁ f₂ -ᵥ g₂
theorem Filter.vsub_le_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g₁ : } {g₂ : } :
g₁ g₂f -ᵥ g₁ f -ᵥ g₂
theorem Filter.vsub_le_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {f₁ : } {f₂ : } {g : } :
f₁ f₂f₁ -ᵥ g f₂ -ᵥ g
@[simp]
theorem Filter.le_vsub_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f : } {g : } {h : } :
h f -ᵥ g ∀ ⦃s : Set β⦄, s f∀ ⦃t : Set β⦄, t gs -ᵥ t h

Translation/scaling of filters #

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

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

Equations
• Filter.instVAddFilter = { vadd := fun (a : α) => Filter.map fun (x : β) => a +ᵥ x }
Instances For
def Filter.instSMulFilter {α : Type u_2} {β : Type u_3} [SMul α β] :
SMul α ()

a • f is the map of f under a • in locale Pointwise.

Equations
• Filter.instSMulFilter = { smul := fun (a : α) => Filter.map fun (x : β) => a x }
Instances For
@[simp]
theorem Filter.map_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {a : α} :
Filter.map (fun (b : β) => a +ᵥ b) f = a +ᵥ f
@[simp]
theorem Filter.map_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {a : α} :
Filter.map (fun (b : β) => a b) f = a f
theorem Filter.mem_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {s : Set β} {a : α} :
s a +ᵥ f (fun (x : β) => a +ᵥ x) ⁻¹' s f
theorem Filter.mem_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {s : Set β} {a : α} :
s a f (fun (x : β) => a x) ⁻¹' s f
theorem Filter.vadd_set_mem_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {s : Set β} {a : α} :
s fa +ᵥ s a +ᵥ f
theorem Filter.smul_set_mem_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {s : Set β} {a : α} :
s fa s a f
@[simp]
theorem Filter.vadd_filter_bot {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} :
@[simp]
theorem Filter.smul_filter_bot {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} :
@[simp]
theorem Filter.vadd_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {a : α} :
a +ᵥ f = f =
@[simp]
theorem Filter.smul_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {a : α} :
a f = f =
@[simp]
theorem Filter.vadd_filter_neBot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {a : α} :
(a +ᵥ f).NeBot f.NeBot
@[simp]
theorem Filter.smul_filter_neBot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {a : α} :
(a f).NeBot f.NeBot
theorem Filter.NeBot.vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {a : α} :
f.NeBot(a +ᵥ f).NeBot
theorem Filter.NeBot.smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {a : α} :
f.NeBot(a f).NeBot
theorem Filter.NeBot.of_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {a : α} :
(a +ᵥ f).NeBotf.NeBot
theorem Filter.NeBot.of_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {a : α} :
(a f).NeBotf.NeBot
theorem Filter.vadd_filter.instNeBot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : } {a : α} [f.NeBot] :
(a +ᵥ f).NeBot
theorem Filter.smul_filter.instNeBot {α : Type u_2} {β : Type u_3} [SMul α β] {f : } {a : α} [f.NeBot] :
(a f).NeBot
theorem Filter.vadd_filter_le_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ : } {f₂ : } {a : α} (hf : f₁ f₂) :
a +ᵥ f₁ a +ᵥ f₂
theorem Filter.smul_filter_le_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ : } {f₂ : } {a : α} (hf : f₁ f₂) :
a f₁ a f₂
instance Filter.covariant_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] :
CovariantClass α () (fun (x : α) (x_1 : ) => x +ᵥ x_1) fun (x x_1 : ) => x x_1
Equations
• =
instance Filter.covariant_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] :
CovariantClass α () (fun (x : α) (x_1 : ) => x x_1) fun (x x_1 : ) => x x_1
Equations
• =
instance Filter.vaddCommClass_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [] :
Equations
• =
instance Filter.smulCommClass_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [] :
SMulCommClass α β ()
Equations
• =
instance Filter.vaddCommClass_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [] :
Equations
• =
instance Filter.smulCommClass_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [] :
SMulCommClass α () ()
Equations
• =
instance Filter.vaddCommClass_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [] :
Equations
• =
instance Filter.smulCommClass_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [] :
SMulCommClass () β ()
Equations
• =
instance Filter.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [] :
Equations
• =
instance Filter.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [] :
SMulCommClass () () ()
Equations
• =
instance Filter.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [] :
Equations
• =
instance Filter.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [] :
IsScalarTower α β ()
Equations
• =
instance Filter.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [] :
Equations
• =
instance Filter.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [] :
IsScalarTower α () ()
Equations
• =
instance Filter.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [] :
Equations
• =
instance Filter.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [] :
IsScalarTower () () ()
Equations
• =
instance Filter.isCentralVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] [VAdd αᵃᵒᵖ β] [] :
Equations
• =
instance Filter.isCentralScalar {α : Type u_2} {β : Type u_3} [SMul α β] [SMul αᵐᵒᵖ β] [] :
Equations
• =
def Filter.addAction {α : Type u_2} {β : Type u_3} [] [] :

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

Equations
Instances For
theorem Filter.addAction.proof_2 {α : Type u_1} {β : Type u_2} [] [] (f : ) (g : ) (h : ) :
Filter.map₂ (fun (x : α) (x_1 : β) => x +ᵥ x_1) (Filter.map₂ (fun (x x_1 : α) => x + x_1) f g) h = Filter.map₂ (fun (x : α) (x_1 : β) => x +ᵥ x_1) f (Filter.map₂ (fun (x : α) (x_1 : β) => x +ᵥ x_1) g h)
theorem Filter.addAction.proof_1 {α : Type u_2} {β : Type u_1} [] [] (f : ) :
Filter.map₂ (fun (x : α) (x_1 : β) => x +ᵥ x_1) (pure 0) f = f
def Filter.mulAction {α : Type u_2} {β : Type u_3} [] [] :
MulAction () ()

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

Equations
• Filter.mulAction =
Instances For
theorem Filter.addActionFilter.proof_1 {α : Type u_2} {β : Type u_1} [] [] (f : ) :
Filter.map (fun (x : β) => 0 +ᵥ x) f = f
def Filter.addActionFilter {α : Type u_2} {β : Type u_3} [] [] :

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

Equations
Instances For
theorem Filter.addActionFilter.proof_2 {α : Type u_2} {β : Type u_1} [] [] (a : α) (b : α) (f : ) :
Filter.map (fun (b_1 : β) => a + b +ᵥ b_1) f = Filter.map (fun (b : β) => a +ᵥ b) (Filter.map (fun (b_1 : β) => b +ᵥ b_1) f)
def Filter.mulActionFilter {α : Type u_2} {β : Type u_3} [] [] :
MulAction α ()

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

Equations
• Filter.mulActionFilter =
Instances For
def Filter.distribMulActionFilter {α : Type u_2} {β : Type u_3} [] [] [] :

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

Equations
• Filter.distribMulActionFilter =
Instances For
def Filter.mulDistribMulActionFilter {α : Type u_2} {β : Type u_3} [] [] [] :

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

Equations
• Filter.mulDistribMulActionFilter =
Instances For

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

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