Pointwise operations on filters.
The pointwise operations on filters have nice properties, such as
• map m (f₁ * f₂) = map m f₁ * map m f₂
• 𝓝 x * 𝓝 y = 𝓝 (x * y)
@[instance]
Equations
- filter.has_one = {one := filter.principal 1}
@[instance]
Equations
- filter.monoid = {mul := has_mul.mul filter.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _}
theorem
filter.map_mul
{α : Type u}
{β : Type v}
[monoid α]
[monoid β]
(m : α → β)
[is_mul_hom m]
{f₁ f₂ : filter α} :
filter.map m (f₁ * f₂) = filter.map m f₁ * filter.map m f₂
theorem
filter.map_add
{α : Type u}
{β : Type v}
[add_monoid α]
[add_monoid β]
(m : α → β)
[is_add_hom m]
{f₁ f₂ : filter α} :
filter.map m (f₁ + f₂) = filter.map m f₁ + filter.map m f₂
theorem
filter.map_zero
{α : Type u}
{β : Type v}
[add_monoid α]
[add_monoid β]
(m : α → β)
[is_add_monoid_hom m] :
filter.map m 0 = 0
theorem
filter.map_one
{α : Type u}
{β : Type v}
[monoid α]
[monoid β]
(m : α → β)
[is_monoid_hom m] :
filter.map m 1 = 1
theorem
map.is_add_monoid_hom
{α : Type u}
{β : Type v}
[add_monoid α]
[add_monoid β]
(m : α → β)
[is_add_monoid_hom m] :
theorem
filter.map.is_monoid_hom
{α : Type u}
{β : Type v}
[monoid α]
[monoid β]
(m : α → β)
[is_monoid_hom m] :
theorem
filter.comap_mul_comap_le
{α : Type u}
{β : Type v}
[monoid α]
[monoid β]
(m : α → β)
[is_mul_hom m]
{f₁ f₂ : filter β} :
filter.comap m f₁ * filter.comap m f₂ ≤ filter.comap m (f₁ * f₂)
theorem
filter.comap_add_comap_le
{α : Type u}
{β : Type v}
[add_monoid α]
[add_monoid β]
(m : α → β)
[is_add_hom m]
{f₁ f₂ : filter β} :
filter.comap m f₁ + filter.comap m f₂ ≤ filter.comap m (f₁ + f₂)
theorem
filter.tendsto.mul_mul
{α : Type u}
{β : Type v}
[monoid α]
[monoid β]
{m : α → β}
[is_mul_hom m]
{f₁ g₁ : filter α}
{f₂ g₂ : filter β} :
filter.tendsto m f₁ f₂ → filter.tendsto m g₁ g₂ → filter.tendsto m (f₁ * g₁) (f₂ * g₂)
theorem
filter.tendsto.add_add
{α : Type u}
{β : Type v}
[add_monoid α]
[add_monoid β]
{m : α → β}
[is_add_hom m]
{f₁ g₁ : filter α}
{f₂ g₂ : filter β} :
filter.tendsto m f₁ f₂ → filter.tendsto m g₁ g₂ → filter.tendsto m (f₁ + g₁) (f₂ + g₂)