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

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

0/1 as filters

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

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

Equations

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

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

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

Equations

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

@[simp]

theorem Filter.mem_one {α : Type u_2} [One α] {s : Set α} : s ∈ 1 ↔ 1 ∈ s

@[simp]

theorem Filter.mem_zero {α : Type u_2} [Zero α] {s : Set α} : s ∈ 0 ↔ 0 ∈ s

theorem Filter.one_mem_one {α : Type u_2} [One α] : 1 ∈ 1

theorem Filter.zero_mem_zero {α : Type u_2} [Zero α] : 0 ∈ 0

@[simp]

theorem Filter.pure_one {α : Type u_2} [One α] : pure 1 = 1

@[simp]

theorem Filter.pure_zero {α : Type u_2} [Zero α] : pure 0 = 0

@[simp]

theorem Filter.one_prod {α : Type u_2} {β : Type u_3} [One α] {l : Filter β} : 1 ×ˢ l = map (fun (x : β) => (1, x)) l

@[simp]

theorem Filter.zero_prod {α : Type u_2} {β : Type u_3} [Zero α] {l : Filter β} : 0 ×ˢ l = map (fun (x : β) => (0, x)) l

@[simp]

theorem Filter.prod_one {α : Type u_2} {β : Type u_3} [One α] {l : Filter β} : l ×ˢ 1 = map (fun (x : β) => (x, 1)) l

@[simp]

theorem Filter.prod_zero {α : Type u_2} {β : Type u_3} [Zero α] {l : Filter β} : l ×ˢ 0 = map (fun (x : β) => (x, 0)) l

@[simp]

theorem Filter.principal_one {α : Type u_2} [One α] : principal 1 = 1

@[simp]

theorem Filter.principal_zero {α : Type u_2} [Zero α] : principal 0 = 0

theorem Filter.one_neBot {α : Type u_2} [One α] : NeBot 1

theorem Filter.zero_neBot {α : Type u_2} [Zero α] : NeBot 0

@[simp]

theorem Filter.map_one' {α : Type u_2} {β : Type u_3} [One α] (f : α → β) : map f 1 = pure (f 1)

@[simp]

theorem Filter.map_zero' {α : Type u_2} {β : Type u_3} [Zero α] (f : α → β) : map f 0 = pure (f 0)

@[simp]

theorem Filter.le_one_iff {α : Type u_2} [One α] {f : Filter α} : f ≤ 1 ↔ 1 ∈ f

@[simp]

theorem Filter.nonpos_iff {α : Type u_2} [Zero α] {f : Filter α} : f ≤ 0 ↔ 0 ∈ f

theorem Filter.NeBot.le_one_iff {α : Type u_2} [One α] {f : Filter α} (h : f.NeBot) : f ≤ 1 ↔ f = 1

theorem Filter.NeBot.nonpos_iff {α : Type u_2} [Zero α] {f : Filter α} (h : f.NeBot) : f ≤ 0 ↔ f = 0

@[simp]

theorem Filter.eventually_one {α : Type u_2} [One α] {p : α → Prop} : (∀ᶠ (x : α) in 1, p x) ↔ p 1

@[simp]

theorem Filter.eventually_zero {α : Type u_2} [Zero α] {p : α → Prop} : (∀ᶠ (x : α) in 0, p x) ↔ p 0

@[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

@[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

theorem Filter.one_prod_one {α : Type u_2} {β : Type u_3} [One α] [One β] : 1 ×ˢ 1 = 1

theorem Filter.zero_prod_zero {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] : 0 ×ˢ 0 = 0

def Filter.pureOneHom {α : Type u_2} [One α] : OneHom α (Filter α)

pure as a OneHom.

Equations

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

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

pure as a ZeroHom.

Equations

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

@[simp]

theorem Filter.coe_pureOneHom {α : Type u_2} [One α] : ⇑pureOneHom = pure

@[simp]

theorem Filter.coe_pureZeroHom {α : Type u_2} [Zero α] : ⇑pureZeroHom = pure

@[simp]

theorem Filter.pureOneHom_apply {α : Type u_2} [One α] (a : α) : pureOneHom a = pure a

@[simp]

theorem Filter.pureZeroHom_apply {α : Type u_2} [Zero α] (a : α) : pureZeroHom a = pure a

theorem Filter.map_one {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [One β] [FunLike F α β] [OneHomClass F α β] (φ : F) : map (⇑φ) 1 = 1

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

instance 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 }

instance 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 }

@[simp]

theorem Filter.map_inv {α : Type u_2} [Inv α] {f : Filter α} : map Inv.inv f = f⁻¹

@[simp]

theorem Filter.map_neg {α : Type u_2} [Neg α] {f : Filter α} : map Neg.neg f = -f

theorem Filter.mem_inv {α : Type u_2} [Inv α] {f : Filter α} {s : Set α} : s ∈ f⁻¹ ↔ Inv.inv ⁻¹' s ∈ f

theorem Filter.mem_neg {α : Type u_2} [Neg α] {f : Filter α} {s : Set α} : s ∈ -f ↔ Neg.neg ⁻¹' s ∈ f

theorem Filter.inv_le_inv {α : Type u_2} [Inv α] {f g : Filter α} (hf : f ≤ g) : f⁻¹ ≤ g⁻¹

theorem Filter.neg_le_neg {α : Type u_2} [Neg α] {f g : Filter α} (hf : f ≤ g) : -f ≤ -g

@[simp]

theorem Filter.inv_pure {α : Type u_2} [Inv α] {a : α} : (pure a)⁻¹ = pure a⁻¹

@[simp]

theorem Filter.neg_pure {α : Type u_2} [Neg α] {a : α} : -pure a = pure (-a)

@[simp]

theorem Filter.inv_eq_bot_iff {α : Type u_2} [Inv α] {f : Filter α} : f⁻¹ = ⊥ ↔ f = ⊥

@[simp]

theorem Filter.neg_eq_bot_iff {α : Type u_2} [Neg α] {f : Filter α} : -f = ⊥ ↔ f = ⊥

@[simp]

theorem Filter.neBot_inv_iff {α : Type u_2} [Inv α] {f : Filter α} : f⁻¹.NeBot ↔ f.NeBot

@[simp]

theorem Filter.neBot_neg_iff {α : Type u_2} [Neg α] {f : Filter α} : (-f).NeBot ↔ f.NeBot

theorem Filter.NeBot.inv {α : Type u_2} [Inv α] {f : Filter α} : f.NeBot → f⁻¹.NeBot

theorem Filter.NeBot.neg {α : Type u_2} [Neg α] {f : Filter α} : f.NeBot → (-f).NeBot

theorem Filter.inv.instNeBot {α : Type u_2} [Inv α] {f : Filter α} [f.NeBot] : f⁻¹.NeBot

theorem Filter.neg.instNeBot {α : Type u_2} [Neg α] {f : Filter α} [f.NeBot] : (-f).NeBot

@[simp]

theorem Filter.comap_inv {α : Type u_2} [InvolutiveInv α] {f : Filter α} : comap Inv.inv f = f⁻¹

@[simp]

theorem Filter.comap_neg {α : Type u_2} [InvolutiveNeg α] {f : Filter α} : comap Neg.neg f = -f

theorem Filter.inv_mem_inv {α : Type u_2} [InvolutiveInv α] {f : Filter α} {s : Set α} (hs : s ∈ f) : s⁻¹ ∈ f⁻¹

theorem Filter.neg_mem_neg {α : Type u_2} [InvolutiveNeg α] {f : Filter α} {s : Set α} (hs : s ∈ f) : -s ∈ -f

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 := ⋯ }

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 := ⋯ }

@[simp]

theorem Filter.inv_le_inv_iff {α : Type u_2} [InvolutiveInv α] {f g : Filter α} : f⁻¹ ≤ g⁻¹ ↔ f ≤ g

@[simp]

theorem Filter.neg_le_neg_iff {α : Type u_2} [InvolutiveNeg α] {f g : Filter α} : -f ≤ -g ↔ f ≤ g

theorem Filter.inv_le_iff_le_inv {α : Type u_2} [InvolutiveInv α] {f g : Filter α} : f⁻¹ ≤ g ↔ f ≤ g⁻¹

theorem Filter.neg_le_iff_le_neg {α : Type u_2} [InvolutiveNeg α] {f g : Filter α} : -f ≤ g ↔ f ≤ -g

@[simp]

theorem Filter.inv_le_self {α : Type u_2} [InvolutiveInv α] {f : Filter α} : f⁻¹ ≤ f ↔ f⁻¹ = f

@[simp]

theorem Filter.neg_le_self {α : Type u_2} [InvolutiveNeg α] {f : Filter α} : -f ≤ f ↔ -f = f

@[simp]

theorem Filter.inv_atTop {G : Type u_7} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : atTop⁻¹ = atBot

@[simp]

theorem Filter.neg_atTop {G : Type u_7} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : -atTop = atBot

Filter addition/multiplication

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

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

@[simp]

theorem Filter.map₂_mul {α : Type u_2} [Mul α] {f g : Filter α} : map₂ (fun (x1 x2 : α) => x1 * x2) f g = f * g

@[simp]

theorem Filter.map₂_add {α : Type u_2} [Add α] {f g : Filter α} : map₂ (fun (x1 x2 : α) => x1 + x2) f g = f + g

theorem Filter.mem_mul {α : Type u_2} [Mul α] {f g : Filter α} {s : Set α} : s ∈ f * g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s

theorem Filter.mem_add {α : Type u_2} [Add α] {f g : Filter α} {s : Set α} : s ∈ f + g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ + t₂ ⊆ s

theorem Filter.mul_mem_mul {α : Type u_2} [Mul α] {f g : Filter α} {s t : Set α} : s ∈ f → t ∈ g → s * t ∈ f * g

theorem Filter.add_mem_add {α : Type u_2} [Add α] {f g : Filter α} {s t : Set α} : s ∈ f → t ∈ g → s + t ∈ f + g

@[simp]

theorem Filter.bot_mul {α : Type u_2} [Mul α] {g : Filter α} : ⊥ * g = ⊥

@[simp]

theorem Filter.bot_add {α : Type u_2} [Add α] {g : Filter α} : ⊥ + g = ⊥

@[simp]

theorem Filter.mul_bot {α : Type u_2} [Mul α] {f : Filter α} : f * ⊥ = ⊥

@[simp]

theorem Filter.add_bot {α : Type u_2} [Add α] {f : Filter α} : f + ⊥ = ⊥

@[simp]

theorem Filter.mul_eq_bot_iff {α : Type u_2} [Mul α] {f g : Filter α} : f * g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.add_eq_bot_iff {α : Type u_2} [Add α] {f g : Filter α} : f + g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.mul_neBot_iff {α : Type u_2} [Mul α] {f g : Filter α} : (f * g).NeBot ↔ f.NeBot ∧ g.NeBot

@[simp]

theorem Filter.add_neBot_iff {α : Type u_2} [Add α] {f g : Filter α} : (f + g).NeBot ↔ f.NeBot ∧ g.NeBot

theorem Filter.NeBot.mul {α : Type u_2} [Mul α] {f g : Filter α} : f.NeBot → g.NeBot → (f * g).NeBot

theorem Filter.NeBot.add {α : Type u_2} [Add α] {f g : Filter α} : f.NeBot → g.NeBot → (f + g).NeBot

theorem Filter.NeBot.of_mul_left {α : Type u_2} [Mul α] {f g : Filter α} : (f * g).NeBot → f.NeBot

theorem Filter.NeBot.of_add_left {α : Type u_2} [Add α] {f g : Filter α} : (f + g).NeBot → f.NeBot

theorem Filter.NeBot.of_mul_right {α : Type u_2} [Mul α] {f g : Filter α} : (f * g).NeBot → g.NeBot

theorem Filter.NeBot.of_add_right {α : Type u_2} [Add α] {f g : Filter α} : (f + g).NeBot → g.NeBot

theorem Filter.mul.instNeBot {α : Type u_2} [Mul α] {f g : Filter α} [f.NeBot] [g.NeBot] : (f * g).NeBot

theorem Filter.add.instNeBot {α : Type u_2} [Add α] {f g : Filter α} [f.NeBot] [g.NeBot] : (f + g).NeBot

@[simp]

theorem Filter.pure_mul {α : Type u_2} [Mul α] {g : Filter α} {a : α} : pure a * g = map (fun (x : α) => a * x) g

@[simp]

theorem Filter.pure_add {α : Type u_2} [Add α] {g : Filter α} {a : α} : pure a + g = map (fun (x : α) => a + x) g

@[simp]

theorem Filter.mul_pure {α : Type u_2} [Mul α] {f : Filter α} {b : α} : f * pure b = map (fun (x : α) => x * b) f

@[simp]

theorem Filter.add_pure {α : Type u_2} [Add α] {f : Filter α} {b : α} : f + pure b = map (fun (x : α) => x + b) f

theorem Filter.pure_mul_pure {α : Type u_2} [Mul α] {a b : α} : pure a * pure b = pure (a * b)

theorem Filter.pure_add_pure {α : Type u_2} [Add α] {a b : α} : pure a + pure b = pure (a + b)

@[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

@[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

instance Filter.mulLeftMono {α : Type u_2} [Mul α] : MulLeftMono (Filter α)

instance Filter.addLeftMono {α : Type u_2} [Add α] : AddLeftMono (Filter α)

instance Filter.mulRightMono {α : Type u_2} [Mul α] : MulRightMono (Filter α)

instance Filter.addRightMono {α : Type u_2} [Add α] : AddRightMono (Filter α)

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₂

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₂

def Filter.pureMulHom {α : Type u_2} [Mul α] : α →ₙ* Filter α

pure operation as a MulHom.

Equations

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

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

The singleton operation as an AddHom.

Equations

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

@[simp]

theorem Filter.coe_pureMulHom {α : Type u_2} [Mul α] : ⇑pureMulHom = pure

@[simp]

theorem Filter.coe_pureAddHom {α : Type u_2} [Add α] : ⇑pureAddHom = pure

@[simp]

theorem Filter.pureMulHom_apply {α : Type u_2} [Mul α] (a : α) : pureMulHom a = pure a

@[simp]

theorem Filter.pureAddHom_apply {α : Type u_2} [Add α] (a : α) : pureAddHom a = pure a

Filter subtraction/division

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

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

@[simp]

theorem Filter.map₂_div {α : Type u_2} [Div α] {f g : Filter α} : map₂ (fun (x1 x2 : α) => x1 / x2) f g = f / g

@[simp]

theorem Filter.map₂_sub {α : Type u_2} [Sub α] {f g : Filter α} : map₂ (fun (x1 x2 : α) => x1 - x2) f g = f - g

theorem Filter.mem_div {α : Type u_2} [Div α] {f g : Filter α} {s : Set α} : s ∈ f / g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s

theorem Filter.mem_sub {α : Type u_2} [Sub α] {f g : Filter α} {s : Set α} : s ∈ f - g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ - t₂ ⊆ s

theorem Filter.div_mem_div {α : Type u_2} [Div α] {f g : Filter α} {s t : Set α} : s ∈ f → t ∈ g → s / t ∈ f / g

theorem Filter.sub_mem_sub {α : Type u_2} [Sub α] {f g : Filter α} {s t : Set α} : s ∈ f → t ∈ g → s - t ∈ f - g

@[simp]

theorem Filter.bot_div {α : Type u_2} [Div α] {g : Filter α} : ⊥ / g = ⊥

@[simp]

theorem Filter.bot_sub {α : Type u_2} [Sub α] {g : Filter α} : ⊥ - g = ⊥

@[simp]

theorem Filter.div_bot {α : Type u_2} [Div α] {f : Filter α} : f / ⊥ = ⊥

@[simp]

theorem Filter.sub_bot {α : Type u_2} [Sub α] {f : Filter α} : f - ⊥ = ⊥

@[simp]

theorem Filter.div_eq_bot_iff {α : Type u_2} [Div α] {f g : Filter α} : f / g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.sub_eq_bot_iff {α : Type u_2} [Sub α] {f g : Filter α} : f - g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.div_neBot_iff {α : Type u_2} [Div α] {f g : Filter α} : (f / g).NeBot ↔ f.NeBot ∧ g.NeBot

@[simp]

theorem Filter.sub_neBot_iff {α : Type u_2} [Sub α] {f g : Filter α} : (f - g).NeBot ↔ f.NeBot ∧ g.NeBot

theorem Filter.NeBot.div {α : Type u_2} [Div α] {f g : Filter α} : f.NeBot → g.NeBot → (f / g).NeBot

theorem Filter.NeBot.sub {α : Type u_2} [Sub α] {f g : Filter α} : f.NeBot → g.NeBot → (f - g).NeBot

theorem Filter.NeBot.of_div_left {α : Type u_2} [Div α] {f g : Filter α} : (f / g).NeBot → f.NeBot

theorem Filter.NeBot.of_sub_left {α : Type u_2} [Sub α] {f g : Filter α} : (f - g).NeBot → f.NeBot

theorem Filter.NeBot.of_div_right {α : Type u_2} [Div α] {f g : Filter α} : (f / g).NeBot → g.NeBot

theorem Filter.NeBot.of_sub_right {α : Type u_2} [Sub α] {f g : Filter α} : (f - g).NeBot → g.NeBot

theorem Filter.div.instNeBot {α : Type u_2} [Div α] {f g : Filter α} [f.NeBot] [g.NeBot] : (f / g).NeBot

theorem Filter.sub.instNeBot {α : Type u_2} [Sub α] {f g : Filter α} [f.NeBot] [g.NeBot] : (f - g).NeBot

@[simp]

theorem Filter.pure_div {α : Type u_2} [Div α] {g : Filter α} {a : α} : pure a / g = map (fun (x : α) => a / x) g

@[simp]

theorem Filter.pure_sub {α : Type u_2} [Sub α] {g : Filter α} {a : α} : pure a - g = map (fun (x : α) => a - x) g

@[simp]

theorem Filter.div_pure {α : Type u_2} [Div α] {f : Filter α} {b : α} : f / pure b = map (fun (x : α) => x / b) f

@[simp]

theorem Filter.sub_pure {α : Type u_2} [Sub α] {f : Filter α} {b : α} : f - pure b = map (fun (x : α) => x - b) f

theorem Filter.pure_div_pure {α : Type u_2} [Div α] {a b : α} : pure a / pure b = pure (a / b)

theorem Filter.pure_sub_pure {α : Type u_2} [Sub α] {a b : α} : pure a - pure b = pure (a - b)

theorem Filter.div_le_div {α : Type u_2} [Div α] {f₁ f₂ g₁ g₂ : Filter α} : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ / g₁ ≤ f₂ / g₂

theorem Filter.sub_le_sub {α : Type u_2} [Sub α] {f₁ f₂ g₁ g₂ : Filter α} : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ - g₁ ≤ f₂ - g₂

theorem Filter.div_le_div_left {α : Type u_2} [Div α] {f g₁ g₂ : Filter α} : g₁ ≤ g₂ → f / g₁ ≤ f / g₂

theorem Filter.sub_le_sub_left {α : Type u_2} [Sub α] {f g₁ g₂ : Filter α} : g₁ ≤ g₂ → f - g₁ ≤ f - g₂

theorem Filter.div_le_div_right {α : Type u_2} [Div α] {f₁ f₂ g : Filter α} : f₁ ≤ f₂ → f₁ / g ≤ f₂ / g

theorem Filter.sub_le_sub_right {α : Type u_2} [Sub α] {f₁ f₂ g : Filter α} : f₁ ≤ f₂ → f₁ - g ≤ f₂ - g

@[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

@[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

instance Filter.covariant_div {α : Type u_2} [Div α] : CovariantClass (Filter α) (Filter α) (fun (x1 x2 : Filter α) => x1 / x2) fun (x1 x2 : Filter α) => x1 ≤ x2

instance Filter.covariant_sub {α : Type u_2} [Sub α] : CovariantClass (Filter α) (Filter α) (fun (x1 x2 : Filter α) => x1 - x2) fun (x1 x2 : Filter α) => x1 ≤ x2

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

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

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 }

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 }

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 }

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 }

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

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

Equations

• Filter.semigroup = { mul := fun (x1 x2 : Filter α) => x1 * x2, mul_assoc := ⋯ }

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

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

Equations

• Filter.addSemigroup = { add := fun (x1 x2 : Filter α) => x1 + x2, add_assoc := ⋯ }

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 := ⋯ }

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 := ⋯ }

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

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

Equations

• Filter.mulOneClass = { one := 1, mul := fun (x1 x2 : Filter α) => x1 * x2, one_mul := ⋯, mul_one := ⋯ }

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

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

Equations

• Filter.addZeroClass = { zero := 0, add := fun (x1 x2 : Filter α) => x1 + x2, zero_add := ⋯, add_zero := ⋯ }

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' := ⋯ }

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' := ⋯ }

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)

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)

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₂)

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₂)

def Filter.pureMonoidHom {α : Type u_2} [MulOneClass α] : α →* Filter α

pure as a MonoidHom.

Equations

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

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

pure as an AddMonoidHom.

Equations

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

@[simp]

theorem Filter.coe_pureMonoidHom {α : Type u_2} [MulOneClass α] : ⇑pureMonoidHom = pure

@[simp]

theorem Filter.coe_pureAddMonoidHom {α : Type u_2} [AddZeroClass α] : ⇑pureAddMonoidHom = pure

@[simp]

theorem Filter.pureMonoidHom_apply {α : Type u_2} [MulOneClass α] (a : α) : pureMonoidHom a = pure a

@[simp]

theorem Filter.pureAddMonoidHom_apply {α : Type u_2} [AddZeroClass α] (a : α) : pureAddMonoidHom a = pure a

def Filter.monoid {α : Type u_2} [Monoid α] : Monoid (Filter α)

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

Equations

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

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

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

Equations

• Filter.addMonoid = { toAdd := AddZeroClass.toAdd, add_assoc := ⋯, toZero := AddZeroClass.toZero, zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯ }

theorem Filter.pow_mem_pow {α : Type u_2} [Monoid α] {f : Filter α} {s : Set α} (hs : s ∈ f) (n : ℕ) : s ^ n ∈ f ^ n

theorem Filter.nsmul_mem_nsmul {α : Type u_2} [AddMonoid α] {f : Filter α} {s : Set α} (hs : s ∈ f) (n : ℕ) : n • s ∈ n • f

@[simp]

theorem Filter.bot_pow {α : Type u_2} [Monoid α] {n : ℕ} (hn : n ≠ 0) : ⊥ ^ n = ⊥

@[simp]

theorem Filter.nsmul_bot {α : Type u_2} [AddMonoid α] {n : ℕ} (hn : n ≠ 0) : n • ⊥ = ⊥

theorem Filter.mul_top_of_one_le {α : Type u_2} [Monoid α] {f : Filter α} (hf : 1 ≤ f) : f * ⊤ = ⊤

theorem Filter.add_top_of_nonneg {α : Type u_2} [AddMonoid α] {f : Filter α} (hf : 0 ≤ f) : f + ⊤ = ⊤

theorem Filter.top_mul_of_one_le {α : Type u_2} [Monoid α] {f : Filter α} (hf : 1 ≤ f) : ⊤ * f = ⊤

theorem Filter.top_add_of_nonneg {α : Type u_2} [AddMonoid α] {f : Filter α} (hf : 0 ≤ f) : ⊤ + f = ⊤

@[simp]

theorem Filter.top_mul_top {α : Type u_2} [Monoid α] : ⊤ * ⊤ = ⊤

@[simp]

theorem Filter.top_add_top {α : Type u_2} [AddMonoid α] : ⊤ + ⊤ = ⊤

theorem Filter.top_pow {α : Type u_2} [Monoid α] {n : ℕ} : n ≠ 0 → ⊤ ^ n = ⊤

theorem Filter.nsmul_top {α : Type u_2} [AddMonoid α] {n : ℕ} : n ≠ 0 → n • ⊤ = ⊤

theorem IsUnit.filter {α : Type u_2} [Monoid α] {a : α} : IsUnit a → IsUnit (pure a)

theorem IsAddUnit.filter {α : Type u_2} [AddMonoid α] {a : α} : IsAddUnit a → IsAddUnit (pure a)

def Filter.commMonoid {α : Type u_2} [CommMonoid α] : CommMonoid (Filter α)

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

Equations

• Filter.commMonoid = { toMul := MulOneClass.toMul, mul_assoc := ⋯, toOne := MulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }

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.

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

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

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.

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.

theorem Filter.isUnit_iff {α : Type u_2} [DivisionMonoid α] {f : Filter α} : IsUnit f ↔ ∃ (a : α), f = pure a ∧ IsUnit a

theorem Filter.isAddUnit_iff {α : Type u_2} [SubtractionMonoid α] {f : Filter α} : IsAddUnit f ↔ ∃ (a : α), f = pure a ∧ IsAddUnit a

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 := ⋯ }

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 := ⋯ }

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 := ⋯ }

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

theorem Filter.mul_add_subset {α : Type u_2} [Distrib α] {f g h : Filter α} : f * (g + h) ≤ f * g + f * h

theorem Filter.add_mul_subset {α : Type u_2} [Distrib α] {f g h : Filter α} : (f + g) * h ≤ f * h + g * h

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

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

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

@[simp]

theorem Filter.one_le_div_iff {α : Type u_2} [Group α] {f g : Filter α} : 1 ≤ f / g ↔ ¬Disjoint f g

@[simp]

theorem Filter.nonneg_sub_iff {α : Type u_2} [AddGroup α] {f g : Filter α} : 0 ≤ f - g ↔ ¬Disjoint f g

theorem Filter.not_one_le_div_iff {α : Type u_2} [Group α] {f g : Filter α} : ¬1 ≤ f / g ↔ Disjoint f g

theorem Filter.not_nonneg_sub_iff {α : Type u_2} [AddGroup α] {f g : Filter α} : ¬0 ≤ f - g ↔ Disjoint f g

theorem Filter.NeBot.one_le_div {α : Type u_2} [Group α] {f : Filter α} (h : f.NeBot) : 1 ≤ f / f

theorem Filter.NeBot.nonneg_sub {α : Type u_2} [AddGroup α] {f : Filter α} (h : f.NeBot) : 0 ≤ f - f

theorem Filter.isUnit_pure {α : Type u_2} [Group α] (a : α) : IsUnit (pure a)

theorem Filter.isAddUnit_pure {α : Type u_2} [AddGroup α] (a : α) : IsAddUnit (pure a)

@[simp]

theorem Filter.isUnit_iff_singleton {α : Type u_2} [Group α] {f : Filter α} : IsUnit f ↔ ∃ (a : α), f = pure a

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)⁻¹

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

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₂⁻¹

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₂)

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

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

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₂)

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₂)

theorem Filter.NeBot.div_zero_nonneg {α : Type u_2} [GroupWithZero α] {f : Filter α} (hf : f.NeBot) : 0 ≤ f / 0

theorem Filter.NeBot.zero_div_nonneg {α : Type u_2} [GroupWithZero α] {g : Filter α} (hg : g.NeBot) : 0 ≤ 0 / g

Scalar addition/multiplication of filters

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 locale Pointwise.

Equations

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

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.

@[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

@[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

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

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

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

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

@[simp]

theorem Filter.bot_smul {α : Type u_2} {β : Type u_3} [SMul α β] {g : Filter β} : ⊥ • g = ⊥

@[simp]

theorem Filter.bot_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {g : Filter β} : ⊥ +ᵥ g = ⊥

@[simp]

theorem Filter.smul_bot {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} : f • ⊥ = ⊥

@[simp]

theorem Filter.vadd_bot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} : f +ᵥ ⊥ = ⊥

@[simp]

theorem Filter.smul_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} : f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.vadd_eq_bot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} : f +ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.smul_neBot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} : (f • g).NeBot ↔ f.NeBot ∧ g.NeBot

@[simp]

theorem Filter.vadd_neBot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} : (f +ᵥ g).NeBot ↔ f.NeBot ∧ g.NeBot

theorem Filter.NeBot.smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} : f.NeBot → g.NeBot → (f • g).NeBot

theorem Filter.NeBot.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} : f.NeBot → g.NeBot → (f +ᵥ g).NeBot

theorem Filter.NeBot.of_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} : (f • g).NeBot → f.NeBot

theorem Filter.NeBot.of_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} : (f +ᵥ g).NeBot → f.NeBot

theorem Filter.NeBot.of_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} : (f • g).NeBot → g.NeBot

theorem Filter.NeBot.of_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} : (f +ᵥ g).NeBot → g.NeBot

theorem Filter.smul.instNeBot {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} [f.NeBot] [g.NeBot] : (f • g).NeBot

theorem Filter.vadd.instNeBot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} [f.NeBot] [g.NeBot] : (f +ᵥ g).NeBot

@[simp]

theorem Filter.pure_smul {α : Type u_2} {β : Type u_3} [SMul α β] {g : Filter β} {a : α} : pure a • g = map (fun (x : β) => a • x) g

@[simp]

theorem Filter.pure_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {g : Filter β} {a : α} : pure a +ᵥ g = map (fun (x : β) => a +ᵥ x) g

@[simp]

theorem Filter.smul_pure {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {b : β} : f • pure b = map (fun (x : α) => x • b) f

@[simp]

theorem Filter.vadd_pure {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {b : β} : f +ᵥ pure b = map (fun (x : α) => x +ᵥ b) f

theorem Filter.pure_smul_pure {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} : pure a • pure b = pure (a • b)

theorem Filter.pure_vadd_pure {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} : pure a +ᵥ pure b = pure (a +ᵥ b)

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₂

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₂

theorem Filter.smul_le_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g₁ g₂ : Filter β} : g₁ ≤ g₂ → f • g₁ ≤ f • g₂

theorem Filter.vadd_le_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g₁ g₂ : Filter β} : g₁ ≤ g₂ → f +ᵥ g₁ ≤ f +ᵥ g₂

theorem Filter.smul_le_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ f₂ : Filter α} {g : Filter β} : f₁ ≤ f₂ → f₁ • g ≤ f₂ • g

theorem Filter.vadd_le_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ f₂ : Filter α} {g : Filter β} : f₁ ≤ f₂ → f₁ +ᵥ g ≤ f₂ +ᵥ g

@[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

@[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

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

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

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 locale Pointwise.

Equations

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

@[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

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

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

@[simp]

theorem Filter.bot_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {g : Filter β} : ⊥ -ᵥ g = ⊥

@[simp]

theorem Filter.vsub_bot {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} : f -ᵥ ⊥ = ⊥

@[simp]

theorem Filter.vsub_eq_bot_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} : f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.vsub_neBot_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} : (f -ᵥ g).NeBot ↔ f.NeBot ∧ g.NeBot

theorem Filter.NeBot.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} : f.NeBot → g.NeBot → (f -ᵥ g).NeBot

theorem Filter.NeBot.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} : (f -ᵥ g).NeBot → f.NeBot

theorem Filter.NeBot.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} : (f -ᵥ g).NeBot → g.NeBot

theorem Filter.vsub.instNeBot {α : Type u_2} {β : Type u_3} [VSub α β] {f g : Filter β} [f.NeBot] [g.NeBot] : (f -ᵥ g).NeBot

@[simp]

theorem Filter.pure_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {g : Filter β} {a : β} : pure a -ᵥ g = map (fun (x : β) => a -ᵥ x) g

@[simp]

theorem Filter.vsub_pure {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {b : β} : f -ᵥ pure b = 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₂ : Filter β} : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ -ᵥ g₁ ≤ f₂ -ᵥ g₂

theorem Filter.vsub_le_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {f g₁ g₂ : Filter β} : g₁ ≤ g₂ → f -ᵥ g₁ ≤ f -ᵥ g₂

theorem Filter.vsub_le_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {f₁ f₂ g : Filter β} : f₁ ≤ f₂ → f₁ -ᵥ g ≤ f₂ -ᵥ g

@[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

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

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

Equations

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

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

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

Equations

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

@[simp]

theorem Filter.map_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} : map (fun (b : β) => a • b) f = a • f

@[simp]

theorem Filter.map_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} : map (fun (b : β) => a +ᵥ b) f = a +ᵥ f

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

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

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

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

@[simp]

theorem Filter.smul_filter_bot {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} : a • ⊥ = ⊥

@[simp]

theorem Filter.vadd_filter_bot {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} : a +ᵥ ⊥ = ⊥

@[simp]

theorem Filter.smul_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} : a • f = ⊥ ↔ f = ⊥

@[simp]

theorem Filter.vadd_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} : a +ᵥ f = ⊥ ↔ f = ⊥

@[simp]

theorem Filter.smul_filter_neBot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} : (a • f).NeBot ↔ f.NeBot

@[simp]

theorem Filter.vadd_filter_neBot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} : (a +ᵥ f).NeBot ↔ f.NeBot

theorem Filter.NeBot.smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} : f.NeBot → (a • f).NeBot

theorem Filter.NeBot.vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} : f.NeBot → (a +ᵥ f).NeBot

theorem Filter.NeBot.of_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} : (a • f).NeBot → f.NeBot

theorem Filter.NeBot.of_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} : (a +ᵥ f).NeBot → f.NeBot

theorem Filter.smul_filter.instNeBot {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} [f.NeBot] : (a • f).NeBot

theorem Filter.vadd_filter.instNeBot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} [f.NeBot] : (a +ᵥ f).NeBot

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₂

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₂

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

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

instance Filter.smulCommClass_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Filter γ)

instance Filter.vaddCommClass_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α β (Filter γ)

instance Filter.smulCommClass_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Filter β) (Filter γ)

instance Filter.vaddCommClass_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α (Filter β) (Filter γ)

instance Filter.smulCommClass_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Filter α) β (Filter γ)

instance Filter.vaddCommClass_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Filter α) β (Filter γ)

instance Filter.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Filter α) (Filter β) (Filter γ)

instance Filter.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Filter α) (Filter β) (Filter γ)

instance Filter.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Filter γ)

instance Filter.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α β (Filter γ)

instance Filter.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α (Filter β) (Filter γ)

instance Filter.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α (Filter β) (Filter γ)

instance Filter.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower (Filter α) (Filter β) (Filter γ)

instance Filter.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass (Filter α) (Filter β) (Filter γ)

instance Filter.isCentralScalar {α : Type u_2} {β : Type u_3} [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Filter β)

instance Filter.isCentralVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] : IsCentralVAdd α (Filter β)

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 := ⋯ }

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 := ⋯ }

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 := ⋯ }

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 := ⋯ }

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 := ⋯ }

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 := ⋯ }

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 β] [SMulWithZero α β] {f : Filter α} (hf : f.NeBot) : 0 ≤ f • 0

theorem Filter.NeBot.zero_smul_nonneg {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} (hg : g.NeBot) : 0 ≤ 0 • g

theorem Filter.zero_smul_filter_nonpos {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} : 0 • g ≤ 0

theorem Filter.zero_smul_filter {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} (hg : g.NeBot) : 0 • g = 0