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)

source
@[instance]
def filter.has_zero {α : Type u} [has_zero α] :
has_zero (filter α)

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

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

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

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

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

Equations
source
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

source
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

source
theorem filter.mul_mem_mul {α : Type u} [monoid α] {f g : filter α} {s t : set α} (hs : s ∈ f) (ht : t ∈ g) :
s * t ∈ f * g

source
theorem filter.add_mem_add {α : Type u} [add_monoid α] {f g : filter α} {s t : set α} (hs : s ∈ f) (ht : t ∈ g) :
s + t ∈ f + g

source
theorem filter.add_le_add {α : Type u} [add_monoid α] {f₁ f₂ g₁ g₂ : filter α} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
f₁ + g₁ ≤ f₂ + g₂

source
theorem filter.mul_le_mul {α : Type u} [monoid α] {f₁ f₂ g₁ g₂ : filter α} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
f₁ * g₁ ≤ f₂ * g₂

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

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

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

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

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

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

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

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

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

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

Equations
source
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₂

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

source
theorem filter.map_one {α : Type u} {β : Type v} [monoid α] [monoid β] (m : α → β) [is_monoid_hom m] :
filter.map m 1 = 1

source
theorem filter.map_zero {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] (m : α → β) [is_add_monoid_hom m] :
filter.map m 0 = 0

source
theorem filter.map.is_monoid_hom {α : Type u} {β : Type v} [monoid α] [monoid β] (m : α → β) [is_monoid_hom m] :
is_monoid_hom (filter.map m)

source
theorem map.is_add_monoid_hom {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] (m : α → β) [is_add_monoid_hom m] :
is_add_monoid_hom (filter.map m)

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

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

source
theorem filter.tendsto.add_add {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] {m : α → β} [is_add_hom m] {f₁ g₁ : filter α} {f₂ g₂ : filter β} (a : filter.tendsto m f₁ f₂) (a_1 : filter.tendsto m g₁ g₂) :
filter.tendsto m (f₁ + g₁) (f₂ + g₂)

source
theorem filter.tendsto.mul_mul {α : Type u} {β : Type v} [monoid α] [monoid β] {m : α → β} [is_mul_hom m] {f₁ g₁ : filter α} {f₂ g₂ : filter β} (a : filter.tendsto m f₁ f₂) (a_1 : filter.tendsto m g₁ g₂) :
filter.tendsto m (f₁ * g₁) (f₂ * g₂)