Documentation

Mathlib.Order.Filter.Pointwise

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∈ f and t ∈ g∈ g.
f * g (Filter.instMul): Multiplication, filter generated by all s * t where s ∈ f∈ f and t ∈ g∈ g.
-f (Filter.instNeg): Negation, filter of all -s where s ∈ f∈ f.
f⁻¹⁻¹ (Filter.instInv): Inversion, filter of all s⁻¹⁻¹ where s ∈ f∈ f.
f - g (Filter.instSub): Subtraction, filter generated by all s - t where s ∈ f∈ f and t ∈ g∈ g.
f / g (Filter.instDiv): Division, filter generated by all s / t where s ∈ f∈ f and t ∈ g∈ g.
f +ᵥ g (Filter.instVAdd): Scalar addition, filter generated by all s +ᵥ t where s ∈ f∈ f and t ∈ g∈ g.
f -ᵥ g (Filter.instVSub): Scalar subtraction, filter generated by all s -ᵥ t where s ∈ f∈ f and t ∈ g∈ g.
f • g (Filter.instSMul): Scalar multiplication, filter generated by all s • t where s ∈ f∈ f and t ∈ g∈ g.
a +ᵥ f (Filter.instVAddFilter): Translation, filter of all a +ᵥ s where s ∈ f∈ f.
a • f (Filter.instSMulFilter): Scaling, filter of all a • s where s ∈ f∈ 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_1} [inst : 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_1} [inst : 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_1} [inst : Zero α] {s : Set α} :

s ∈ 0 ↔ 0 ∈ s

@[simp]

theorem Filter.mem_one {α : Type u_1} [inst : One α] {s : Set α} :

s ∈ 1 ↔ 1 ∈ s

theorem Filter.zero_mem_zero {α : Type u_1} [inst : Zero α] :

0 ∈ 0

theorem Filter.one_mem_one {α : Type u_1} [inst : One α] :

1 ∈ 1

@[simp]

theorem Filter.pure_zero {α : Type u_1} [inst : Zero α] :

pure 0 = 0

@[simp]

theorem Filter.pure_one {α : Type u_1} [inst : One α] :

pure 1 = 1

@[simp]

theorem Filter.principal_zero {α : Type u_1} [inst : Zero α] :

Filter.principal 0 = 0

@[simp]

theorem Filter.principal_one {α : Type u_1} [inst : One α] :

Filter.principal 1 = 1

theorem Filter.zero_neBot {α : Type u_1} [inst : Zero α] :

theorem Filter.one_neBot {α : Type u_1} [inst : One α] :

@[simp]

theorem Filter.map_zero' {α : Type u_2} {β : Type u_1} [inst : Zero α] (f : α → β) :

Filter.map f 0 = pure (f 0)

@[simp]

theorem Filter.map_one' {α : Type u_2} {β : Type u_1} [inst : One α] (f : α → β) :

Filter.map f 1 = pure (f 1)

@[simp]

theorem Filter.nonpos_iff {α : Type u_1} [inst : Zero α] {f : Filter α} :

f ≤ 0 ↔ 0 ∈ f

@[simp]

theorem Filter.le_one_iff {α : Type u_1} [inst : One α] {f : Filter α} :

f ≤ 1 ↔ 1 ∈ f

theorem Filter.NeBot.nonpos_iff {α : Type u_1} [inst : Zero α] {f : Filter α} (h : Filter.NeBot f) :

f ≤ 0 ↔ f = 0

theorem Filter.NeBot.le_one_iff {α : Type u_1} [inst : One α] {f : Filter α} (h : Filter.NeBot f) :

f ≤ 1 ↔ f = 1

@[simp]

theorem Filter.eventually_zero {α : Type u_1} [inst : Zero α] {p : α → Prop} :

Filter.Eventually (fun x => p x) 0 ↔ p 0

@[simp]

theorem Filter.eventually_one {α : Type u_1} [inst : One α] {p : α → Prop} :

Filter.Eventually (fun x => p x) 1 ↔ p 1

@[simp]

theorem Filter.tendsto_zero {α : Type u_2} {β : Type u_1} [inst : Zero α] {a : Filter β} {f : β → α} :

Filter.Tendsto f a 0 ↔ Filter.Eventually (fun x => f x = 0) a

@[simp]

theorem Filter.tendsto_one {α : Type u_2} {β : Type u_1} [inst : One α] {a : Filter β} {f : β → α} :

Filter.Tendsto f a 1 ↔ Filter.Eventually (fun x => f x = 1) a

@[simp]

theorem Filter.zero_sum_zero {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] :

Filter.prod 0 0 = 0

@[simp]

theorem Filter.one_prod_one {α : Type u_2} {β : Type u_1} [inst : One α] [inst : One β] :

Filter.prod 1 1 = 1

def Filter.pureZeroHom {α : Type u_1} [inst : Zero α] :

ZeroHom α (Filter α)

pure as a zero_hom.

Equations

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

def Filter.pureOneHom {α : Type u_1} [inst : One α] :

OneHom α (Filter α)

pure as a one_hom.

Equations

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

@[simp]

theorem Filter.coe_pureZeroHom {α : Type u_1} [inst : Zero α] :

↑Filter.pureZeroHom = pure

@[simp]

theorem Filter.coe_pureOneHom {α : Type u_1} [inst : One α] :

↑Filter.pureOneHom = pure

@[simp]

theorem Filter.pureZeroHom_apply {α : Type u_1} [inst : Zero α] (a : α) :

↑Filter.pureZeroHom a = pure a

@[simp]

theorem Filter.pureOneHom_apply {α : Type u_1} [inst : One α] (a : α) :

↑Filter.pureOneHom a = pure a

theorem Filter.map_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst : Zero β] [inst : ZeroHomClass F α β] (φ : F) :

Filter.map (↑φ) 0 = 0

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

Filter.map (↑φ) 1 = 1

Filter negation/inversion #

instance Filter.instNeg {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : Neg α] {f : Filter α} :

Filter.map Neg.neg f = -f

@[simp]

theorem Filter.map_inv {α : Type u_1} [inst : Inv α] {f : Filter α} :

Filter.map Inv.inv f = f⁻¹

theorem Filter.mem_neg {α : Type u_1} [inst : Neg α] {f : Filter α} {s : Set α} :

s ∈ -f ↔ Neg.neg ⁻¹' s ∈ f

theorem Filter.mem_inv {α : Type u_1} [inst : Inv α] {f : Filter α} {s : Set α} :

s ∈ f⁻¹ ↔ Inv.inv ⁻¹' s ∈ f

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

theorem Filter.inv_le_inv {α : Type u_1} [inst : Inv α] {f : Filter α} {g : Filter α} (hf : f ≤ g) :

f⁻¹ ≤ g⁻¹

@[simp]

theorem Filter.neg_pure {α : Type u_1} [inst : Neg α] {a : α} :

-pure a = pure (-a)

@[simp]

theorem Filter.inv_pure {α : Type u_1} [inst : Inv α] {a : α} :

(pure a)⁻¹ = pure a⁻¹

@[simp]

theorem Filter.neg_eq_bot_iff {α : Type u_1} [inst : Neg α] {f : Filter α} :

-f = ⊥ ↔ f = ⊥

@[simp]

theorem Filter.inv_eq_bot_iff {α : Type u_1} [inst : Inv α] {f : Filter α} :

f⁻¹ = ⊥ ↔ f = ⊥

@[simp]

theorem Filter.neBot_neg_iff {α : Type u_1} [inst : Neg α] {f : Filter α} :

Filter.NeBot (-f) ↔ Filter.NeBot f

@[simp]

theorem Filter.neBot_inv_iff {α : Type u_1} [inst : Inv α] {f : Filter α} :

Filter.NeBot f⁻¹ ↔ Filter.NeBot f

theorem Filter.NeBot.neg {α : Type u_1} [inst : Neg α] {f : Filter α} :

Filter.NeBot f → Filter.NeBot (-f)

theorem Filter.NeBot.inv {α : Type u_1} [inst : Inv α] {f : Filter α} :

Filter.NeBot f → Filter.NeBot f⁻¹

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

theorem Filter.inv_mem_inv {α : Type u_1} [inst : InvolutiveInv α] {f : Filter α} {s : Set α} (hs : s ∈ f) :

s⁻¹ ∈ f⁻¹

def Filter.instInvolutiveNeg.proof_1 {α : Type u_1} [inst : InvolutiveNeg α] (f : Filter α) :

Filter.map Neg.neg (Filter.map Neg.neg f) = f

Equations

(_ : Filter.map Neg.neg (Filter.map Neg.neg f) = f) = (_ : Filter.map Neg.neg (Filter.map Neg.neg f) = f)

def Filter.instInvolutiveNeg {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : InvolutiveNeg α] {f : Filter α} {g : Filter α} :

-f ≤ -g ↔ f ≤ g

@[simp]

theorem Filter.inv_le_inv_iff {α : Type u_1} [inst : InvolutiveInv α] {f : Filter α} {g : Filter α} :

f⁻¹ ≤ g⁻¹ ↔ f ≤ g

theorem Filter.neg_le_iff_le_neg {α : Type u_1} [inst : InvolutiveNeg α] {f : Filter α} {g : Filter α} :

-f ≤ g ↔ f ≤ -g

theorem Filter.inv_le_iff_le_inv {α : Type u_1} [inst : InvolutiveInv α] {f : Filter α} {g : Filter α} :

f⁻¹ ≤ g ↔ f ≤ g⁻¹

@[simp]

theorem Filter.neg_le_self {α : Type u_1} [inst : InvolutiveNeg α] {f : Filter α} :

-f ≤ f ↔ -f = f

@[simp]

theorem Filter.inv_le_self {α : Type u_1} [inst : InvolutiveInv α] {f : Filter α} :

f⁻¹ ≤ f ↔ f⁻¹ = f

Filter addition/multiplication #

def Filter.instAdd {α : Type u_1} [inst : Add α] :

Add (Filter α)

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

Equations

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

def Filter.instAdd.proof_2 {α : Type u_1} [inst : Add α] (f : Filter α) (g : Filter α) :

∀ {x y : Set α}, x ∈ (Filter.map₂ (fun x x_1 => x + x_1) f g).sets → y ∈ (Filter.map₂ (fun x x_1 => x + x_1) f g).sets → x ∩ y ∈ (Filter.map₂ (fun x x_1 => x + x_1) f g).sets

Equations

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

def Filter.instAdd.proof_1 {α : Type u_1} [inst : Add α] (f : Filter α) (g : Filter α) :

∀ {x y : Set α}, x ∈ (Filter.map₂ (fun x x_1 => x + x_1) f g).sets → x ⊆ y → y ∈ (Filter.map₂ (fun x x_1 => x + x_1) f g).sets

Equations

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

def Filter.instMul {α : Type u_1} [inst : Mul α] :

Mul (Filter α)

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

Equations

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

@[simp]

theorem Filter.map₂_add {α : Type u_1} [inst : 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_1} [inst : Mul α] {f : Filter α} {g : Filter α} :

Filter.map₂ (fun x x_1 => x * x_1) f g = f * g

theorem Filter.mem_add {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : Add α] {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} :

s ∈ f → t ∈ g → s + t ∈ f + g

theorem Filter.mul_mem_mul {α : Type u_1} [inst : Mul α] {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} :

s ∈ f → t ∈ g → s * t ∈ f * g

@[simp]

theorem Filter.bot_add {α : Type u_1} [inst : Add α] {g : Filter α} :

@[simp]

theorem Filter.bot_mul {α : Type u_1} [inst : Mul α] {g : Filter α} :

@[simp]

theorem Filter.add_bot {α : Type u_1} [inst : Add α] {f : Filter α} :

@[simp]

theorem Filter.mul_bot {α : Type u_1} [inst : Mul α] {f : Filter α} :

@[simp]

theorem Filter.add_eq_bot_iff {α : Type u_1} [inst : Add α] {f : Filter α} {g : Filter α} :

f + g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.mul_eq_bot_iff {α : Type u_1} [inst : Mul α] {f : Filter α} {g : Filter α} :

f * g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.add_neBot_iff {α : Type u_1} [inst : Add α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f + g) ↔ Filter.NeBot f ∧ Filter.NeBot g

@[simp]

theorem Filter.mul_neBot_iff {α : Type u_1} [inst : Mul α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f * g) ↔ Filter.NeBot f ∧ Filter.NeBot g

theorem Filter.NeBot.add {α : Type u_1} [inst : Add α] {f : Filter α} {g : Filter α} :

Filter.NeBot f → Filter.NeBot g → Filter.NeBot (f + g)

theorem Filter.NeBot.mul {α : Type u_1} [inst : Mul α] {f : Filter α} {g : Filter α} :

Filter.NeBot f → Filter.NeBot g → Filter.NeBot (f * g)

theorem Filter.NeBot.of_add_left {α : Type u_1} [inst : Add α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f + g) → Filter.NeBot f

theorem Filter.NeBot.of_mul_left {α : Type u_1} [inst : Mul α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f * g) → Filter.NeBot f

theorem Filter.NeBot.of_add_right {α : Type u_1} [inst : Add α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f + g) → Filter.NeBot g

theorem Filter.NeBot.of_mul_right {α : Type u_1} [inst : Mul α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f * g) → Filter.NeBot g

@[simp]

theorem Filter.pure_add {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : Add α] {f : Filter α} {b : α} :

f + pure b = Filter.map (fun x => x + b) f

@[simp]

theorem Filter.mul_pure {α : Type u_1} [inst : Mul α] {f : Filter α} {b : α} :

f * pure b = Filter.map (fun x => x * b) f

theorem Filter.pure_add_pure {α : Type u_1} [inst : Add α] {a : α} {b : α} :

pure a + pure b = pure (a + b)

theorem Filter.pure_mul_pure {α : Type u_1} [inst : Mul α] {a : α} {b : α} :

pure a * pure b = pure (a * b)

@[simp]

theorem Filter.le_add_iff {α : Type u_1} [inst : 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_1} [inst : Mul α] {f : Filter α} {g : Filter α} {h : Filter α} :

h ≤ f * g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s * t ∈ h

instance Filter.covariant_add {α : Type u_1} [inst : 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

def Filter.covariant_add.proof_1 {α : Type u_1} [inst : Add α] :

CovariantClass (Filter α) (Filter α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

(_ : CovariantClass (Filter α) (Filter α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass (Filter α) (Filter α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

instance Filter.covariant_mul {α : Type u_1} [inst : 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

instance Filter.covariant_swap_add {α : Type u_1} [inst : 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

def Filter.covariant_swap_add.proof_1 {α : Type u_1} [inst : Add α] :

CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

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

instance Filter.covariant_swap_mul {α : Type u_1} [inst : 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} [inst : Add α] [inst : Add β] {f₁ : Filter α} {f₂ : Filter α} [inst : 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} [inst : Mul α] [inst : Mul β] {f₁ : Filter α} {f₂ : Filter α} [inst : MulHomClass F α β] (m : F) :

Filter.map (↑m) (f₁ * f₂) = Filter.map (↑m) f₁ * Filter.map (↑m) f₂

def Filter.pureAddHom.proof_1 {α : Type u_1} [inst : Add α] :

∀ (x x_1 : α), pure (x + x_1) = pure x + pure x_1

Equations

(_ : pure (x + x) = pure x + pure x) = (_ : pure (x + x) = pure x + pure x)

def Filter.pureAddHom {α : Type u_1} [inst : 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) }

def Filter.pureMulHom {α : Type u_1} [inst : 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_1} [inst : Add α] :

↑Filter.pureAddHom = pure

@[simp]

theorem Filter.coe_pureMulHom {α : Type u_1} [inst : Mul α] :

↑Filter.pureMulHom = pure

@[simp]

theorem Filter.pureAddHom_apply {α : Type u_1} [inst : Add α] (a : α) :

↑Filter.pureAddHom a = pure a

@[simp]

theorem Filter.pureMulHom_apply {α : Type u_1} [inst : Mul α] (a : α) :

↑Filter.pureMulHom a = pure a

Filter subtraction/division #

def Filter.instSub {α : Type u_1} [inst : Sub α] :

Sub (Filter α)

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

Equations

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

def Filter.instSub.proof_2 {α : Type u_1} [inst : Sub α] (f : Filter α) (g : Filter α) :

∀ {x y : Set α}, x ∈ (Filter.map₂ (fun x x_1 => x - x_1) f g).sets → y ∈ (Filter.map₂ (fun x x_1 => x - x_1) f g).sets → x ∩ y ∈ (Filter.map₂ (fun x x_1 => x - x_1) f g).sets

Equations

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

def Filter.instSub.proof_1 {α : Type u_1} [inst : Sub α] (f : Filter α) (g : Filter α) :

∀ {x y : Set α}, x ∈ (Filter.map₂ (fun x x_1 => x - x_1) f g).sets → x ⊆ y → y ∈ (Filter.map₂ (fun x x_1 => x - x_1) f g).sets

Equations

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

def Filter.instDiv {α : Type u_1} [inst : Div α] :

Div (Filter α)

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

Equations

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

@[simp]

theorem Filter.map₂_sub {α : Type u_1} [inst : 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_1} [inst : Div α] {f : Filter α} {g : Filter α} :

Filter.map₂ (fun x x_1 => x / x_1) f g = f / g

theorem Filter.mem_sub {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : Sub α] {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} :

s ∈ f → t ∈ g → s - t ∈ f - g

theorem Filter.div_mem_div {α : Type u_1} [inst : Div α] {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} :

s ∈ f → t ∈ g → s / t ∈ f / g

@[simp]

theorem Filter.bot_sub {α : Type u_1} [inst : Sub α] {g : Filter α} :

@[simp]

theorem Filter.bot_div {α : Type u_1} [inst : Div α] {g : Filter α} :

@[simp]

theorem Filter.sub_bot {α : Type u_1} [inst : Sub α] {f : Filter α} :

@[simp]

theorem Filter.div_bot {α : Type u_1} [inst : Div α] {f : Filter α} :

@[simp]

theorem Filter.sub_eq_bot_iff {α : Type u_1} [inst : Sub α] {f : Filter α} {g : Filter α} :

f - g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.div_eq_bot_iff {α : Type u_1} [inst : Div α] {f : Filter α} {g : Filter α} :

f / g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.sub_neBot_iff {α : Type u_1} [inst : Sub α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f - g) ↔ Filter.NeBot f ∧ Filter.NeBot g

@[simp]

theorem Filter.div_neBot_iff {α : Type u_1} [inst : Div α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f / g) ↔ Filter.NeBot f ∧ Filter.NeBot g

theorem Filter.NeBot.sub {α : Type u_1} [inst : Sub α] {f : Filter α} {g : Filter α} :

Filter.NeBot f → Filter.NeBot g → Filter.NeBot (f - g)

theorem Filter.NeBot.div {α : Type u_1} [inst : Div α] {f : Filter α} {g : Filter α} :

Filter.NeBot f → Filter.NeBot g → Filter.NeBot (f / g)

theorem Filter.NeBot.of_sub_left {α : Type u_1} [inst : Sub α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f - g) → Filter.NeBot f

theorem Filter.NeBot.of_div_left {α : Type u_1} [inst : Div α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f / g) → Filter.NeBot f

theorem Filter.NeBot.of_sub_right {α : Type u_1} [inst : Sub α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f - g) → Filter.NeBot g

theorem Filter.NeBot.of_div_right {α : Type u_1} [inst : Div α] {f : Filter α} {g : Filter α} :

Filter.NeBot (f / g) → Filter.NeBot g

@[simp]

theorem Filter.pure_sub {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : Sub α] {f : Filter α} {b : α} :

f - pure b = Filter.map (fun x => x - b) f

@[simp]

theorem Filter.div_pure {α : Type u_1} [inst : Div α] {f : Filter α} {b : α} :

f / pure b = Filter.map (fun x => x / b) f

theorem Filter.pure_sub_pure {α : Type u_1} [inst : Sub α] {a : α} {b : α} :

pure a - pure b = pure (a - b)

theorem Filter.pure_div_pure {α : Type u_1} [inst : Div α] {a : α} {b : α} :

pure a / pure b = pure (a / b)

theorem Filter.sub_le_sub {α : Type u_1} [inst : Sub α] {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter α} {g₂ : Filter α} :

f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ - g₁ ≤ f₂ - g₂

theorem Filter.div_le_div {α : Type u_1} [inst : 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_1} [inst : Sub α] {f : Filter α} {g₁ : Filter α} {g₂ : Filter α} :

g₁ ≤ g₂ → f - g₁ ≤ f - g₂

theorem Filter.div_le_div_left {α : Type u_1} [inst : Div α] {f : Filter α} {g₁ : Filter α} {g₂ : Filter α} :

g₁ ≤ g₂ → f / g₁ ≤ f / g₂

theorem Filter.sub_le_sub_right {α : Type u_1} [inst : Sub α] {f₁ : Filter α} {f₂ : Filter α} {g : Filter α} :

f₁ ≤ f₂ → f₁ - g ≤ f₂ - g

theorem Filter.div_le_div_right {α : Type u_1} [inst : Div α] {f₁ : Filter α} {f₂ : Filter α} {g : Filter α} :

f₁ ≤ f₂ → f₁ / g ≤ f₂ / g

@[simp]

theorem Filter.le_sub_iff {α : Type u_1} [inst : 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_1} [inst : Div α] {f : Filter α} {g : Filter α} {h : Filter α} :

h ≤ f / g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s / t ∈ h

def Filter.covariant_sub.proof_1 {α : Type u_1} [inst : Sub α] :

CovariantClass (Filter α) (Filter α) (fun x x_1 => x - x_1) fun x x_1 => x ≤ x_1

Equations

(_ : CovariantClass (Filter α) (Filter α) (fun x x_1 => x - x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass (Filter α) (Filter α) (fun x x_1 => x - x_1) fun x x_1 => x ≤ x_1)

instance Filter.covariant_sub {α : Type u_1} [inst : 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

instance Filter.covariant_div {α : Type u_1} [inst : 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

instance Filter.covariant_swap_sub {α : Type u_1} [inst : 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

def Filter.covariant_swap_sub.proof_1 {α : Type u_1} [inst : Sub α] :

CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x - x_1) fun x x_1 => x ≤ x_1

Equations

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

instance Filter.covariant_swap_div {α : Type u_1} [inst : 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_1} [inst : Zero α] [inst : 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_1} [inst : One α] [inst : 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_1} [inst : Zero α] [inst : Add α] [inst : 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_1} [inst : One α] [inst : Mul α] [inst : 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 }

def Filter.addSemigroup {α : Type u_1} [inst : 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.addSemigroup.proof_1 {α : Type u_1} [inst : 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)

Equations

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

def Filter.semigroup {α : Type u_1} [inst : 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.

def Filter.addCommSemigroup.proof_2 {α : Type u_1} [inst : 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

Equations

(_ : Filter.map₂ (fun x x_1 => x + x_1) x x = Filter.map₂ (fun x x_1 => x + x_1) x x) = (_ : Filter.map₂ (fun x x_1 => x + x_1) x x = Filter.map₂ (fun x x_1 => x + x_1) x x)

def Filter.addCommSemigroup.proof_1 {α : Type u_1} [inst : AddCommSemigroup α] (a : Filter α) (b : Filter α) (c : Filter α) :

a + b + c = a + (b + c)

Equations

(_ : ∀ (a b c : Filter α), a + b + c = a + (b + c)) = (_ : ∀ (a b c : Filter α), a + b + c = a + (b + c))

def Filter.addCommSemigroup {α : Type u_1} [inst : 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.

def Filter.commSemigroup {α : Type u_1} [inst : 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)

def Filter.addZeroClass.proof_2 {α : Type u_1} [inst : AddZeroClass α] (l : Filter α) :

Filter.map₂ (fun x x_1 => x + x_1) l (pure 0) = l

Equations

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

def Filter.addZeroClass {α : Type u_1} [inst : 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)

def Filter.addZeroClass.proof_1 {α : Type u_1} [inst : AddZeroClass α] (l : Filter α) :

Filter.map₂ (fun x x_1 => x + x_1) (pure 0) l = l

Equations

(_ : ∀ (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) (pure 0) l = l)

def Filter.mulOneClass {α : Type u_1} [inst : 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)

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

∀ (x x_1 : Filter α), Filter.map (↑φ) (x + x_1) = Filter.map (↑φ) x + Filter.map (↑φ) x_1

Equations

(_ : Filter.map (↑φ) (x + x) = Filter.map (↑φ) x + Filter.map (↑φ) x) = (_ : Filter.map (↑φ) (x + x) = Filter.map (↑φ) x + Filter.map (↑φ) x)

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

Filter.map (↑φ) 0 = 0

Equations

(_ : Filter.map (↑φ) 0 = 0) = (_ : Filter.map (↑φ) 0 = 0)

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

Filter α →+ Filter β

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

Equations

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

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

Filter α →* Filter β

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

Equations

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

abbrev Filter.comap_add_comap_le.match_1 {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : 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_add_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddHomClass F α β] (m : F) {f : Filter β} {g : Filter β} :

Filter.comap (↑m) f + Filter.comap (↑m) g ≤ Filter.comap (↑m) (f + g)

theorem Filter.comap_mul_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass α] [inst : MulOneClass β] [inst : 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} [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : 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} [inst : MulOneClass α] [inst : MulOneClass β] [inst : 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₂)

def Filter.pureAddMonoidHom {α : Type u_1} [inst : AddZeroClass α] :

α →+ Filter α

pure as an AddMonoidHom.

Equations

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

def Filter.pureAddMonoidHom.proof_2 {α : Type u_1} [inst : AddZeroClass α] (x : α) (y : α) :

AddHom.toFun Filter.pureAddHom (x + y) = AddHom.toFun Filter.pureAddHom x + AddHom.toFun Filter.pureAddHom y

Equations

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

def Filter.pureAddMonoidHom.proof_1 {α : Type u_1} [inst : AddZeroClass α] :

ZeroHom.toFun Filter.pureZeroHom 0 = 0

Equations

(_ : ZeroHom.toFun Filter.pureZeroHom 0 = 0) = (_ : ZeroHom.toFun Filter.pureZeroHom 0 = 0)

def Filter.pureMonoidHom {α : Type u_1} [inst : 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_1} [inst : AddZeroClass α] :

↑Filter.pureAddMonoidHom = pure

@[simp]

theorem Filter.coe_pureMonoidHom {α : Type u_1} [inst : MulOneClass α] :

↑Filter.pureMonoidHom = pure

@[simp]

theorem Filter.pureAddMonoidHom_apply {α : Type u_1} [inst : AddZeroClass α] (a : α) :

↑Filter.pureAddMonoidHom a = pure a

@[simp]

theorem Filter.pureMonoidHom_apply {α : Type u_1} [inst : MulOneClass α] (a : α) :

↑Filter.pureMonoidHom a = pure a

def Filter.addMonoid.proof_1 {α : Type u_1} [inst : AddMonoid α] (a : Filter α) (b : Filter α) (c : Filter α) :

a + b + c = a + (b + c)

Equations

(_ : ∀ (a b c : Filter α), a + b + c = a + (b + c)) = (_ : ∀ (a b c : Filter α), a + b + c = a + (b + c))

def Filter.addMonoid {α : Type u_1} [inst : 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.

def Filter.addMonoid.proof_2 {α : Type u_1} [inst : AddMonoid α] (a : Filter α) :

0 + a = a

Equations

(_ : ∀ (a : Filter α), 0 + a = a) = (_ : ∀ (a : Filter α), 0 + a = a)

def Filter.addMonoid.proof_5 {α : Type u_1} [inst : AddMonoid α] :

∀ (n : ℕ) (x : Filter α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

Equations

(_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)

def Filter.addMonoid.proof_4 {α : Type u_1} [inst : AddMonoid α] :

∀ (x : Filter α), nsmulRec 0 x = nsmulRec 0 x

Equations

(_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)

def Filter.addMonoid.proof_3 {α : Type u_1} [inst : AddMonoid α] (a : Filter α) :

a + 0 = a

Equations

(_ : ∀ (a : Filter α), a + 0 = a) = (_ : ∀ (a : Filter α), a + 0 = a)

def Filter.monoid {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : Monoid α] {f : Filter α} {s : Set α} (hs : s ∈ f) (n : ℕ) :

s ^ n ∈ f ^ n

@[simp]

theorem Filter.nsmul_bot {α : Type u_1} [inst : AddMonoid α] {n : ℕ} (hn : n ≠ 0) :

n • ⊥ = ⊥

@[simp]

theorem Filter.bot_pow {α : Type u_1} [inst : Monoid α] {n : ℕ} (hn : n ≠ 0) :

theorem Filter.add_top_of_nonneg {α : Type u_1} [inst : AddMonoid α] {f : Filter α} (hf : 0 ≤ f) :

theorem Filter.mul_top_of_one_le {α : Type u_1} [inst : Monoid α] {f : Filter α} (hf : 1 ≤ f) :

theorem Filter.top_add_of_nonneg {α : Type u_1} [inst : AddMonoid α] {f : Filter α} (hf : 0 ≤ f) :

theorem Filter.top_mul_of_one_le {α : Type u_1} [inst : Monoid α] {f : Filter α} (hf : 1 ≤ f) :

@[simp]

theorem Filter.top_add_top {α : Type u_1} [inst : AddMonoid α] :

⊤ + ⊤ = ⊤

@[simp]

theorem Filter.top_mul_top {α : Type u_1} [inst : Monoid α] :

⊤ * ⊤ = ⊤

theorem Filter.nsmul_top {α : Type u_1} [inst : AddMonoid α] {n : ℕ} :

n ≠ 0 → n • ⊤ = ⊤

theorem Filter.top_pow {α : Type u_1} [inst : Monoid α] {n : ℕ} :

n ≠ 0 → ⊤ ^ n = ⊤

theorem IsAddUnit.filter {α : Type u_1} [inst : AddMonoid α] {a : α} :

IsAddUnit a → IsAddUnit (pure a)

theorem IsUnit.filter {α : Type u_1} [inst : Monoid α] {a : α} :

IsUnit a → IsUnit (pure a)

def Filter.addCommMonoid.proof_3 {α : Type u_1} [inst : AddCommMonoid α] :

∀ (x : Filter α), nsmulRec 0 x = nsmulRec 0 x

Equations

(_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)

def Filter.addCommMonoid.proof_5 {α : Type u_1} [inst : AddCommMonoid α] (a : Filter α) (b : Filter α) :

a + b = b + a

Equations

(_ : ∀ (a b : Filter α), a + b = b + a) = (_ : ∀ (a b : Filter α), a + b = b + a)

def Filter.addCommMonoid.proof_2 {α : Type u_1} [inst : AddCommMonoid α] (a : Filter α) :

a + 0 = a

Equations

(_ : ∀ (a : Filter α), a + 0 = a) = (_ : ∀ (a : Filter α), a + 0 = a)

def Filter.addCommMonoid.proof_4 {α : Type u_1} [inst : AddCommMonoid α] :

∀ (n : ℕ) (x : Filter α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

Equations

(_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)

def Filter.addCommMonoid.proof_1 {α : Type u_1} [inst : AddCommMonoid α] (a : Filter α) :

0 + a = a

Equations

(_ : ∀ (a : Filter α), 0 + a = a) = (_ : ∀ (a : Filter α), 0 + a = a)

def Filter.addCommMonoid {α : Type u_1} [inst : 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)

def Filter.commMonoid {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : DivisionMonoid α] {f : Filter α} {g : Filter α} :

f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

def Filter.subtractionMonoid.proof_8 {α : Type u_1} [inst : SubtractionMonoid α] :

∀ (n : ℕ) (a : Filter α), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a

Equations

(_ : zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a) = (_ : zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a)

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

-s = t

Equations

(_ : -s = t) = (_ : -s = t)

def Filter.subtractionMonoid.proof_2 {α : Type u_1} [inst : SubtractionMonoid α] (a : Filter α) :

a + 0 = a

Equations

(_ : ∀ (a : Filter α), a + 0 = a) = (_ : ∀ (a : Filter α), a + 0 = a)

def Filter.subtractionMonoid.proof_7 {α : Type u_1} [inst : SubtractionMonoid α] :

∀ (a : Filter α), zsmulRec 0 a = zsmulRec 0 a

Equations

(_ : zsmulRec 0 a = zsmulRec 0 a) = (_ : zsmulRec 0 a = zsmulRec 0 a)

def Filter.subtractionMonoid.proof_3 {α : Type u_1} [inst : SubtractionMonoid α] (x : Filter α) :

AddMonoid.nsmul 0 x = 0

Equations

(_ : ∀ (x : Filter α), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : Filter α), AddMonoid.nsmul 0 x = 0)

def Filter.subtractionMonoid {α : Type u_1} [inst : 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.

def Filter.subtractionMonoid.proof_10 {α : Type u_1} [inst : SubtractionMonoid α] (x : Filter α) :

- -x = x

Equations

(_ : ∀ (x : Filter α), - -x = x) = (_ : ∀ (x : Filter α), - -x = x)

def Filter.subtractionMonoid.proof_6 {α : Type u_1} [inst : SubtractionMonoid α] (a : Filter α) (b : Filter α) (c : Filter α) :

a + b + c = a + (b + c)

Equations

(_ : ∀ (a b c : Filter α), a + b + c = a + (b + c)) = (_ : ∀ (a b c : Filter α), a + b + c = a + (b + c))

def Filter.subtractionMonoid.proof_9 {α : Type u_1} [inst : SubtractionMonoid α] :

∀ (n : ℕ) (a : Filter α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

Equations

(_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a) = (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a)

def Filter.subtractionMonoid.proof_5 {α : Type u_1} [inst : 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)

Equations

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

def Filter.subtractionMonoid.proof_1 {α : Type u_1} [inst : SubtractionMonoid α] (a : Filter α) :

0 + a = a

Equations

(_ : ∀ (a : Filter α), 0 + a = a) = (_ : ∀ (a : Filter α), 0 + a = a)

def Filter.subtractionMonoid.proof_4 {α : Type u_1} [inst : SubtractionMonoid α] (n : ℕ) (x : Filter α) :

AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

(_ : ∀ (n : ℕ) (x : Filter α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : Filter α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

def Filter.subtractionMonoid.proof_11 {α : Type u_1} [inst : 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)

Equations

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

def Filter.divisionMonoid {α : Type u_1} [inst : 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_1} [inst : SubtractionMonoid α] {f : Filter α} :

IsAddUnit f ↔ ∃ a, f = pure a ∧ IsAddUnit a

theorem Filter.isUnit_iff {α : Type u_1} [inst : DivisionMonoid α] {f : Filter α} :

IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a

def Filter.subtractionCommMonoid.proof_2 {α : Type u_1} [inst : SubtractionCommMonoid α] (a : Filter α) (b : Filter α) :

-(a + b) = -b + -a

Equations

(_ : ∀ (a b : Filter α), -(a + b) = -b + -a) = (_ : ∀ (a b : Filter α), -(a + b) = -b + -a)

def Filter.subtractionCommMonoid {α : Type u_1} [inst : 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.subtractionCommMonoid.proof_4 {α : Type u_1} [inst : SubtractionCommMonoid α] (a : Filter α) (b : Filter α) :

a + b = b + a

Equations

(_ : ∀ (a b : Filter α), a + b = b + a) = (_ : ∀ (a b : Filter α), a + b = b + a)

def Filter.subtractionCommMonoid.proof_1 {α : Type u_1} [inst : SubtractionCommMonoid α] (x : Filter α) :

- -x = x

Equations

(_ : ∀ (x : Filter α), - -x = x) = (_ : ∀ (x : Filter α), - -x = x)

def Filter.subtractionCommMonoid.proof_3 {α : Type u_1} [inst : SubtractionCommMonoid α] (a : Filter α) (b : Filter α) :

a + b = 0 → -a = b

Equations

(_ : ∀ (a b : Filter α), a + b = 0 → -a = b) = (_ : ∀ (a b : Filter α), a + b = 0 → -a = b)

def Filter.divisionCommMonoid {α : Type u_1} [inst : 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_1} [inst : Mul α] [inst : 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_1} [inst : Distrib α] {f : Filter α} {g : Filter α} {h : Filter α} :

f * (g + h) ≤ f * g + f * h

theorem Filter.add_mul_subset {α : Type u_1} [inst : Distrib α] {f : Filter α} {g : Filter α} {h : Filter α} :

(f + g) * h ≤ f * h + g * h

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

theorem Filter.NeBot.mul_zero_nonneg {α : Type u_1} [inst : MulZeroClass α] {f : Filter α} (hf : Filter.NeBot f) :

0 ≤ f * 0

theorem Filter.NeBot.zero_mul_nonneg {α : Type u_1} [inst : MulZeroClass α] {g : Filter α} (hg : Filter.NeBot g) :

0 ≤ 0 * g

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

@[simp]

theorem Filter.nonneg_sub_iff {α : Type u_1} [inst : AddGroup α] {f : Filter α} {g : Filter α} :

0 ≤ f - g ↔ ¬Disjoint f g

@[simp]

theorem Filter.one_le_div_iff {α : Type u_1} [inst : Group α] {f : Filter α} {g : Filter α} :

1 ≤ f / g ↔ ¬Disjoint f g

theorem Filter.not_nonneg_sub_iff {α : Type u_1} [inst : AddGroup α] {f : Filter α} {g : Filter α} :

¬0 ≤ f - g ↔ Disjoint f g

theorem Filter.not_one_le_div_iff {α : Type u_1} [inst : Group α] {f : Filter α} {g : Filter α} :

¬1 ≤ f / g ↔ Disjoint f g

theorem Filter.NeBot.nonneg_sub {α : Type u_1} [inst : AddGroup α] {f : Filter α} (h : Filter.NeBot f) :

0 ≤ f - f

theorem Filter.NeBot.one_le_div {α : Type u_1} [inst : Group α] {f : Filter α} (h : Filter.NeBot f) :

1 ≤ f / f

theorem Filter.isAddUnit_pure {α : Type u_1} [inst : AddGroup α] (a : α) :

IsAddUnit (pure a)

theorem Filter.isUnit_pure {α : Type u_1} [inst : Group α] (a : α) :

IsUnit (pure a)

@[simp]

theorem Filter.isUnit_iff_singleton {α : Type u_1} [inst : Group α] {f : Filter α} :

IsUnit f ↔ ∃ a, f = pure a

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

Filter.map (↑m) (-f) = -Filter.map (↑m) f

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

Filter.map (↑m) f⁻¹ = (Filter.map (↑m) f)⁻¹

theorem Filter.Tendsto.neg_neg {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : SubtractionMonoid β] [inst : 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_3} {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : DivisionMonoid β] [inst : 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_3} {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : SubtractionMonoid β] [inst : 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_3} {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : DivisionMonoid β] [inst : 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_3} {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : SubtractionMonoid β] [inst : 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_3} {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : DivisionMonoid β] [inst : 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_1} [inst : GroupWithZero α] {f : Filter α} (hf : Filter.NeBot f) :

0 ≤ f / 0

theorem Filter.NeBot.zero_div_nonneg {α : Type u_1} [inst : GroupWithZero α] {g : Filter α} (hg : Filter.NeBot g) :

0 ≤ 0 / g

Scalar addition/multiplication of filters #

def Filter.instVAdd.proof_2 {α : Type u_2} {β : Type u_1} [inst : VAdd α β] (f : Filter α) (g : Filter β) :

∀ {x y : Set β}, x ∈ (Filter.map₂ (fun x x_1 => x +ᵥ x_1) f g).sets → y ∈ (Filter.map₂ (fun x x_1 => x +ᵥ x_1) f g).sets → x ∩ y ∈ (Filter.map₂ (fun x x_1 => x +ᵥ x_1) f g).sets

Equations

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

def Filter.instVAdd.proof_1 {α : Type u_2} {β : Type u_1} [inst : VAdd α β] (f : Filter α) (g : Filter β) :

∀ {x y : Set β}, x ∈ (Filter.map₂ (fun x x_1 => x +ᵥ x_1) f g).sets → x ⊆ y → y ∈ (Filter.map₂ (fun x x_1 => x +ᵥ x_1) f g).sets

Equations

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

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

VAdd (Filter α) (Filter β)

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

Equations

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

def Filter.instSMul {α : Type u_1} {β : Type u_2} [inst : SMul α β] :

SMul (Filter α) (Filter β)

The filter f • g is generated by {s • t | s ∈ f, t ∈ g}∈ f, t ∈ g}∈ 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_1} [inst : 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_1} [inst : 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_1} [inst : 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_1} [inst : 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_1} {β : Type u_2} [inst : VAdd α β] {f : Filter α} {g : Filter β} {s : Set α} {t : Set β} :

s ∈ f → t ∈ g → s +ᵥ t ∈ f +ᵥ g

theorem Filter.smul_mem_smul {α : Type u_1} {β : Type u_2} [inst : 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_1} [inst : VAdd α β] {g : Filter β} :

⊥ +ᵥ g = ⊥

@[simp]

theorem Filter.bot_smul {α : Type u_2} {β : Type u_1} [inst : SMul α β] {g : Filter β} :

⊥ • g = ⊥

@[simp]

theorem Filter.vadd_bot {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {f : Filter α} :

f +ᵥ ⊥ = ⊥

@[simp]

theorem Filter.smul_bot {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter α} :

f • ⊥ = ⊥

@[simp]

theorem Filter.vadd_eq_bot_iff {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {f : Filter α} {g : Filter β} :

f +ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.smul_eq_bot_iff {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter α} {g : Filter β} :

f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.vadd_neBot_iff {α : Type u_2} {β : Type u_1} [inst : 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_1} [inst : SMul α β] {f : Filter α} {g : Filter β} :

Filter.NeBot (f • g) ↔ Filter.NeBot f ∧ Filter.NeBot g

theorem Filter.NeBot.vadd {α : Type u_1} {β : Type u_2} [inst : VAdd α β] {f : Filter α} {g : Filter β} :

Filter.NeBot f → Filter.NeBot g → Filter.NeBot (f +ᵥ g)

theorem Filter.NeBot.smul {α : Type u_1} {β : Type u_2} [inst : 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_1} [inst : VAdd α β] {f : Filter α} {g : Filter β} :

Filter.NeBot (f +ᵥ g) → Filter.NeBot f

theorem Filter.NeBot.of_smul_left {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter α} {g : Filter β} :

Filter.NeBot (f • g) → Filter.NeBot f

theorem Filter.NeBot.of_vadd_right {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {f : Filter α} {g : Filter β} :

Filter.NeBot (f +ᵥ g) → Filter.NeBot g

theorem Filter.NeBot.of_smul_right {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter α} {g : Filter β} :

Filter.NeBot (f • g) → Filter.NeBot g

@[simp]

theorem Filter.pure_vadd {α : Type u_2} {β : Type u_1} [inst : 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_1} [inst : 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_1} [inst : VAdd α β] {f : Filter α} {b : β} :

f +ᵥ pure b = Filter.map (fun x => x +ᵥ b) f

@[simp]

theorem Filter.smul_pure {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter α} {b : β} :

f • pure b = Filter.map (fun x => x • b) f

theorem Filter.pure_vadd_pure {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {a : α} {b : β} :

pure a +ᵥ pure b = pure (a +ᵥ b)

theorem Filter.pure_smul_pure {α : Type u_2} {β : Type u_1} [inst : SMul α β] {a : α} {b : β} :

pure a • pure b = pure (a • b)

theorem Filter.vadd_le_vadd {α : Type u_1} {β : Type u_2} [inst : VAdd α β] {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter β} {g₂ : Filter β} :

f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ +ᵥ g₁ ≤ f₂ +ᵥ g₂

theorem Filter.smul_le_smul {α : Type u_1} {β : Type u_2} [inst : 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_1} [inst : VAdd α β] {f : Filter α} {g₁ : Filter β} {g₂ : Filter β} :

g₁ ≤ g₂ → f +ᵥ g₁ ≤ f +ᵥ g₂

theorem Filter.smul_le_smul_left {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter α} {g₁ : Filter β} {g₂ : Filter β} :

g₁ ≤ g₂ → f • g₁ ≤ f • g₂

theorem Filter.vadd_le_vadd_right {α : Type u_1} {β : Type u_2} [inst : VAdd α β] {f₁ : Filter α} {f₂ : Filter α} {g : Filter β} :

f₁ ≤ f₂ → f₁ +ᵥ g ≤ f₂ +ᵥ g

theorem Filter.smul_le_smul_right {α : Type u_1} {β : Type u_2} [inst : SMul α β] {f₁ : Filter α} {f₂ : Filter α} {g : Filter β} :

f₁ ≤ f₂ → f₁ • g ≤ f₂ • g

@[simp]

theorem Filter.le_vadd_iff {α : Type u_2} {β : Type u_1} [inst : 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_1} [inst : SMul α β] {f : Filter α} {g : Filter β} {h : Filter β} :

h ≤ f • g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s • t ∈ h

def Filter.covariant_vadd.proof_1 {α : Type u_1} {β : Type u_2} [inst : VAdd α β] :

CovariantClass (Filter α) (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1

Equations

(_ : CovariantClass (Filter α) (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass (Filter α) (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1)

instance Filter.covariant_vadd {α : Type u_1} {β : Type u_2} [inst : 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

instance Filter.covariant_smul {α : Type u_1} {β : Type u_2} [inst : 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_1} {β : Type u_2} [inst : VSub α β] :

VSub (Filter α) (Filter β)

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

Equations

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

@[simp]

theorem Filter.map₂_vsub {α : Type u_1} {β : Type u_2} [inst : VSub α β] {f : Filter β} {g : Filter β} :

Filter.map₂ (fun x x_1 => x -ᵥ x_1) f g = f -ᵥ g

theorem Filter.mem_vsub {α : Type u_1} {β : Type u_2} [inst : 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_1} [inst : VSub α β] {f : Filter β} {g : Filter β} {s : Set β} {t : Set β} :

s ∈ f → t ∈ g → s -ᵥ t ∈ f -ᵥ g

@[simp]

theorem Filter.bot_vsub {α : Type u_1} {β : Type u_2} [inst : VSub α β] {g : Filter β} :

⊥ -ᵥ g = ⊥

@[simp]

theorem Filter.vsub_bot {α : Type u_1} {β : Type u_2} [inst : VSub α β] {f : Filter β} :

f -ᵥ ⊥ = ⊥

@[simp]

theorem Filter.vsub_eq_bot_iff {α : Type u_1} {β : Type u_2} [inst : VSub α β] {f : Filter β} {g : Filter β} :

f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[simp]

theorem Filter.vsub_neBot_iff {α : Type u_1} {β : Type u_2} [inst : VSub α β] {f : Filter β} {g : Filter β} :

Filter.NeBot (f -ᵥ g) ↔ Filter.NeBot f ∧ Filter.NeBot g

theorem Filter.NeBot.vsub {α : Type u_2} {β : Type u_1} [inst : VSub α β] {f : Filter β} {g : Filter β} :

Filter.NeBot f → Filter.NeBot g → Filter.NeBot (f -ᵥ g)

theorem Filter.NeBot.of_vsub_left {α : Type u_1} {β : Type u_2} [inst : VSub α β] {f : Filter β} {g : Filter β} :

Filter.NeBot (f -ᵥ g) → Filter.NeBot f

theorem Filter.NeBot.of_vsub_right {α : Type u_1} {β : Type u_2} [inst : VSub α β] {f : Filter β} {g : Filter β} :

Filter.NeBot (f -ᵥ g) → Filter.NeBot g

@[simp]

theorem Filter.pure_vsub {α : Type u_1} {β : Type u_2} [inst : 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_1} {β : Type u_2} [inst : VSub α β] {f : Filter β} {b : β} :

f -ᵥ pure b = Filter.map (fun x => x -ᵥ b) f

theorem Filter.pure_vsub_pure {α : Type u_1} {β : Type u_2} [inst : VSub α β] {a : β} {b : β} :

pure a -ᵥ pure b = pure (a -ᵥ b)

theorem Filter.vsub_le_vsub {α : Type u_2} {β : Type u_1} [inst : 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_1} [inst : VSub α β] {f : Filter β} {g₁ : Filter β} {g₂ : Filter β} :

g₁ ≤ g₂ → f -ᵥ g₁ ≤ f -ᵥ g₂

theorem Filter.vsub_le_vsub_right {α : Type u_2} {β : Type u_1} [inst : VSub α β] {f₁ : Filter β} {f₂ : Filter β} {g : Filter β} :

f₁ ≤ f₂ → f₁ -ᵥ g ≤ f₂ -ᵥ g

@[simp]

theorem Filter.le_vsub_iff {α : Type u_1} {β : Type u_2} [inst : 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_1} {β : Type u_2} [inst : 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_1} {β : Type u_2} [inst : 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_1} [inst : VAdd α β] {f : Filter β} {a : α} :

Filter.map (fun b => a +ᵥ b) f = a +ᵥ f

@[simp]

theorem Filter.map_smul {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter β} {a : α} :

Filter.map (fun b => a • b) f = a • f

theorem Filter.mem_vadd_filter {α : Type u_2} {β : Type u_1} [inst : 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_1} [inst : 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_1} [inst : VAdd α β] {f : Filter β} {s : Set β} {a : α} :

s ∈ f → a +ᵥ s ∈ a +ᵥ f

theorem Filter.smul_set_mem_smul_filter {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter β} {s : Set β} {a : α} :

s ∈ f → a • s ∈ a • f

@[simp]

theorem Filter.vadd_filter_bot {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {a : α} :

a +ᵥ ⊥ = ⊥

@[simp]

theorem Filter.smul_filter_bot {α : Type u_2} {β : Type u_1} [inst : SMul α β] {a : α} :

a • ⊥ = ⊥

@[simp]

theorem Filter.vadd_filter_eq_bot_iff {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {f : Filter β} {a : α} :

a +ᵥ f = ⊥ ↔ f = ⊥

@[simp]

theorem Filter.smul_filter_eq_bot_iff {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter β} {a : α} :

a • f = ⊥ ↔ f = ⊥

@[simp]

theorem Filter.vadd_filter_neBot_iff {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {f : Filter β} {a : α} :

Filter.NeBot (a +ᵥ f) ↔ Filter.NeBot f

@[simp]

theorem Filter.smul_filter_neBot_iff {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter β} {a : α} :

Filter.NeBot (a • f) ↔ Filter.NeBot f

theorem Filter.NeBot.vadd_filter {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {f : Filter β} {a : α} :

Filter.NeBot f → Filter.NeBot (a +ᵥ f)

theorem Filter.NeBot.smul_filter {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter β} {a : α} :

Filter.NeBot f → Filter.NeBot (a • f)

theorem Filter.NeBot.of_vadd_filter {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {f : Filter β} {a : α} :

Filter.NeBot (a +ᵥ f) → Filter.NeBot f

theorem Filter.NeBot.of_smul_filter {α : Type u_2} {β : Type u_1} [inst : SMul α β] {f : Filter β} {a : α} :

Filter.NeBot (a • f) → Filter.NeBot f

theorem Filter.vadd_filter_le_vadd_filter {α : Type u_2} {β : Type u_1} [inst : 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_1} [inst : SMul α β] {f₁ : Filter β} {f₂ : Filter β} {a : α} (hf : f₁ ≤ f₂) :

a • f₁ ≤ a • f₂

def Filter.covariant_vadd_filter.proof_1 {α : Type u_1} {β : Type u_2} [inst : VAdd α β] :

CovariantClass α (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1

Equations

(_ : CovariantClass α (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass α (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1)

instance Filter.covariant_vadd_filter {α : Type u_1} {β : Type u_2} [inst : 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_1} {β : Type u_2} [inst : 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_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :

VAddCommClass α β (Filter γ)

Equations

@Filter.vaddCommClass_filter = @Filter.vaddCommClass_filter.proof_1

def Filter.vaddCommClass_filter.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :

VAddCommClass α β (Filter γ)

Equations

(_ : VAddCommClass α β (Filter γ)) = (_ : VAddCommClass α β (Filter γ))

instance Filter.smulCommClass_filter {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α γ] [inst : SMul β γ] [inst : SMulCommClass α β γ] :

SMulCommClass α β (Filter γ)

Equations

@Filter.smulCommClass_filter = @Filter.smulCommClass_filter.proof_1

instance Filter.vaddCommClass_filter' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :

VAddCommClass α (Filter β) (Filter γ)

Equations

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

def Filter.vaddCommClass_filter'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :

VAddCommClass α (Filter β) (Filter γ)

Equations

(_ : VAddCommClass α (Filter β) (Filter γ)) = (_ : VAddCommClass α (Filter β) (Filter γ))

instance Filter.smulCommClass_filter' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α γ] [inst : SMul β γ] [inst : SMulCommClass α β γ] :

SMulCommClass α (Filter β) (Filter γ)

Equations

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

def Filter.vaddCommClass_filter''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :

VAddCommClass (Filter α) β (Filter γ)

Equations

(_ : VAddCommClass (Filter α) β (Filter γ)) = (_ : VAddCommClass (Filter α) β (Filter γ))

instance Filter.vaddCommClass_filter'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :

VAddCommClass (Filter α) β (Filter γ)

Equations

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

instance Filter.smulCommClass_filter'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α γ] [inst : SMul β γ] [inst : SMulCommClass α β γ] :

SMulCommClass (Filter α) β (Filter γ)

Equations

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

instance Filter.vaddCommClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :

VAddCommClass (Filter α) (Filter β) (Filter γ)

Equations

@Filter.vaddCommClass = @Filter.vaddCommClass.proof_1

def Filter.vaddCommClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :

VAddCommClass (Filter α) (Filter β) (Filter γ)

Equations

(_ : VAddCommClass (Filter α) (Filter β) (Filter γ)) = (_ : VAddCommClass (Filter α) (Filter β) (Filter γ))

instance Filter.smulCommClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α γ] [inst : SMul β γ] [inst : SMulCommClass α β γ] :

SMulCommClass (Filter α) (Filter β) (Filter γ)

Equations

@Filter.smulCommClass = @Filter.smulCommClass.proof_1

def Filter.vaddAssocClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :

VAddAssocClass α β (Filter γ)

Equations

(_ : VAddAssocClass α β (Filter γ)) = (_ : VAddAssocClass α β (Filter γ))

instance Filter.vaddAssocClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :

VAddAssocClass α β (Filter γ)

Equations

@Filter.vaddAssocClass = @Filter.vaddAssocClass.proof_1

instance Filter.isScalarTower {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α β] [inst : SMul α γ] [inst : SMul β γ] [inst : IsScalarTower α β γ] :

IsScalarTower α β (Filter γ)

Equations

@Filter.isScalarTower = @Filter.isScalarTower.proof_1

def Filter.vaddAssocClass'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :

VAddAssocClass α (Filter β) (Filter γ)

Equations

(_ : VAddAssocClass α (Filter β) (Filter γ)) = (_ : VAddAssocClass α (Filter β) (Filter γ))

instance Filter.vaddAssocClass' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :

VAddAssocClass α (Filter β) (Filter γ)

Equations

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

instance Filter.isScalarTower' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α β] [inst : SMul α γ] [inst : SMul β γ] [inst : IsScalarTower α β γ] :

IsScalarTower α (Filter β) (Filter γ)

Equations

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

def Filter.vaddAssocClass''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :

VAddAssocClass (Filter α) (Filter β) (Filter γ)

Equations

(_ : VAddAssocClass (Filter α) (Filter β) (Filter γ)) = (_ : VAddAssocClass (Filter α) (Filter β) (Filter γ))

instance Filter.vaddAssocClass'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :

VAddAssocClass (Filter α) (Filter β) (Filter γ)

Equations

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

instance Filter.isScalarTower'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α β] [inst : SMul α γ] [inst : SMul β γ] [inst : IsScalarTower α β γ] :

IsScalarTower (Filter α) (Filter β) (Filter γ)

Equations

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

def Filter.isCentralVAdd.proof_1 {α : Type u_1} {β : Type u_2} [inst : VAdd α β] [inst : VAdd αᵃᵒᵖ β] [inst : IsCentralVAdd α β] :

IsCentralVAdd α (Filter β)

Equations

(_ : IsCentralVAdd α (Filter β)) = (_ : IsCentralVAdd α (Filter β))

instance Filter.isCentralVAdd {α : Type u_1} {β : Type u_2} [inst : VAdd α β] [inst : VAdd αᵃᵒᵖ β] [inst : IsCentralVAdd α β] :

IsCentralVAdd α (Filter β)

Equations

@Filter.isCentralVAdd = @Filter.isCentralVAdd.proof_1

instance Filter.isCentralScalar {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst : SMul αᵐᵒᵖ β] [inst : IsCentralScalar α β] :

IsCentralScalar α (Filter β)

Equations

@Filter.isCentralScalar = @Filter.isCentralScalar.proof_1

def Filter.addAction.proof_1 {α : Type u_2} {β : Type u_1} [inst : AddMonoid α] [inst : AddAction α β] (f : Filter β) :

Filter.map₂ (fun x x_1 => x +ᵥ x_1) (pure 0) f = f

Equations

(_ : Filter.map₂ (fun x x_1 => x +ᵥ x_1) (pure 0) f = f) = (_ : Filter.map₂ (fun x x_1 => x +ᵥ x_1) (pure 0) f = f)

def Filter.addAction.proof_2 {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst : 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)

Equations

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

def Filter.addAction {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst : 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.

def Filter.mulAction {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst : 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.

def Filter.addActionFilter.proof_2 {α : Type u_2} {β : Type u_1} [inst : AddMonoid α] [inst : 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)

Equations

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

def Filter.addActionFilter {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst : 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.

def Filter.addActionFilter.proof_1 {α : Type u_2} {β : Type u_1} [inst : AddMonoid α] [inst : AddAction α β] (f : Filter β) :

Filter.map (fun x => 0 +ᵥ x) f = f

Equations

(_ : Filter.map (fun x => 0 +ᵥ x) f = f) = (_ : Filter.map (fun x => 0 +ᵥ x) f = f)

def Filter.mulActionFilter {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst : 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_1} {β : Type u_2} [inst : Monoid α] [inst : AddMonoid β] [inst : 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_1} {β : Type u_2} [inst : Monoid α] [inst : Monoid β] [inst : 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⊥ ≠ 0≠ 0.

theorem Filter.NeBot.smul_zero_nonneg {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {f : Filter α} (hf : Filter.NeBot f) :

0 ≤ f • 0

theorem Filter.NeBot.zero_smul_nonneg {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {g : Filter β} (hg : Filter.NeBot g) :

0 ≤ 0 • g

theorem Filter.zero_smul_filter_nonpos {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {g : Filter β} :

0 • g ≤ 0

theorem Filter.zero_smul_filter {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {g : Filter β} (hg : Filter.NeBot g) :

0 • g = 0