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

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 }

@[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 α] : Filter.principal 0 = 0

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Filter.NeBot.le_one_iff {α : Type u_2} [One α] {f : Filter α} (h : Filter.NeBot f) : 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 : Filter β} {f : β → α} : Filter.Tendsto f a 0 ↔ ∀ᶠ (x : β) in a, f x = 0

@[simp]

theorem Filter.tendsto_one {α : Type u_2} {β : Type u_3} [One α] {a : Filter β} {f : β → α} : Filter.Tendsto f a 1 ↔ ∀ᶠ (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 α (Filter α)

pure as a ZeroHom.

Equations

• Filter.pureZeroHom = { toFun := pure, map_zero' := (_ : pure 0 = 0) }

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

pure as a OneHom.

Equations

• Filter.pureOneHom = { toFun := pure, map_one' := (_ : pure 1 = 1) }

@[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 β] [ZeroHomClass F α β] (φ : F) : Filter.map (↑φ) 0 = 0

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

Filter negation/inversion

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 }

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 }

@[simp]

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

@[simp]

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

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

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

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

theorem Filter.inv_le_inv {α : Type u_2} [Inv α] {f : Filter α} {g : Filter α} (hf : f ≤ g) : 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 : α} : (pure a)⁻¹ = pure a⁻¹

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem Filter.instInvolutiveNeg.proof_1 {α : Type u_1} [InvolutiveNeg α] (f : Filter α) : Filter.map Neg.neg (Filter.map Neg.neg f) = f

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

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

Equations

• Filter.instInvolutiveNeg = let src := Filter.instNeg; InvolutiveNeg.mk (_ : ∀ (f : Filter α), Filter.map Neg.neg (Filter.map Neg.neg f) = f)

def Filter.instInvolutiveInv {α : Type u_2} [InvolutiveInv α] : InvolutiveInv (Filter α)

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

Equations

• Filter.instInvolutiveInv = let src := Filter.instInv; InvolutiveInv.mk (_ : ∀ (f : Filter α), Filter.map Inv.inv (Filter.map Inv.inv f) = f)

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

Filter addition/multiplication

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.

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.

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Filter.mul_pure {α : Type u_2} [Mul α] {f : Filter α} {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 : Filter α} {g : Filter α} {h : Filter α} : h ≤ f + g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s + t ∈ h

@[simp]

theorem Filter.le_mul_iff {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} {h : Filter α} : h ≤ f * g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s * t ∈ h

theorem Filter.covariant_add.proof_1 {α : Type u_1} [Add α] : CovariantClass (Filter α) (Filter α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

instance Filter.covariant_add {α : Type u_2} [Add α] : CovariantClass (Filter α) (Filter α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_add = @Filter.covariant_add.proof_1

instance Filter.covariant_mul {α : Type u_2} [Mul α] : CovariantClass (Filter α) (Filter α) (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_mul = @Filter.covariant_mul.proof_1

theorem Filter.covariant_swap_add.proof_1 {α : Type u_1} [Add α] : CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

instance Filter.covariant_swap_add {α : Type u_2} [Add α] : CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_swap_add = @Filter.covariant_swap_add.proof_1

instance Filter.covariant_swap_mul {α : Type u_2} [Mul α] : CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_swap_mul = @Filter.covariant_swap_mul.proof_1

theorem Filter.map_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] {f₁ : Filter α} {f₂ : Filter α} [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₁ : Filter α} {f₂ : Filter α} [MulHomClass F α β] (m : F) : Filter.map (↑m) (f₁ * f₂) = Filter.map (↑m) f₁ * Filter.map (↑m) f₂

def Filter.pureAddHom {α : Type u_2} [Add α] : AddHom α (Filter α)

The singleton operation as an AddHom.

Equations

• Filter.pureAddHom = { toFun := pure, map_add' := (_ : ∀ (x x_1 : α), pure (x + x_1) = pure x + pure x_1) }

theorem Filter.pureAddHom.proof_1 {α : Type u_1} [Add α] : ∀ (x x_1 : α), pure (x + x_1) = pure x + pure x_1

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

pure operation as a MulHom.

Equations

• Filter.pureMulHom = { toFun := pure, map_mul' := (_ : ∀ (x x_1 : α), pure (x * x_1) = pure x * pure x_1) }

@[simp]

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

@[simp]

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

@[simp]

theorem Filter.pureAddHom_apply {α : Type u_2} [Add α] (a : α) : ↑Filter.pureAddHom a = pure 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 (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.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.

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Filter.div_pure {α : Type u_2} [Div α] {f : Filter α} {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₁ : Filter α} {f₂ : Filter α} {g₁ : Filter α} {g₂ : Filter α} : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ - g₁ ≤ f₂ - g₂

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

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

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

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

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

@[simp]

theorem Filter.le_sub_iff {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} {h : Filter α} : h ≤ f - g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s - t ∈ h

@[simp]

theorem Filter.le_div_iff {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} {h : Filter α} : h ≤ f / g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s / t ∈ h

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

Equations

• @Filter.covariant_sub = @Filter.covariant_sub.proof_1

theorem Filter.covariant_sub.proof_1 {α : Type u_1} [Sub α] : CovariantClass (Filter α) (Filter α) (fun x x_1 => x - x_1) fun x x_1 => x ≤ x_1

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

Equations

• @Filter.covariant_div = @Filter.covariant_div.proof_1

theorem Filter.covariant_swap_sub.proof_1 {α : Type u_1} [Sub α] : CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x - x_1) fun x x_1 => x ≤ x_1

instance Filter.covariant_swap_sub {α : Type u_2} [Sub α] : CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x - x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_swap_sub = @Filter.covariant_swap_sub.proof_1

instance Filter.covariant_swap_div {α : Type u_2} [Div α] : CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x / x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_swap_div = @Filter.covariant_swap_div.proof_1

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 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 n => zpowRec n s }

theorem Filter.addSemigroup.proof_1 {α : Type u_1} [AddSemigroup α] : ∀ (x x_1 x_2 : Filter α), 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} [AddSemigroup α] : AddSemigroup (Filter α)

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

Equations

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

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

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

Equations

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

theorem Filter.addCommSemigroup.proof_1 {α : Type u_1} [AddCommSemigroup α] (a : Filter α) (b : Filter α) (c : Filter α) : a + b + c = a + (b + c)

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

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

Equations

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

theorem Filter.addCommSemigroup.proof_2 {α : Type u_1} [AddCommSemigroup α] : ∀ (x x_1 : Filter α), 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} [CommSemigroup α] : CommSemigroup (Filter α)

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

Equations

• Filter.commSemigroup = let src := Filter.semigroup; CommSemigroup.mk (_ : ∀ (x x_1 : Filter α), Filter.map₂ (fun x x_2 => x * x_2) x x_1 = Filter.map₂ (fun x x_2 => x * x_2) x_1 x)

theorem Filter.addZeroClass.proof_1 {α : Type u_1} [AddZeroClass α] (l : Filter α) : Filter.map₂ (fun x x_1 => x + x_1) (pure 0) l = l

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

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

Equations

• Filter.addZeroClass = AddZeroClass.mk (_ : ∀ (l : Filter α), Filter.map₂ (fun x x_1 => x + x_1) (pure 0) l = l) (_ : ∀ (l : Filter α), Filter.map₂ (fun x x_1 => x + x_1) l (pure 0) = l)

theorem Filter.addZeroClass.proof_2 {α : Type u_1} [AddZeroClass α] (l : Filter α) : Filter.map₂ (fun x x_1 => x + x_1) l (pure 0) = l

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

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

Equations

• Filter.mulOneClass = MulOneClass.mk (_ : ∀ (l : Filter α), Filter.map₂ (fun x x_1 => x * x_1) (pure 1) l = l) (_ : ∀ (l : Filter α), Filter.map₂ (fun x x_1 => x * x_1) l (pure 1) = l)

theorem Filter.mapAddMonoidHom.proof_2 {F : Type u_3} {α : Type u_1} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (φ : F) : ∀ (x x_1 : Filter α), Filter.map (↑φ) (x + x_1) = Filter.map (↑φ) x + Filter.map (↑φ) x_1

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

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

Equations

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

theorem Filter.mapAddMonoidHom.proof_1 {F : Type u_3} {α : Type u_2} {β : Type u_1} [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (φ : F) : Filter.map (↑φ) 0 = 0

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

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

Equations

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

theorem Filter.comap_add_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [AddHomClass F α β] (m : F) {f : Filter β} {g : Filter β} : 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} [AddZeroClass α] [AddZeroClass β] [AddHomClass F α β] (m : F) {f : Filter β} {g : Filter β} : ∀ (x : Set α) (motive : x ∈ Filter.comap (↑m) (f + g) → Prop) (x_1 : x ∈ Filter.comap (↑m) (f + g)), (∀ (w t₁ t₂ : Set β) (ht₁ : t₁ ∈ f) (ht₂ : t₂ ∈ g) (t₁t₂ : t₁ + t₂ ⊆ w) (mt : ↑m ⁻¹' w ⊆ x), motive (_ : ∃ t, t ∈ f + g ∧ ↑m ⁻¹' t ⊆ x)) → motive x_1

Equations

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

theorem Filter.comap_mul_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [MulHomClass F α β] (m : F) {f : Filter β} {g : Filter β} : 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} [AddZeroClass α] [AddZeroClass β] [AddHomClass F α β] (m : F) {f₁ : Filter α} {g₁ : Filter α} {f₂ : Filter β} {g₂ : Filter β} : 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} [MulOneClass α] [MulOneClass β] [MulHomClass F α β] (m : F) {f₁ : Filter α} {g₁ : Filter α} {f₂ : Filter β} {g₂ : Filter β} : 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} [AddZeroClass α] (x : α) (y : α) : AddHom.toFun Filter.pureAddHom (x + y) = AddHom.toFun Filter.pureAddHom x + AddHom.toFun Filter.pureAddHom y

theorem Filter.pureAddMonoidHom.proof_1 {α : Type u_1} [AddZeroClass α] : ZeroHom.toFun Filter.pureZeroHom 0 = 0

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

pure as an AddMonoidHom.

Equations

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

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

pure as a MonoidHom.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Filter.addMonoid.proof_2 {α : Type u_1} [AddMonoid α] (a : Filter α) : 0 + a = a

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

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

Equations

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

theorem Filter.addMonoid.proof_4 {α : Type u_1} [AddMonoid α] : ∀ (x : Filter α), nsmulRec 0 x = nsmulRec 0 x

theorem Filter.addMonoid.proof_1 {α : Type u_1} [AddMonoid α] (a : Filter α) (b : Filter α) (c : Filter α) : a + b + c = a + (b + c)

theorem Filter.addMonoid.proof_5 {α : Type u_1} [AddMonoid α] : ∀ (n : ℕ) (x : Filter α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem Filter.addMonoid.proof_3 {α : Type u_1} [AddMonoid α] (a : Filter α) : a + 0 = a

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

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

Equations

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

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

abbrev Filter.nsmul_mem_nsmul.match_1 (motive : ℕ → Prop) : (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive (Nat.succ n)) → motive x

Equations

• Filter.nsmul_mem_nsmul.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n

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

@[simp]

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

@[simp]

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

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

theorem Filter.mul_top_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 = ⊤

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

@[simp]

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

@[simp]

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

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

abbrev Filter.nsmul_top.match_1 (motive : ℕ → Prop) : (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → motive (Nat.succ (Nat.succ n))) → motive x

Equations

• Filter.nsmul_top.match_1 motive x h_1 h_2 h_3 = Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n

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

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

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

theorem Filter.addCommMonoid.proof_2 {α : Type u_1} [AddCommMonoid α] (a : Filter α) : a + 0 = a

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

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

Equations

• Filter.addCommMonoid = let src := Filter.addZeroClass; let src_1 := Filter.addCommSemigroup; AddCommMonoid.mk (_ : ∀ (a b : Filter α), a + b = b + a)

theorem Filter.addCommMonoid.proof_3 {α : Type u_1} [AddCommMonoid α] : ∀ (x : Filter α), nsmulRec 0 x = nsmulRec 0 x

theorem Filter.addCommMonoid.proof_1 {α : Type u_1} [AddCommMonoid α] (a : Filter α) : 0 + a = a

theorem Filter.addCommMonoid.proof_5 {α : Type u_1} [AddCommMonoid α] (a : Filter α) (b : Filter α) : a + b = b + a

theorem Filter.addCommMonoid.proof_4 {α : Type u_1} [AddCommMonoid α] : ∀ (n : ℕ) (x : Filter α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

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

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

Equations

• Filter.commMonoid = let src := Filter.mulOneClass; let src_1 := Filter.commSemigroup; CommMonoid.mk (_ : ∀ (a b : Filter α), a * b = b * a)

theorem Filter.add_eq_zero_iff {α : Type u_2} [SubtractionMonoid α] {f : Filter α} {g : Filter α} : f + g = 0 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a + b = 0

theorem Filter.mul_eq_one_iff {α : Type u_2} [DivisionMonoid α] {f : Filter α} {g : Filter α} : f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

theorem Filter.subtractionMonoid.proof_2 {α : Type u_1} [SubtractionMonoid α] (a : Filter α) : a + 0 = a

theorem Filter.subtractionMonoid.proof_12 {α : Type u_1} [SubtractionMonoid α] (s : Filter α) (t : Filter α) (h : s + t = 0) : -s = t

theorem Filter.subtractionMonoid.proof_9 {α : Type u_1} [SubtractionMonoid α] : ∀ (n : ℕ) (a : Filter α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

theorem Filter.subtractionMonoid.proof_10 {α : Type u_1} [SubtractionMonoid α] (x : Filter α) : - -x = x

theorem Filter.subtractionMonoid.proof_7 {α : Type u_1} [SubtractionMonoid α] : ∀ (a : Filter α), zsmulRec 0 a = zsmulRec 0 a

theorem Filter.subtractionMonoid.proof_5 {α : Type u_1} [SubtractionMonoid α] (f : Filter α) (g : Filter α) : 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_6 {α : Type u_1} [SubtractionMonoid α] (a : Filter α) (b : Filter α) (c : Filter α) : a + b + c = a + (b + c)

theorem Filter.subtractionMonoid.proof_11 {α : Type u_1} [SubtractionMonoid α] (s : Filter α) (t : Filter α) : 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)

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.subtractionMonoid.proof_4 {α : Type u_1} [SubtractionMonoid α] (n : ℕ) (x : Filter α) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

theorem Filter.subtractionMonoid.proof_8 {α : Type u_1} [SubtractionMonoid α] : ∀ (n : ℕ) (a : Filter α), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a

theorem Filter.subtractionMonoid.proof_3 {α : Type u_1} [SubtractionMonoid α] (x : Filter α) : AddMonoid.nsmul 0 x = 0

theorem Filter.subtractionMonoid.proof_1 {α : Type u_1} [SubtractionMonoid α] (a : Filter α) : 0 + a = a

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.

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

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

theorem Filter.subtractionCommMonoid.proof_2 {α : Type u_1} [SubtractionCommMonoid α] (a : Filter α) (b : Filter α) : -(a + b) = -b + -a

theorem Filter.subtractionCommMonoid.proof_4 {α : Type u_1} [SubtractionCommMonoid α] (a : Filter α) (b : Filter α) : a + b = b + a

theorem Filter.subtractionCommMonoid.proof_3 {α : Type u_1} [SubtractionCommMonoid α] (a : Filter α) (b : Filter α) : a + b = 0 → -a = b

theorem Filter.subtractionCommMonoid.proof_1 {α : Type u_1} [SubtractionCommMonoid α] (x : Filter α) : - -x = x

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

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

Equations

• Filter.subtractionCommMonoid = let src := Filter.subtractionMonoid; let src_1 := Filter.addCommSemigroup; SubtractionCommMonoid.mk (_ : ∀ (a b : Filter α), a + b = b + a)

def Filter.divisionCommMonoid {α : Type u_2} [DivisionCommMonoid α] : DivisionCommMonoid (Filter α)

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

Equations

• Filter.divisionCommMonoid = let src := Filter.divisionMonoid; let src_1 := Filter.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : Filter α), a * b = b * a)

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

Filter α has distributive negation if α has.

Equations

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

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 : Filter α} {g : Filter α} {h : Filter α} : f * (g + h) ≤ f * g + f * h

theorem Filter.add_mul_subset {α : Type u_2} [Distrib α] {f : Filter α} {g : Filter α} {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 : Filter.NeBot f) : 0 ≤ f * 0

theorem Filter.NeBot.zero_mul_nonneg {α : Type u_2} [MulZeroClass α] {g : Filter α} (hg : Filter.NeBot g) : 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} [AddGroup α] {f : Filter α} {g : Filter α} : 0 ≤ f - g ↔ ¬Disjoint f g

@[simp]

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

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

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

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

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

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

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

@[simp]

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

theorem Filter.map_neg' {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [AddMonoidHomClass F α β] (m : F) {f : Filter α} : Filter.map (↑m) (-f) = -Filter.map (↑m) f

theorem Filter.map_inv' {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (m : F) {f : Filter α} : Filter.map (↑m) f⁻¹ = (Filter.map (↑m) f)⁻¹

theorem Filter.Tendsto.neg_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [AddMonoidHomClass F α β] (m : F) {f₁ : Filter α} {f₂ : Filter β} : 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} [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (m : F) {f₁ : Filter α} {f₂ : Filter β} : Filter.Tendsto (↑m) f₁ f₂ → Filter.Tendsto (↑m) f₁⁻¹ f₂⁻¹

theorem Filter.map_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [AddMonoidHomClass F α β] (m : F) {f : Filter α} {g : Filter α} : 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} [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (m : F) {f : Filter α} {g : Filter α} : 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} [AddGroup α] [SubtractionMonoid β] [AddMonoidHomClass F α β] (m : F) {f₁ : Filter α} {g₁ : Filter α} {f₂ : Filter β} {g₂ : Filter β} (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} [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (m : F) {f₁ : Filter α} {g₁ : Filter α} {f₂ : Filter β} {g₂ : Filter β} (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} [GroupWithZero α] {f : Filter α} (hf : Filter.NeBot f) : 0 ≤ f / 0

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

Scalar addition/multiplication of filters

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.

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.

@[simp]

theorem Filter.map₂_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} : 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 : Filter α} {g : Filter β} : 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 : Filter α} {g : Filter β} {t : Set β} : t ∈ f +ᵥ g ↔ ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ +ᵥ t₂ ⊆ t

theorem Filter.mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} {t : Set β} : t ∈ f • g ↔ ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ • t₂ ⊆ t

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} : f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Filter.smul_pure {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {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₁ : Filter α} {f₂ : Filter α} {g₁ : Filter β} {g₂ : Filter β} : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ +ᵥ g₁ ≤ f₂ +ᵥ g₂

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

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

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

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

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

@[simp]

theorem Filter.le_vadd_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} {h : Filter β} : h ≤ f +ᵥ g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s +ᵥ t ∈ h

@[simp]

theorem Filter.le_smul_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} {h : Filter β} : h ≤ f • g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s • t ∈ h

instance Filter.covariant_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] : CovariantClass (Filter α) (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_vadd = @Filter.covariant_vadd.proof_1

theorem Filter.covariant_vadd.proof_1 {α : Type u_1} {β : Type u_2} [VAdd α β] : CovariantClass (Filter α) (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1

instance Filter.covariant_smul {α : Type u_2} {β : Type u_3} [SMul α β] : CovariantClass (Filter α) (Filter β) (fun x x_1 => x • x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_smul = @Filter.covariant_smul.proof_1

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 : Filter β} {g : Filter β} : 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 : Filter β} {g : Filter β} {s : Set α} : s ∈ f -ᵥ g ↔ ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ -ᵥ t₂ ⊆ s

theorem Filter.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} {s : Set β} {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 : Filter β} {g : Filter β} : f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem Filter.le_vsub_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} {h : Filter α} : h ≤ f -ᵥ g ↔ ∀ ⦃s : Set β⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s -ᵥ t ∈ h

Translation/scaling of filters

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 x_1 => x +ᵥ x_1) a) }

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 x_1 => x • x_1) a) }

@[simp]

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

@[simp]

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

theorem Filter.mem_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {s : Set β} {a : α} : s ∈ a +ᵥ f ↔ (fun x x_1 => x +ᵥ x_1) a ⁻¹' s ∈ f

theorem Filter.mem_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {s : Set β} {a : α} : s ∈ a • f ↔ (fun x x_1 => x • x_1) a ⁻¹' s ∈ 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

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

@[simp]

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

@[simp]

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

@[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_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} : a • f = ⊥ ↔ f = ⊥

@[simp]

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

@[simp]

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

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

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

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

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

theorem Filter.vadd_filter_le_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ : Filter β} {f₂ : Filter β} {a : α} (hf : f₁ ≤ f₂) : a +ᵥ f₁ ≤ a +ᵥ f₂

theorem Filter.smul_filter_le_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ : Filter β} {f₂ : Filter β} {a : α} (hf : f₁ ≤ f₂) : a • f₁ ≤ a • f₂

theorem Filter.covariant_vadd_filter.proof_1 {α : Type u_1} {β : Type u_2} [VAdd α β] : CovariantClass α (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1

instance Filter.covariant_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] : CovariantClass α (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_vadd_filter = @Filter.covariant_vadd_filter.proof_1

instance Filter.covariant_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] : CovariantClass α (Filter β) (fun x x_1 => x • x_1) fun x x_1 => x ≤ x_1

Equations

• @Filter.covariant_smul_filter = @Filter.covariant_smul_filter.proof_1

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

Equations

• @Filter.vaddCommClass_filter = @Filter.vaddCommClass_filter.proof_1

theorem Filter.vaddCommClass_filter.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α β (Filter γ)

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

Equations

• @Filter.smulCommClass_filter = @Filter.smulCommClass_filter.proof_1

theorem Filter.vaddCommClass_filter'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α (Filter β) (Filter γ)

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

Equations

• @Filter.vaddCommClass_filter' = @Filter.vaddCommClass_filter'.proof_1

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

Equations

• @Filter.smulCommClass_filter' = @Filter.smulCommClass_filter'.proof_1

theorem Filter.vaddCommClass_filter''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Filter α) β (Filter γ)

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

Equations

• @Filter.vaddCommClass_filter'' = @Filter.vaddCommClass_filter''.proof_1

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

Equations

• @Filter.smulCommClass_filter'' = @Filter.smulCommClass_filter''.proof_1

theorem Filter.vaddCommClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Filter α) (Filter β) (Filter γ)

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

Equations

• @Filter.vaddCommClass = @Filter.vaddCommClass.proof_1

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

Equations

• @Filter.smulCommClass = @Filter.smulCommClass.proof_1

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

Equations

• @Filter.vaddAssocClass = @Filter.vaddAssocClass.proof_1

theorem Filter.vaddAssocClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α β (Filter γ)

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

Equations

• @Filter.isScalarTower = @Filter.isScalarTower.proof_1

theorem Filter.vaddAssocClass'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α (Filter β) (Filter γ)

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

Equations

• @Filter.vaddAssocClass' = @Filter.vaddAssocClass'.proof_1

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

Equations

• @Filter.isScalarTower' = @Filter.isScalarTower'.proof_1

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

Equations

• @Filter.vaddAssocClass'' = @Filter.vaddAssocClass''.proof_1

theorem Filter.vaddAssocClass''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass (Filter α) (Filter β) (Filter γ)

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

Equations

• @Filter.isScalarTower'' = @Filter.isScalarTower''.proof_1

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

Equations

• @Filter.isCentralVAdd = @Filter.isCentralVAdd.proof_1

theorem Filter.isCentralVAdd.proof_1 {α : Type u_1} {β : Type u_2} [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] : IsCentralVAdd α (Filter β)

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

Equations

• @Filter.isCentralScalar = @Filter.isCentralScalar.proof_1

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

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

theorem Filter.addAction.proof_1 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] (f : Filter β) : Filter.map₂ (fun x x_1 => x +ᵥ x_1) (pure 0) f = f

theorem Filter.addAction.proof_2 {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddAction α β] (f : Filter α) (g : Filter α) (h : Filter β) : 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)

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

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

theorem Filter.addActionFilter.proof_1 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] (f : Filter β) : Filter.map (fun x => 0 +ᵥ x) f = f

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

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

theorem Filter.addActionFilter.proof_2 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] (a : α) (b : α) (f : Filter β) : Filter.map (fun b => a + b +ᵥ b) f = Filter.map (fun b => a +ᵥ b) (Filter.map (fun b => b +ᵥ b) f)

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

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

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

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

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

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

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 : Filter.NeBot f) : 0 ≤ f • 0

theorem Filter.NeBot.zero_smul_nonneg {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} (hg : Filter.NeBot g) : 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 : Filter.NeBot g) : 0 • g = 0