mathlib3 documentation

order.filter.pointwise

Pointwise operations on filters #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines pointwise operations on filters. This is useful because usual algebraic operations distribute over pointwise operations. For example,

Main declarations #

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 #

source
@[protected]
def filter.has_zero {α : Type u_2} [has_zero α] :
has_zero (filter α)

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

Equations
source
@[protected]
def filter.has_one {α : Type u_2} [has_one α] :
has_one (filter α)

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

Equations
source
@[simp]
theorem filter.mem_zero {α : Type u_2} [has_zero α] {s : set α} :
s ∈ 0 ↔ 0 ∈ s
source
@[simp]
theorem filter.mem_one {α : Type u_2} [has_one α] {s : set α} :
s ∈ 1 ↔ 1 ∈ s
source
theorem filter.zero_mem_zero {α : Type u_2} [has_zero α] :
0 ∈ 0
source
theorem filter.one_mem_one {α : Type u_2} [has_one α] :
1 ∈ 1
source
@[simp]
theorem filter.pure_zero {α : Type u_2} [has_zero α] :
has_pure.pure 0 = 0
source
@[simp]
theorem filter.pure_one {α : Type u_2} [has_one α] :
has_pure.pure 1 = 1
source
@[simp]
theorem filter.principal_one {α : Type u_2} [has_one α] :
filter.principal 1 = 1
source
@[simp]
theorem filter.principal_zero {α : Type u_2} [has_zero α] :
filter.principal 0 = 0
source
theorem filter.one_ne_bot {α : Type u_2} [has_one α] :
1.ne_bot
source
theorem filter.zero_ne_bot {α : Type u_2} [has_zero α] :
0.ne_bot
source
@[protected, simp]
theorem filter.map_one' {α : Type u_2} {β : Type u_3} [has_one α] (f : α → β) :
filter.map f 1 = has_pure.pure (f 1)
source
@[protected, simp]
theorem filter.map_zero' {α : Type u_2} {β : Type u_3} [has_zero α] (f : α → β) :
filter.map f 0 = has_pure.pure (f 0)
source
@[simp]
theorem filter.nonpos_iff {α : Type u_2} [has_zero α] {f : filter α} :
f ≤ 0 ↔ 0 ∈ f
source
@[simp]
theorem filter.le_one_iff {α : Type u_2} [has_one α] {f : filter α} :
f ≤ 1 ↔ 1 ∈ f
source
@[protected]
theorem filter.ne_bot.le_one_iff {α : Type u_2} [has_one α] {f : filter α} (h : f.ne_bot) :
f ≤ 1 ↔ f = 1
source
@[protected]
theorem filter.ne_bot.nonpos_iff {α : Type u_2} [has_zero α] {f : filter α} (h : f.ne_bot) :
f ≤ 0 ↔ f = 0
source
@[simp]
theorem filter.eventually_one {α : Type u_2} [has_one α] {p : α → Prop} :
(∀ᶠ (x : α) in 1, p x) ↔ p 1
source
@[simp]
theorem filter.eventually_zero {α : Type u_2} [has_zero α] {p : α → Prop} :
(∀ᶠ (x : α) in 0, p x) ↔ p 0
source
@[simp]
theorem filter.tendsto_one {α : Type u_2} {β : Type u_3} [has_one α] {a : filter β} {f : β → α} :
filter.tendsto f a 1 ↔ ∀ᶠ (x : β) in a, f x = 1
source
@[simp]
theorem filter.tendsto_zero {α : Type u_2} {β : Type u_3} [has_zero α] {a : filter β} {f : β → α} :
filter.tendsto f a 0 ↔ ∀ᶠ (x : β) in a, f x = 0
source
@[simp]
theorem filter.one_prod_one {α : Type u_2} {β : Type u_3} [has_one α] [has_one β] :
1.prod 1 = 1
source
@[simp]
theorem filter.zero_sum_zero {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] :
0.prod 0 = 0
source
def filter.pure_zero_hom {α : Type u_2} [has_zero α] :
zero_hom α (filter α)

pure as a zero_hom.

Equations
source
def filter.pure_one_hom {α : Type u_2} [has_one α] :
one_hom α (filter α)

pure as a one_hom.

Equations
source
@[simp]
theorem filter.coe_pure_zero_hom {α : Type u_2} [has_zero α] :
⇑filter.pure_zero_hom = has_pure.pure
source
@[simp]
theorem filter.coe_pure_one_hom {α : Type u_2} [has_one α] :
⇑filter.pure_one_hom = has_pure.pure
source
@[simp]
theorem filter.pure_zero_hom_apply {α : Type u_2} [has_zero α] (a : α) :
⇑filter.pure_zero_hom a = has_pure.pure a
source
@[simp]
theorem filter.pure_one_hom_apply {α : Type u_2} [has_one α] (a : α) :
⇑filter.pure_one_hom a = has_pure.pure a
source
@[protected, simp]
theorem filter.map_one {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_one α] [has_one β] [one_hom_class F α β] (φ : F) :
filter.map ⇑φ 1 = 1
source
@[protected, simp]
theorem filter.map_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [zero_hom_class F α β] (φ : F) :
filter.map ⇑φ 0 = 0

Filter negation/inversion #

source
@[protected, instance]
def filter.has_inv {α : Type u_2} [has_inv α] :
has_inv (filter α)

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

Equations
source
@[protected, instance]
def filter.has_neg {α : Type u_2} [has_neg α] :
has_neg (filter α)

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

Equations
source
@[protected, simp]
theorem filter.map_neg {α : Type u_2} [has_neg α] {f : filter α} :
filter.map has_neg.neg f = -f
source
@[protected, simp]
theorem filter.map_inv {α : Type u_2} [has_inv α] {f : filter α} :
filter.map has_inv.inv f = f⁻¹
source
theorem filter.mem_inv {α : Type u_2} [has_inv α] {f : filter α} {s : set α} :
s ∈ f⁻¹ ↔ has_inv.inv ⁻¹' s ∈ f
source
theorem filter.mem_neg {α : Type u_2} [has_neg α] {f : filter α} {s : set α} :
s ∈ -f ↔ has_neg.neg ⁻¹' s ∈ f
source
@[protected]
theorem filter.neg_le_neg {α : Type u_2} [has_neg α] {f g : filter α} (hf : f ≤ g) :
-f ≤ -g
source
@[protected]
theorem filter.inv_le_inv {α : Type u_2} [has_inv α] {f g : filter α} (hf : f ≤ g) :
f⁻¹ ≤ g⁻¹
source
@[simp]
theorem filter.inv_pure {α : Type u_2} [has_inv α] {a : α} :
(has_pure.pure a)⁻¹ = has_pure.pure a⁻¹
source
@[simp]
theorem filter.neg_pure {α : Type u_2} [has_neg α] {a : α} :
-has_pure.pure a = has_pure.pure (-a)
source
@[simp]
theorem filter.neg_eq_bot_iff {α : Type u_2} [has_neg α] {f : filter α} :
-f = ⊥ ↔ f = ⊥
source
@[simp]
theorem filter.inv_eq_bot_iff {α : Type u_2} [has_inv α] {f : filter α} :
f⁻¹ = ⊥ ↔ f = ⊥
source
@[simp]
theorem filter.ne_bot_inv_iff {α : Type u_2} [has_inv α] {f : filter α} :
f⁻¹.ne_bot ↔ f.ne_bot
source
@[simp]
theorem filter.ne_bot_neg_iff {α : Type u_2} [has_neg α] {f : filter α} :
(-f).ne_bot ↔ f.ne_bot
source
theorem filter.ne_bot.neg {α : Type u_2} [has_neg α] {f : filter α} :
f.ne_bot → (-f).ne_bot
source
theorem filter.ne_bot.inv {α : Type u_2} [has_inv α] {f : filter α} :
f.ne_bot → f⁻¹.ne_bot
source
theorem filter.neg_mem_neg {α : Type u_2} [has_involutive_neg α] {f : filter α} {s : set α} (hs : s ∈ f) :
-s ∈ -f
source
theorem filter.inv_mem_inv {α : Type u_2} [has_involutive_inv α] {f : filter α} {s : set α} (hs : s ∈ f) :
s⁻¹ ∈ f⁻¹
source
@[protected]
def filter.has_involutive_neg {α : Type u_2} [has_involutive_neg α] :
has_involutive_neg (filter α)

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

Equations
source
@[protected]
def filter.has_involutive_inv {α : Type u_2} [has_involutive_inv α] :
has_involutive_inv (filter α)

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

Equations
source
@[protected, simp]
theorem filter.neg_le_neg_iff {α : Type u_2} [has_involutive_neg α] {f g : filter α} :
-f ≤ -g ↔ f ≤ g
source
@[protected, simp]
theorem filter.inv_le_inv_iff {α : Type u_2} [has_involutive_inv α] {f g : filter α} :
f⁻¹ ≤ g⁻¹ ↔ f ≤ g
source
theorem filter.inv_le_iff_le_inv {α : Type u_2} [has_involutive_inv α] {f g : filter α} :
f⁻¹ ≤ g ↔ f ≤ g⁻¹
source
theorem filter.neg_le_iff_le_neg {α : Type u_2} [has_involutive_neg α] {f g : filter α} :
-f ≤ g ↔ f ≤ -g
source
@[simp]
theorem filter.inv_le_self {α : Type u_2} [has_involutive_inv α] {f : filter α} :
f⁻¹ ≤ f ↔ f⁻¹ = f
source
@[simp]
theorem filter.neg_le_self {α : Type u_2} [has_involutive_neg α] {f : filter α} :
-f ≤ f ↔ -f = f

Filter addition/multiplication #

source
@[protected]
def filter.has_add {α : Type u_2} [has_add α] :
has_add (filter α)

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

Equations
source
@[protected]
def filter.has_mul {α : Type u_2} [has_mul α] :
has_mul (filter α)

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

Equations
source
@[simp]
theorem filter.map₂_mul {α : Type u_2} [has_mul α] {f g : filter α} :
filter.map₂ has_mul.mul f g = f * g
source
@[simp]
theorem filter.map₂_add {α : Type u_2} [has_add α] {f g : filter α} :
filter.map₂ has_add.add f g = f + g
source
theorem filter.mem_mul {α : Type u_2} [has_mul α] {f g : filter α} {s : set α} :
s ∈ f * g ↔ ∃ (t₁ t₂ : set α), t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ * t₂ ⊆ s
source
theorem filter.mem_add {α : Type u_2} [has_add α] {f g : filter α} {s : set α} :
s ∈ f + g ↔ ∃ (t₁ t₂ : set α), t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ + t₂ ⊆ s
source
theorem filter.mul_mem_mul {α : Type u_2} [has_mul α] {f g : filter α} {s t : set α} :
s ∈ f → t ∈ g → s * t ∈ f * g
source
theorem filter.add_mem_add {α : Type u_2} [has_add α] {f g : filter α} {s t : set α} :
s ∈ f → t ∈ g → s + t ∈ f + g
source
@[simp]
theorem filter.bot_add {α : Type u_2} [has_add α] {g : filter α} :
⊥ + g = ⊥
source
@[simp]
theorem filter.bot_mul {α : Type u_2} [has_mul α] {g : filter α} :
⊥ * g = ⊥
source
@[simp]
theorem filter.add_bot {α : Type u_2} [has_add α] {f : filter α} :
f + ⊥ = ⊥
source
@[simp]
theorem filter.mul_bot {α : Type u_2} [has_mul α] {f : filter α} :
f * ⊥ = ⊥
source
@[simp]
theorem filter.add_eq_bot_iff {α : Type u_2} [has_add α] {f g : filter α} :
f + g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem filter.mul_eq_bot_iff {α : Type u_2} [has_mul α] {f g : filter α} :
f * g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem filter.mul_ne_bot_iff {α : Type u_2} [has_mul α] {f g : filter α} :
(f * g).ne_bot ↔ f.ne_bot ∧ g.ne_bot
source
@[simp]
theorem filter.add_ne_bot_iff {α : Type u_2} [has_add α] {f g : filter α} :
(f + g).ne_bot ↔ f.ne_bot ∧ g.ne_bot
source
theorem filter.ne_bot.mul {α : Type u_2} [has_mul α] {f g : filter α} :
f.ne_bot → g.ne_bot → (f * g).ne_bot
source
theorem filter.ne_bot.add {α : Type u_2} [has_add α] {f g : filter α} :
f.ne_bot → g.ne_bot → (f + g).ne_bot
source
theorem filter.ne_bot.of_add_left {α : Type u_2} [has_add α] {f g : filter α} :
(f + g).ne_bot → f.ne_bot
source
theorem filter.ne_bot.of_mul_left {α : Type u_2} [has_mul α] {f g : filter α} :
(f * g).ne_bot → f.ne_bot
source
theorem filter.ne_bot.of_add_right {α : Type u_2} [has_add α] {f g : filter α} :
(f + g).ne_bot → g.ne_bot
source
theorem filter.ne_bot.of_mul_right {α : Type u_2} [has_mul α] {f g : filter α} :
(f * g).ne_bot → g.ne_bot
source
@[simp]
theorem filter.pure_mul {α : Type u_2} [has_mul α] {g : filter α} {a : α} :
has_pure.pure a * g = filter.map (has_mul.mul a) g
source
@[simp]
theorem filter.pure_add {α : Type u_2} [has_add α] {g : filter α} {a : α} :
has_pure.pure a + g = filter.map (has_add.add a) g
source
@[simp]
theorem filter.add_pure {α : Type u_2} [has_add α] {f : filter α} {b : α} :
f + has_pure.pure b = filter.map (λ (_x : α), _x + b) f
source
@[simp]
theorem filter.mul_pure {α : Type u_2} [has_mul α] {f : filter α} {b : α} :
f * has_pure.pure b = filter.map (λ (_x : α), _x * b) f
source
@[simp]
theorem filter.pure_mul_pure {α : Type u_2} [has_mul α] {a b : α} :
has_pure.pure a * has_pure.pure b = has_pure.pure (a * b)
source
@[simp]
theorem filter.pure_add_pure {α : Type u_2} [has_add α] {a b : α} :
has_pure.pure a + has_pure.pure b = has_pure.pure (a + b)
source
@[simp]
theorem filter.le_mul_iff {α : Type u_2} [has_mul α] {f g h : filter α} :
h ≤ f * g ↔ ∀ ⦃s : set α⦄, s ∈ f → ∀ ⦃t : set α⦄, t ∈ g → s * t ∈ h
source
@[simp]
theorem filter.le_add_iff {α : Type u_2} [has_add α] {f g h : filter α} :
h ≤ f + g ↔ ∀ ⦃s : set α⦄, s ∈ f → ∀ ⦃t : set α⦄, t ∈ g → s + t ∈ h
source
@[protected, instance]
def filter.covariant_add {α : Type u_2} [has_add α] :
covariant_class (filter α) (filter α) has_add.add has_le.le
source
@[protected, instance]
def filter.covariant_mul {α : Type u_2} [has_mul α] :
covariant_class (filter α) (filter α) has_mul.mul has_le.le
source
@[protected, instance]
def filter.covariant_swap_add {α : Type u_2} [has_add α] :
covariant_class (filter α) (filter α) (function.swap has_add.add) has_le.le
source
@[protected, instance]
def filter.covariant_swap_mul {α : Type u_2} [has_mul α] :
covariant_class (filter α) (filter α) (function.swap has_mul.mul) has_le.le
source
@[protected]
theorem filter.map_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_mul β] {f₁ f₂ : filter α} [mul_hom_class F α β] (m : F) :
filter.map ⇑m (f₁ * f₂) = filter.map ⇑m f₁ * filter.map ⇑m f₂
source
@[protected]
theorem filter.map_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_add α] [has_add β] {f₁ f₂ : filter α} [add_hom_class F α β] (m : F) :
filter.map ⇑m (f₁ + f₂) = filter.map ⇑m f₁ + filter.map ⇑m f₂
source
def filter.pure_add_hom {α : Type u_2} [has_add α] :
add_hom α (filter α)

The singleton operation as an add_hom.

Equations
source
def filter.pure_mul_hom {α : Type u_2} [has_mul α] :
α →ₙ* filter α

pure operation as a mul_hom.

Equations
source
@[simp]
theorem filter.coe_pure_add_hom {α : Type u_2} [has_add α] :
⇑filter.pure_add_hom = has_pure.pure
source
@[simp]
theorem filter.coe_pure_mul_hom {α : Type u_2} [has_mul α] :
⇑filter.pure_mul_hom = has_pure.pure
source
@[simp]
theorem filter.pure_mul_hom_apply {α : Type u_2} [has_mul α] (a : α) :
⇑filter.pure_mul_hom a = has_pure.pure a
source
@[simp]
theorem filter.pure_add_hom_apply {α : Type u_2} [has_add α] (a : α) :
⇑filter.pure_add_hom a = has_pure.pure a

Filter subtraction/division #

source
@[protected]
def filter.has_sub {α : Type u_2} [has_sub α] :
has_sub (filter α)

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

Equations
source
@[protected]
def filter.has_div {α : Type u_2} [has_div α] :
has_div (filter α)

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

Equations
source
@[simp]
theorem filter.map₂_sub {α : Type u_2} [has_sub α] {f g : filter α} :
filter.map₂ has_sub.sub f g = f - g
source
@[simp]
theorem filter.map₂_div {α : Type u_2} [has_div α] {f g : filter α} :
filter.map₂ has_div.div f g = f / g
source
theorem filter.mem_sub {α : Type u_2} [has_sub α] {f g : filter α} {s : set α} :
s ∈ f - g ↔ ∃ (t₁ t₂ : set α), t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ - t₂ ⊆ s
source
theorem filter.mem_div {α : Type u_2} [has_div α] {f g : filter α} {s : set α} :
s ∈ f / g ↔ ∃ (t₁ t₂ : set α), t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ / t₂ ⊆ s
source
theorem filter.div_mem_div {α : Type u_2} [has_div α] {f g : filter α} {s t : set α} :
s ∈ f → t ∈ g → s / t ∈ f / g
source
theorem filter.sub_mem_sub {α : Type u_2} [has_sub α] {f g : filter α} {s t : set α} :
s ∈ f → t ∈ g → s - t ∈ f - g
source
@[simp]
theorem filter.bot_sub {α : Type u_2} [has_sub α] {g : filter α} :
⊥ - g = ⊥
source
@[simp]
theorem filter.bot_div {α : Type u_2} [has_div α] {g : filter α} :
⊥ / g = ⊥
source
@[simp]
theorem filter.div_bot {α : Type u_2} [has_div α] {f : filter α} :
f / ⊥ = ⊥
source
@[simp]
theorem filter.sub_bot {α : Type u_2} [has_sub α] {f : filter α} :
f - ⊥ = ⊥
source
@[simp]
theorem filter.sub_eq_bot_iff {α : Type u_2} [has_sub α] {f g : filter α} :
f - g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem filter.div_eq_bot_iff {α : Type u_2} [has_div α] {f g : filter α} :
f / g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem filter.div_ne_bot_iff {α : Type u_2} [has_div α] {f g : filter α} :
(f / g).ne_bot ↔ f.ne_bot ∧ g.ne_bot
source
@[simp]
theorem filter.sub_ne_bot_iff {α : Type u_2} [has_sub α] {f g : filter α} :
(f - g).ne_bot ↔ f.ne_bot ∧ g.ne_bot
source
theorem filter.ne_bot.sub {α : Type u_2} [has_sub α] {f g : filter α} :
f.ne_bot → g.ne_bot → (f - g).ne_bot
source
theorem filter.ne_bot.div {α : Type u_2} [has_div α] {f g : filter α} :
f.ne_bot → g.ne_bot → (f / g).ne_bot
source
theorem filter.ne_bot.of_div_left {α : Type u_2} [has_div α] {f g : filter α} :
(f / g).ne_bot → f.ne_bot
source
theorem filter.ne_bot.of_sub_left {α : Type u_2} [has_sub α] {f g : filter α} :
(f - g).ne_bot → f.ne_bot
source
theorem filter.ne_bot.of_div_right {α : Type u_2} [has_div α] {f g : filter α} :
(f / g).ne_bot → g.ne_bot
source
theorem filter.ne_bot.of_sub_right {α : Type u_2} [has_sub α] {f g : filter α} :
(f - g).ne_bot → g.ne_bot
source
@[simp]
theorem filter.pure_div {α : Type u_2} [has_div α] {g : filter α} {a : α} :
has_pure.pure a / g = filter.map (has_div.div a) g
source
@[simp]
theorem filter.pure_sub {α : Type u_2} [has_sub α] {g : filter α} {a : α} :
has_pure.pure a - g = filter.map (has_sub.sub a) g
source
@[simp]
theorem filter.div_pure {α : Type u_2} [has_div α] {f : filter α} {b : α} :
f / has_pure.pure b = filter.map (λ (_x : α), _x / b) f
source
@[simp]
theorem filter.sub_pure {α : Type u_2} [has_sub α] {f : filter α} {b : α} :
f - has_pure.pure b = filter.map (λ (_x : α), _x - b) f
source
@[simp]
theorem filter.pure_sub_pure {α : Type u_2} [has_sub α] {a b : α} :
has_pure.pure a - has_pure.pure b = has_pure.pure (a - b)
source
@[simp]
theorem filter.pure_div_pure {α : Type u_2} [has_div α] {a b : α} :
has_pure.pure a / has_pure.pure b = has_pure.pure (a / b)
source
@[protected]
theorem filter.div_le_div {α : Type u_2} [has_div α] {f₁ f₂ g₁ g₂ : filter α} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ / g₁ ≤ f₂ / g₂
source
@[protected]
theorem filter.sub_le_sub {α : Type u_2} [has_sub α] {f₁ f₂ g₁ g₂ : filter α} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ - g₁ ≤ f₂ - g₂
source
@[protected]
theorem filter.div_le_div_left {α : Type u_2} [has_div α] {f g₁ g₂ : filter α} :
g₁ ≤ g₂ → f / g₁ ≤ f / g₂
source
@[protected]
theorem filter.sub_le_sub_left {α : Type u_2} [has_sub α] {f g₁ g₂ : filter α} :
g₁ ≤ g₂ → f - g₁ ≤ f - g₂
source
@[protected]
theorem filter.div_le_div_right {α : Type u_2} [has_div α] {f₁ f₂ g : filter α} :
f₁ ≤ f₂ → f₁ / g ≤ f₂ / g
source
@[protected]
theorem filter.sub_le_sub_right {α : Type u_2} [has_sub α] {f₁ f₂ g : filter α} :
f₁ ≤ f₂ → f₁ - g ≤ f₂ - g
source
@[protected, simp]
theorem filter.le_sub_iff {α : Type u_2} [has_sub α] {f g h : filter α} :
h ≤ f - g ↔ ∀ ⦃s : set α⦄, s ∈ f → ∀ ⦃t : set α⦄, t ∈ g → s - t ∈ h
source
@[protected, simp]
theorem filter.le_div_iff {α : Type u_2} [has_div α] {f g h : filter α} :
h ≤ f / g ↔ ∀ ⦃s : set α⦄, s ∈ f → ∀ ⦃t : set α⦄, t ∈ g → s / t ∈ h
source
@[protected, instance]
def filter.covariant_sub {α : Type u_2} [has_sub α] :
covariant_class (filter α) (filter α) has_sub.sub has_le.le
source
@[protected, instance]
def filter.covariant_div {α : Type u_2} [has_div α] :
covariant_class (filter α) (filter α) has_div.div has_le.le
source
@[protected, instance]
def filter.covariant_swap_sub {α : Type u_2} [has_sub α] :
covariant_class (filter α) (filter α) (function.swap has_sub.sub) has_le.le
source
@[protected, instance]
def filter.covariant_swap_div {α : Type u_2} [has_div α] :
covariant_class (filter α) (filter α) (function.swap has_div.div) has_le.le
source
@[protected]
def filter.has_nsmul {α : Type u_2} [has_zero α] [has_add α] :
has_smul ℕ (filter α)

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

Equations
source
@[protected]
def filter.has_npow {α : Type u_2} [has_one α] [has_mul α] :
has_pow (filter α) ℕ

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

Equations
source
@[protected]
def filter.has_zsmul {α : Type u_2} [has_zero α] [has_add α] [has_neg α] :
has_smul ℤ (filter α)

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

Equations
source
@[protected]
def filter.has_zpow {α : Type u_2} [has_one α] [has_mul α] [has_inv α] :
has_pow (filter α) ℤ

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

Equations
source
@[protected]
def filter.semigroup {α : Type u_2} [semigroup α] :
semigroup (filter α)

filter α is a semigroup under pointwise operations if α is.

Equations
source
@[protected]
def filter.add_semigroup {α : Type u_2} [add_semigroup α] :
add_semigroup (filter α)

filter α is an add_semigroup under pointwise operations if α is.

Equations
source
@[protected]
def filter.comm_semigroup {α : Type u_2} [comm_semigroup α] :
comm_semigroup (filter α)

filter α is a comm_semigroup under pointwise operations if α is.

Equations
source
@[protected]
def filter.add_comm_semigroup {α : Type u_2} [add_comm_semigroup α] :
add_comm_semigroup (filter α)

filter α is an add_comm_semigroup under pointwise operations if α is.

Equations
source
@[protected]
def filter.add_zero_class {α : Type u_2} [add_zero_class α] :
add_zero_class (filter α)

filter α is an add_zero_class under pointwise operations if α is.

Equations
source
@[protected]
def filter.mul_one_class {α : Type u_2} [mul_one_class α] :
mul_one_class (filter α)

filter α is a mul_one_class under pointwise operations if α is.

Equations
source
def filter.map_add_monoid_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_zero_class α] [add_zero_class β] [add_monoid_hom_class F α β] (φ : F) :
filter α →+ filter β

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

Equations
source
def filter.map_monoid_hom {F : Type u_1} {α : Type u_2} {β : Type u_3} [mul_one_class α] [mul_one_class β] [monoid_hom_class F α β] (φ : F) :
filter α →* filter β

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

Equations
source
theorem filter.comap_add_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_zero_class α] [add_zero_class β] [add_hom_class F α β] (m : F) {f g : filter β} :
filter.comap ⇑m f + filter.comap ⇑m g ≤ filter.comap ⇑m (f + g)
source
theorem filter.comap_mul_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [mul_one_class α] [mul_one_class β] [mul_hom_class F α β] (m : F) {f g : filter β} :
filter.comap ⇑m f * filter.comap ⇑m g ≤ filter.comap ⇑m (f * g)
source
theorem filter.tendsto.add_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_zero_class α] [add_zero_class β] [add_hom_class F α β] (m : F) {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
filter.tendsto ⇑m f₁ f₂ → filter.tendsto ⇑m g₁ g₂ → filter.tendsto ⇑m (f₁ + g₁) (f₂ + g₂)
source
theorem filter.tendsto.mul_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [mul_one_class α] [mul_one_class β] [mul_hom_class F α β] (m : F) {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
filter.tendsto ⇑m f₁ f₂ → filter.tendsto ⇑m g₁ g₂ → filter.tendsto ⇑m (f₁ * g₁) (f₂ * g₂)
source
def filter.pure_monoid_hom {α : Type u_2} [mul_one_class α] :
α →* filter α

pure as a monoid_hom.

Equations
source
def filter.pure_add_monoid_hom {α : Type u_2} [add_zero_class α] :
α →+ filter α

pure as an add_monoid_hom.

Equations
source
@[simp]
theorem filter.coe_pure_add_monoid_hom {α : Type u_2} [add_zero_class α] :
⇑filter.pure_add_monoid_hom = has_pure.pure
source
@[simp]
theorem filter.coe_pure_monoid_hom {α : Type u_2} [mul_one_class α] :
⇑filter.pure_monoid_hom = has_pure.pure
source
@[simp]
theorem filter.pure_monoid_hom_apply {α : Type u_2} [mul_one_class α] (a : α) :
⇑filter.pure_monoid_hom a = has_pure.pure a
source
@[simp]
theorem filter.pure_add_monoid_hom_apply {α : Type u_2} [add_zero_class α] (a : α) :
⇑filter.pure_add_monoid_hom a = has_pure.pure a
source
@[protected]
def filter.add_monoid {α : Type u_2} [add_monoid α] :
add_monoid (filter α)

filter α is an add_monoid under pointwise operations if α is.

Equations
source
@[protected]
def filter.monoid {α : Type u_2} [monoid α] :
monoid (filter α)

filter α is a monoid under pointwise operations if α is.

Equations
source
theorem filter.pow_mem_pow {α : Type u_2} [monoid α] {f : filter α} {s : set α} (hs : s ∈ f) (n : ℕ) :
s ^ n ∈ f ^ n
source
theorem filter.nsmul_mem_nsmul {α : Type u_2} [add_monoid α] {f : filter α} {s : set α} (hs : s ∈ f) (n : ℕ) :
n • s ∈ n • f
source
@[simp]
theorem filter.nsmul_bot {α : Type u_2} [add_monoid α] {n : ℕ} (hn : n ≠ 0) :
n • ⊥ = ⊥
source
@[simp]
theorem filter.bot_pow {α : Type u_2} [monoid α] {n : ℕ} (hn : n ≠ 0) :
⊥ ^ n = ⊥
source
theorem filter.mul_top_of_one_le {α : Type u_2} [monoid α] {f : filter α} (hf : 1 ≤ f) :
f * ⊤ = ⊤
source
theorem filter.add_top_of_nonneg {α : Type u_2} [add_monoid α] {f : filter α} (hf : 0 ≤ f) :
f + ⊤ = ⊤
source
theorem filter.top_mul_of_one_le {α : Type u_2} [monoid α] {f : filter α} (hf : 1 ≤ f) :
⊤ * f = ⊤
source
theorem filter.top_add_of_nonneg {α : Type u_2} [add_monoid α] {f : filter α} (hf : 0 ≤ f) :
⊤ + f = ⊤
source
@[simp]
theorem filter.top_mul_top {α : Type u_2} [monoid α] :
⊤ * ⊤ = ⊤
source
@[simp]
theorem filter.top_add_top {α : Type u_2} [add_monoid α] :
⊤ + ⊤ = ⊤
source
theorem filter.nsmul_top {α : Type u_1} [add_monoid α] {n : ℕ} :
n ≠ 0 → n • ⊤ = ⊤
source
theorem filter.top_pow {α : Type u_2} [monoid α] {n : ℕ} :
n ≠ 0 → ⊤ ^ n = ⊤
source
@[protected]
theorem is_unit.filter {α : Type u_2} [monoid α] {a : α} :
is_unit a → is_unit (has_pure.pure a)
source
@[protected]
theorem is_add_unit.filter {α : Type u_2} [add_monoid α] {a : α} :
is_add_unit a → is_add_unit (has_pure.pure a)
source
@[protected]
def filter.comm_monoid {α : Type u_2} [comm_monoid α] :
comm_monoid (filter α)

filter α is a comm_monoid under pointwise operations if α is.

Equations
source
@[protected]
def filter.add_comm_monoid {α : Type u_2} [add_comm_monoid α] :
add_comm_monoid (filter α)

filter α is an add_comm_monoid under pointwise operations if α is.

Equations
source
@[protected]
theorem filter.mul_eq_one_iff {α : Type u_2} [division_monoid α] {f g : filter α} :
f * g = 1 ↔ ∃ (a b : α), f = has_pure.pure a ∧ g = has_pure.pure b ∧ a * b = 1
source
@[protected]
theorem filter.add_eq_zero_iff {α : Type u_2} [subtraction_monoid α] {f g : filter α} :
f + g = 0 ↔ ∃ (a b : α), f = has_pure.pure a ∧ g = has_pure.pure b ∧ a + b = 0
source
@[protected]
def filter.division_monoid {α : Type u_2} [division_monoid α] :
division_monoid (filter α)

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

Equations
source
@[protected]
def filter.subtraction_monoid {α : Type u_2} [subtraction_monoid α] :
subtraction_monoid (filter α)

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

Equations
source
theorem filter.is_unit_iff {α : Type u_2} [division_monoid α] {f : filter α} :
is_unit f ↔ ∃ (a : α), f = has_pure.pure a ∧ is_unit a
source
theorem filter.is_add_unit_iff {α : Type u_2} [subtraction_monoid α] {f : filter α} :
is_add_unit f ↔ ∃ (a : α), f = has_pure.pure a ∧ is_add_unit a
source
@[protected]
def filter.division_comm_monoid {α : Type u_2} [division_comm_monoid α] :
division_comm_monoid (filter α)

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

Equations
source
@[protected]
def filter.subtraction_comm_monoid {α : Type u_2} [subtraction_comm_monoid α] :
subtraction_comm_monoid (filter α)

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

Equations
source
@[protected]
def filter.has_distrib_neg {α : Type u_2} [has_mul α] [has_distrib_neg α] :
has_distrib_neg (filter α)

filter α has distributive negation if α has.

Equations

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

source
theorem filter.mul_add_subset {α : Type u_2} [distrib α] {f g h : filter α} :
f * (g + h) ≤ f * g + f * h
source
theorem filter.add_mul_subset {α : Type u_2} [distrib α] {f g h : filter α} :
(f + g) * h ≤ f * h + g * h

Note that filter is not a mul_zero_class because 0 * ⊥ ≠ 0.

source
theorem filter.ne_bot.mul_zero_nonneg {α : Type u_2} [mul_zero_class α] {f : filter α} (hf : f.ne_bot) :
0 ≤ f * 0
source
theorem filter.ne_bot.zero_mul_nonneg {α : Type u_2} [mul_zero_class α] {g : filter α} (hg : g.ne_bot) :
0 ≤ 0 * g

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

source
@[protected, simp]
theorem filter.nonneg_sub_iff {α : Type u_2} [add_group α] {f g : filter α} :
0 ≤ f - g ↔ ¬disjoint f g
source
@[protected, simp]
theorem filter.one_le_div_iff {α : Type u_2} [group α] {f g : filter α} :
1 ≤ f / g ↔ ¬disjoint f g
source
theorem filter.not_nonneg_sub_iff {α : Type u_2} [add_group α] {f g : filter α} :
¬0 ≤ f - g ↔ disjoint f g
source
theorem filter.not_one_le_div_iff {α : Type u_2} [group α] {f g : filter α} :
¬1 ≤ f / g ↔ disjoint f g
source
theorem filter.ne_bot.one_le_div {α : Type u_2} [group α] {f : filter α} (h : f.ne_bot) :
1 ≤ f / f
source
theorem filter.ne_bot.nonneg_sub {α : Type u_2} [add_group α] {f : filter α} (h : f.ne_bot) :
0 ≤ f - f
source
theorem filter.is_unit_pure {α : Type u_2} [group α] (a : α) :
is_unit (has_pure.pure a)
source
theorem filter.is_add_unit_pure {α : Type u_2} [add_group α] (a : α) :
is_add_unit (has_pure.pure a)
source
@[simp]
theorem filter.is_unit_iff_singleton {α : Type u_2} [group α] {f : filter α} :
is_unit f ↔ ∃ (a : α), f = has_pure.pure a
source
theorem filter.map_neg' {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [subtraction_monoid β] [add_monoid_hom_class F α β] (m : F) {f : filter α} :
filter.map ⇑m (-f) = -filter.map ⇑m f
source
theorem filter.map_inv' {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [division_monoid β] [monoid_hom_class F α β] (m : F) {f : filter α} :
filter.map ⇑m f⁻¹ = (filter.map ⇑m f)⁻¹
source
theorem filter.tendsto.neg_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [subtraction_monoid β] [add_monoid_hom_class F α β] (m : F) {f₁ : filter α} {f₂ : filter β} :
filter.tendsto ⇑m f₁ f₂ → filter.tendsto ⇑m (-f₁) (-f₂)
source
theorem filter.tendsto.inv_inv {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [division_monoid β] [monoid_hom_class F α β] (m : F) {f₁ : filter α} {f₂ : filter β} :
filter.tendsto ⇑m f₁ f₂ → filter.tendsto ⇑m f₁⁻¹ f₂⁻¹
source
@[protected]
theorem filter.map_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [subtraction_monoid β] [add_monoid_hom_class F α β] (m : F) {f g : filter α} :
filter.map ⇑m (f - g) = filter.map ⇑m f - filter.map ⇑m g
source
@[protected]
theorem filter.map_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [division_monoid β] [monoid_hom_class F α β] (m : F) {f g : filter α} :
filter.map ⇑m (f / g) = filter.map ⇑m f / filter.map ⇑m g
source
theorem filter.tendsto.div_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [division_monoid β] [monoid_hom_class F α β] (m : F) {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
filter.tendsto ⇑m f₁ f₂ → filter.tendsto ⇑m g₁ g₂ → filter.tendsto ⇑m (f₁ / g₁) (f₂ / g₂)
source
theorem filter.tendsto.sub_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [subtraction_monoid β] [add_monoid_hom_class F α β] (m : F) {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
filter.tendsto ⇑m f₁ f₂ → filter.tendsto ⇑m g₁ g₂ → filter.tendsto ⇑m (f₁ - g₁) (f₂ - g₂)
source
theorem filter.ne_bot.div_zero_nonneg {α : Type u_2} [group_with_zero α] {f : filter α} (hf : f.ne_bot) :
0 ≤ f / 0
source
theorem filter.ne_bot.zero_div_nonneg {α : Type u_2} [group_with_zero α] {g : filter α} (hg : g.ne_bot) :
0 ≤ 0 / g

Scalar addition/multiplication of filters #

source
@[protected]
def filter.has_smul {α : Type u_2} {β : Type u_3} [has_smul α β] :
has_smul (filter α) (filter β)

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

Equations
source
@[protected]
def filter.has_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] :
has_vadd (filter α) (filter β)

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

Equations
source
@[simp]
theorem filter.map₂_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g : filter β} :
filter.map₂ has_smul.smul f g = f • g
source
@[simp]
theorem filter.map₂_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g : filter β} :
filter.map₂ has_vadd.vadd f g = f +ᵥ g
source
theorem filter.mem_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g : filter β} {t : set β} :
t ∈ f • g ↔ ∃ (t₁ : set α) (t₂ : set β), t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ • t₂ ⊆ t
source
theorem filter.mem_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g : filter β} {t : set β} :
t ∈ f +ᵥ g ↔ ∃ (t₁ : set α) (t₂ : set β), t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ +ᵥ t₂ ⊆ t
source
theorem filter.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g : filter β} {s : set α} {t : set β} :
s ∈ f → t ∈ g → s +ᵥ t ∈ f +ᵥ g
source
theorem filter.smul_mem_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g : filter β} {s : set α} {t : set β} :
s ∈ f → t ∈ g → s • t ∈ f • g
source
@[simp]
theorem filter.bot_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {g : filter β} :
⊥ • g = ⊥
source
@[simp]
theorem filter.bot_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {g : filter β} :
⊥ +ᵥ g = ⊥
source
@[simp]
theorem filter.vadd_bot {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} :
f +ᵥ ⊥ = ⊥
source
@[simp]
theorem filter.smul_bot {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} :
f • ⊥ = ⊥
source
@[simp]
theorem filter.smul_eq_bot_iff {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g : filter β} :
f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem filter.vadd_eq_bot_iff {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g : filter β} :
f +ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem filter.smul_ne_bot_iff {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g : filter β} :
(f • g).ne_bot ↔ f.ne_bot ∧ g.ne_bot
source
@[simp]
theorem filter.vadd_ne_bot_iff {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g : filter β} :
(f +ᵥ g).ne_bot ↔ f.ne_bot ∧ g.ne_bot
source
theorem filter.ne_bot.smul {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g : filter β} :
f.ne_bot → g.ne_bot → (f • g).ne_bot
source
theorem filter.ne_bot.vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g : filter β} :
f.ne_bot → g.ne_bot → (f +ᵥ g).ne_bot
source
theorem filter.ne_bot.of_smul_left {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g : filter β} :
(f • g).ne_bot → f.ne_bot
source
theorem filter.ne_bot.of_vadd_left {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g : filter β} :
(f +ᵥ g).ne_bot → f.ne_bot
source
theorem filter.ne_bot.of_vadd_right {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g : filter β} :
(f +ᵥ g).ne_bot → g.ne_bot
source
theorem filter.ne_bot.of_smul_right {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g : filter β} :
(f • g).ne_bot → g.ne_bot
source
@[simp]
theorem filter.pure_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {g : filter β} {a : α} :
has_pure.pure a +ᵥ g = filter.map (has_vadd.vadd a) g
source
@[simp]
theorem filter.pure_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {g : filter β} {a : α} :
has_pure.pure a • g = filter.map (has_smul.smul a) g
source
@[simp]
theorem filter.smul_pure {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {b : β} :
f • has_pure.pure b = filter.map (λ (_x : α), _x • b) f
source
@[simp]
theorem filter.vadd_pure {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {b : β} :
f +ᵥ has_pure.pure b = filter.map (λ (_x : α), _x +ᵥ b) f
source
@[simp]
theorem filter.pure_vadd_pure {α : Type u_2} {β : Type u_3} [has_vadd α β] {a : α} {b : β} :
has_pure.pure a +ᵥ has_pure.pure b = has_pure.pure (a +ᵥ b)
source
@[simp]
theorem filter.pure_smul_pure {α : Type u_2} {β : Type u_3} [has_smul α β] {a : α} {b : β} :
has_pure.pure a • has_pure.pure b = has_pure.pure (a • b)
source
theorem filter.smul_le_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {f₁ f₂ : filter α} {g₁ g₂ : filter β} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ • g₁ ≤ f₂ • g₂
source
theorem filter.vadd_le_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {f₁ f₂ : filter α} {g₁ g₂ : filter β} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ +ᵥ g₁ ≤ f₂ +ᵥ g₂
source
theorem filter.vadd_le_vadd_left {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g₁ g₂ : filter β} :
g₁ ≤ g₂ → f +ᵥ g₁ ≤ f +ᵥ g₂
source
theorem filter.smul_le_smul_left {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g₁ g₂ : filter β} :
g₁ ≤ g₂ → f • g₁ ≤ f • g₂
source
theorem filter.smul_le_smul_right {α : Type u_2} {β : Type u_3} [has_smul α β] {f₁ f₂ : filter α} {g : filter β} :
f₁ ≤ f₂ → f₁ • g ≤ f₂ • g
source
theorem filter.vadd_le_vadd_right {α : Type u_2} {β : Type u_3} [has_vadd α β] {f₁ f₂ : filter α} {g : filter β} :
f₁ ≤ f₂ → f₁ +ᵥ g ≤ f₂ +ᵥ g
source
@[simp]
theorem filter.le_vadd_iff {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter α} {g h : filter β} :
h ≤ f +ᵥ g ↔ ∀ ⦃s : set α⦄, s ∈ f → ∀ ⦃t : set β⦄, t ∈ g → s +ᵥ t ∈ h
source
@[simp]
theorem filter.le_smul_iff {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter α} {g h : filter β} :
h ≤ f • g ↔ ∀ ⦃s : set α⦄, s ∈ f → ∀ ⦃t : set β⦄, t ∈ g → s • t ∈ h
source
@[protected, instance]
def filter.covariant_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] :
covariant_class (filter α) (filter β) has_vadd.vadd has_le.le
source
@[protected, instance]
def filter.covariant_smul {α : Type u_2} {β : Type u_3} [has_smul α β] :
covariant_class (filter α) (filter β) has_smul.smul has_le.le

Scalar subtraction of filters #

source
@[protected]
def filter.has_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] :
has_vsub (filter α) (filter β)

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

Equations
source
@[simp]
theorem filter.map₂_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g : filter β} :
filter.map₂ has_vsub.vsub f g = f -ᵥ g
source
theorem filter.mem_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g : filter β} {s : set α} :
s ∈ f -ᵥ g ↔ ∃ (t₁ t₂ : set β), t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ -ᵥ t₂ ⊆ s
source
theorem filter.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g : filter β} {s t : set β} :
s ∈ f → t ∈ g → s -ᵥ t ∈ f -ᵥ g
source
@[simp]
theorem filter.bot_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {g : filter β} :
⊥ -ᵥ g = ⊥
source
@[simp]
theorem filter.vsub_bot {α : Type u_2} {β : Type u_3} [has_vsub α β] {f : filter β} :
f -ᵥ ⊥ = ⊥
source
@[simp]
theorem filter.vsub_eq_bot_iff {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g : filter β} :
f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
@[simp]
theorem filter.vsub_ne_bot_iff {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g : filter β} :
(f -ᵥ g).ne_bot ↔ f.ne_bot ∧ g.ne_bot
source
theorem filter.ne_bot.vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g : filter β} :
f.ne_bot → g.ne_bot → (f -ᵥ g).ne_bot
source
theorem filter.ne_bot.of_vsub_left {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g : filter β} :
(f -ᵥ g).ne_bot → f.ne_bot
source
theorem filter.ne_bot.of_vsub_right {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g : filter β} :
(f -ᵥ g).ne_bot → g.ne_bot
source
@[simp]
theorem filter.pure_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {g : filter β} {a : β} :
has_pure.pure a -ᵥ g = filter.map (has_vsub.vsub a) g
source
@[simp]
theorem filter.vsub_pure {α : Type u_2} {β : Type u_3} [has_vsub α β] {f : filter β} {b : β} :
f -ᵥ has_pure.pure b = filter.map (λ (_x : β), _x -ᵥ b) f
source
@[simp]
theorem filter.pure_vsub_pure {α : Type u_2} {β : Type u_3} [has_vsub α β] {a b : β} :
has_pure.pure a -ᵥ has_pure.pure b = has_pure.pure (a -ᵥ b)
source
theorem filter.vsub_le_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {f₁ f₂ g₁ g₂ : filter β} :
f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ -ᵥ g₁ ≤ f₂ -ᵥ g₂
source
theorem filter.vsub_le_vsub_left {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g₁ g₂ : filter β} :
g₁ ≤ g₂ → f -ᵥ g₁ ≤ f -ᵥ g₂
source
theorem filter.vsub_le_vsub_right {α : Type u_2} {β : Type u_3} [has_vsub α β] {f₁ f₂ g : filter β} :
f₁ ≤ f₂ → f₁ -ᵥ g ≤ f₂ -ᵥ g
source
@[simp]
theorem filter.le_vsub_iff {α : Type u_2} {β : Type u_3} [has_vsub α β] {f g : filter β} {h : filter α} :
h ≤ f -ᵥ g ↔ ∀ ⦃s : set β⦄, s ∈ f → ∀ ⦃t : set β⦄, t ∈ g → s -ᵥ t ∈ h

Translation/scaling of filters #

source
@[protected]
def filter.has_smul_filter {α : Type u_2} {β : Type u_3} [has_smul α β] :
has_smul α (filter β)

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

Equations
source
@[protected]
def filter.has_vadd_filter {α : Type u_2} {β : Type u_3} [has_vadd α β] :
has_vadd α (filter β)

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

Equations
source
@[simp]
theorem filter.map_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter β} {a : α} :
filter.map (λ (b : β), a • b) f = a • f
source
@[simp]
theorem filter.map_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter β} {a : α} :
filter.map (λ (b : β), a +ᵥ b) f = a +ᵥ f
source
theorem filter.mem_smul_filter {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter β} {s : set β} {a : α} :
s ∈ a • f ↔ has_smul.smul a ⁻¹' s ∈ f
source
theorem filter.mem_vadd_filter {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter β} {s : set β} {a : α} :
s ∈ a +ᵥ f ↔ has_vadd.vadd a ⁻¹' s ∈ f
source
theorem filter.vadd_set_mem_vadd_filter {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter β} {s : set β} {a : α} :
s ∈ f → a +ᵥ s ∈ a +ᵥ f
source
theorem filter.smul_set_mem_smul_filter {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter β} {s : set β} {a : α} :
s ∈ f → a • s ∈ a • f
source
@[simp]
theorem filter.smul_filter_bot {α : Type u_2} {β : Type u_3} [has_smul α β] {a : α} :
a • ⊥ = ⊥
source
@[simp]
theorem filter.vadd_filter_bot {α : Type u_2} {β : Type u_3} [has_vadd α β] {a : α} :
a +ᵥ ⊥ = ⊥
source
@[simp]
theorem filter.vadd_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter β} {a : α} :
a +ᵥ f = ⊥ ↔ f = ⊥
source
@[simp]
theorem filter.smul_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter β} {a : α} :
a • f = ⊥ ↔ f = ⊥
source
@[simp]
theorem filter.smul_filter_ne_bot_iff {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter β} {a : α} :
(a • f).ne_bot ↔ f.ne_bot
source
@[simp]
theorem filter.vadd_filter_ne_bot_iff {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter β} {a : α} :
(a +ᵥ f).ne_bot ↔ f.ne_bot
source
theorem filter.ne_bot.vadd_filter {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter β} {a : α} :
f.ne_bot → (a +ᵥ f).ne_bot
source
theorem filter.ne_bot.smul_filter {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter β} {a : α} :
f.ne_bot → (a • f).ne_bot
source
theorem filter.ne_bot.of_smul_filter {α : Type u_2} {β : Type u_3} [has_smul α β] {f : filter β} {a : α} :
(a • f).ne_bot → f.ne_bot
source
theorem filter.ne_bot.of_vadd_filter {α : Type u_2} {β : Type u_3} [has_vadd α β] {f : filter β} {a : α} :
(a +ᵥ f).ne_bot → f.ne_bot
source
theorem filter.smul_filter_le_smul_filter {α : Type u_2} {β : Type u_3} [has_smul α β] {f₁ f₂ : filter β} {a : α} (hf : f₁ ≤ f₂) :
a • f₁ ≤ a • f₂
source
theorem filter.vadd_filter_le_vadd_filter {α : Type u_2} {β : Type u_3} [has_vadd α β] {f₁ f₂ : filter β} {a : α} (hf : f₁ ≤ f₂) :
a +ᵥ f₁ ≤ a +ᵥ f₂
source
@[protected, instance]
def filter.covariant_smul_filter {α : Type u_2} {β : Type u_3} [has_smul α β] :
covariant_class α (filter β) has_smul.smul has_le.le
source
@[protected, instance]
def filter.covariant_vadd_filter {α : Type u_2} {β : Type u_3} [has_vadd α β] :
covariant_class α (filter β) has_vadd.vadd has_le.le
source
@[protected, instance]
def filter.smul_comm_class_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class α β (filter γ)
source
@[protected, instance]
def filter.vadd_comm_class_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class α β (filter γ)
source
@[protected, instance]
def filter.smul_comm_class_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class α (filter β) (filter γ)
source
@[protected, instance]
def filter.vadd_comm_class_filter' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class α (filter β) (filter γ)
source
@[protected, instance]
def filter.vadd_comm_class_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class (filter α) β (filter γ)
source
@[protected, instance]
def filter.smul_comm_class_filter'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class (filter α) β (filter γ)
source
@[protected, instance]
def filter.vadd_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class (filter α) (filter β) (filter γ)
source
@[protected, instance]
def filter.smul_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class (filter α) (filter β) (filter γ)
source
@[protected, instance]
def filter.vadd_assoc_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
vadd_assoc_class α β (filter γ)
source
@[protected, instance]
def filter.is_scalar_tower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
is_scalar_tower α β (filter γ)
source
@[protected, instance]
def filter.vadd_assoc_class' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
vadd_assoc_class α (filter β) (filter γ)
source
@[protected, instance]
def filter.is_scalar_tower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
is_scalar_tower α (filter β) (filter γ)
source
@[protected, instance]
def filter.vadd_assoc_class'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
vadd_assoc_class (filter α) (filter β) (filter γ)
source
@[protected, instance]
def filter.is_scalar_tower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
is_scalar_tower (filter α) (filter β) (filter γ)
source
@[protected, instance]
def filter.is_central_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] [has_vadd αᵃᵒᵖ β] [is_central_vadd α β] :
is_central_vadd α (filter β)
source
@[protected, instance]
def filter.is_central_scalar {α : Type u_2} {β : Type u_3} [has_smul α β] [has_smul αᵐᵒᵖ β] [is_central_scalar α β] :
is_central_scalar α (filter β)
source
@[protected]
def filter.add_action {α : Type u_2} {β : Type u_3} [add_monoid α] [add_action α β] :
add_action (filter α) (filter β)

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

Equations
source
@[protected]
def filter.mul_action {α : Type u_2} {β : Type u_3} [monoid α] [mul_action α β] :
mul_action (filter α) (filter β)

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

Equations
source
@[protected]
def filter.mul_action_filter {α : Type u_2} {β : Type u_3} [monoid α] [mul_action α β] :
mul_action α (filter β)

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

Equations
source
@[protected]
def filter.add_action_filter {α : Type u_2} {β : Type u_3} [add_monoid α] [add_action α β] :
add_action α (filter β)

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

Equations
source
@[protected]
def filter.distrib_mul_action_filter {α : Type u_2} {β : Type u_3} [monoid α] [add_monoid β] [distrib_mul_action α β] :
distrib_mul_action α (filter β)

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

Equations
source
@[protected]
def filter.mul_distrib_mul_action_filter {α : Type u_2} {β : Type u_3} [monoid α] [monoid β] [mul_distrib_mul_action α β] :
mul_distrib_mul_action α (set β)

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

Equations

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

source
theorem filter.ne_bot.smul_zero_nonneg {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {f : filter α} (hf : f.ne_bot) :
0 ≤ f • 0
source
theorem filter.ne_bot.zero_smul_nonneg {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {g : filter β} (hg : g.ne_bot) :
0 ≤ 0 • g
source
theorem filter.zero_smul_filter_nonpos {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {g : filter β} :
0 • g ≤ 0
source
theorem filter.zero_smul_filter {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {g : filter β} (hg : g.ne_bot) :
0 • g = 0