mathlib documentation

order.filter.pointwise

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]
def filter.has_zero {α : Type u} [has_zero α] :

@[instance]
def filter.has_one {α : Type u} [has_one α] :

Equations
@[simp]
theorem filter.mem_zero {α : Type u} [has_zero α] (s : set α) :
s 0 0 s

@[simp]
theorem filter.mem_one {α : Type u} [has_one α] (s : set α) :
s 1 1 s

@[instance]
def filter.has_add {α : Type u} [add_monoid α] :

@[instance]
def filter.has_mul {α : Type u} [monoid α] :

Equations
theorem filter.mem_mul {α : Type u} [monoid α] {f g : filter α} {s : set α} :
s f * g ∃ (t₁ t₂ : set α), t₁ f t₂ g t₁ * t₂ s

theorem filter.mem_add {α : Type u} [add_monoid α] {f g : filter α} {s : set α} :
s f + g ∃ (t₁ t₂ : set α), t₁ f t₂ g t₁ + t₂ s

theorem filter.mul_mem_mul {α : Type u} [monoid α] {f g : filter α} {s t : set α} :
s ft gs * t f * g

theorem filter.add_mem_add {α : Type u} [add_monoid α] {f g : filter α} {s t : set α} :
s ft gs + t f + g

theorem filter.add_le_add {α : Type u} [add_monoid α] {f₁ f₂ g₁ g₂ : filter α} :
f₁ f₂g₁ g₂f₁ + g₁ f₂ + g₂

theorem filter.mul_le_mul {α : Type u} [monoid α] {f₁ f₂ g₁ g₂ : filter α} :
f₁ f₂g₁ g₂f₁ * g₁ f₂ * g₂

theorem filter.ne_bot.mul {α : Type u} [monoid α] {f g : filter α} :
f.ne_botg.ne_bot(f * g).ne_bot

theorem filter.ne_bot.add {α : Type u} [add_monoid α] {f g : filter α} :
f.ne_botg.ne_bot(f + g).ne_bot

theorem filter.add_assoc {α : Type u} [add_monoid α] (f g h : filter α) :
f + g + h = f + (g + h)

theorem filter.mul_assoc {α : Type u} [monoid α] (f g h : filter α) :
(f * g) * h = f * g * h

theorem filter.one_mul {α : Type u} [monoid α] (f : filter α) :
1 * f = f

theorem filter.zero_add {α : Type u} [add_monoid α] (f : filter α) :
0 + f = f

theorem filter.add_zero {α : Type u} [add_monoid α] (f : filter α) :
f + 0 = f

theorem filter.mul_one {α : Type u} [monoid α] (f : filter α) :
f * 1 = f

@[instance]
def filter.add_monoid {α : Type u} [add_monoid α] :

@[instance]
def filter.monoid {α : Type u} [monoid α] :

Equations
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_one {α : Type u} {β : Type v} [monoid α] [monoid β] (m : α → β) [is_monoid_hom m] :

theorem filter.map_zero {α : 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 map.is_add_monoid_hom {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] (m : α → β) [is_add_monoid_hom m] :

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

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