Mathlib.Order.Filter.Pointwise

Filter.instOne definition

: One (Filter α)

Full source

/-- `1 : Filter α` is defined as the filter of sets containing `1 : α` in locale `Pointwise`. -/
@[to_additive
      "`0 : Filter α` is defined as the filter of sets containing `0 : α` in locale `Pointwise`."]
protected def instOne : One (Filter α) :=
  ⟨pure 1⟩

Principal filter at the multiplicative identity

Informal description

The definition `1 : Filter α` represents the filter on a type `α` consisting of all subsets of `α` that contain the element `1` (where `1` is the multiplicative identity in `α`). This is equivalent to the principal filter generated by the singleton set `{1}`.

Filter.mem_one theorem

: s ∈ (1 : Filter α) ↔ (1 : α) ∈ s

Full source

@[to_additive (attr := simp)]
theorem mem_one : s ∈ (1 : Filter α)s ∈ (1 : Filter α) ↔ (1 : α) ∈ s :=
  mem_pure

Membership Criterion for Principal Filter at One: $s \in 1 \leftrightarrow 1 \in s$

Informal description

For any subset $s$ of a type $\alpha$ with a multiplicative identity $1$, the set $s$ belongs to the filter $1$ (i.e., the principal filter generated by $\{1\}$) if and only if $1 \in s$.

Filter.one_mem_one theorem

: (1 : Set α) ∈ (1 : Filter α)

Full source

@[to_additive]
theorem one_mem_one : (1 : Set α) ∈ (1 : Filter α) :=
  mem_pure.2 Set.one_mem_one

Membership of Identity Set in Principal Filter at One

Informal description

The set containing the multiplicative identity element $1$ of type $\alpha$ belongs to the principal filter generated by $1$ (i.e., $\{1\} \in (1 : \text{Filter } \alpha)$).

Filter.pure_one theorem

: pure 1 = (1 : Filter α)

Full source

@[to_additive (attr := simp)]
theorem pure_one : pure 1 = (1 : Filter α) :=
  rfl

Equality of Principal Filter at One and Filter One

Informal description

The principal filter generated by the singleton set $\{1\}$ is equal to the filter `1` on a type $\alpha$ with a multiplicative identity element $1$.

Filter.one_prod theorem

{l : Filter β} : (1 : Filter α) ×ˢ l = map (1, ·) l

Full source

@[to_additive (attr := simp) zero_prod]
theorem one_prod {l : Filter β} : (1 : Filter α) ×ˢ l = map (1, ·) l := pure_prod

Product of Identity Filter with Any Filter Equals Image Filter under Pairing with Identity

Informal description

For any filter $l$ on a type $\beta$, the product filter $(1 : \text{Filter } \alpha) \timesˢ l$ is equal to the image filter of $l$ under the function $(1, \cdot) : \beta \to \alpha \times \beta$ that maps $y \in \beta$ to $(1, y)$, where $1$ is the multiplicative identity in $\alpha$.

Filter.prod_one theorem

{l : Filter β} : l ×ˢ (1 : Filter α) = map (·, 1) l

Full source

@[to_additive (attr := simp) prod_zero]
theorem prod_one {l : Filter β} : l ×ˢ (1 : Filter α) = map (·, 1) l := prod_pure

Product Filter with Identity Filter Equals Mapping to Identity

Informal description

For any filter $l$ on a type $\beta$, the product filter $l \timesˢ (1 : \text{Filter } \alpha)$ is equal to the image filter of $l$ under the function $\lambda y, (y, 1)$, where $1$ is the multiplicative identity in $\alpha$.

Filter.principal_one theorem

: 𝓟 1 = (1 : Filter α)

Full source

@[to_additive (attr := simp)]
theorem principal_one : 𝓟 1 = (1 : Filter α) :=
  principal_singleton _

Principal Filter of Multiplicative Identity Equals One Filter

Informal description

The principal filter generated by the singleton set $\{1\}$ in a type $\alpha$ is equal to the filter $1$ (the multiplicative identity filter). That is, $\mathcal{P}\{1\} = 1$.

Filter.one_neBot theorem

: (1 : Filter α).NeBot

Full source

@[to_additive]
theorem one_neBot : (1 : Filter α).NeBot :=
  Filter.pure_neBot

Non-triviality of the Principal Filter at One

Informal description

The principal filter at the multiplicative identity $1$ in a type $\alpha$ is non-trivial, i.e., it does not contain the empty set.

Filter.map_one' theorem

(f : α → β) : (1 : Filter α).map f = pure (f 1)

Full source

@[to_additive (attr := simp)]
protected theorem map_one' (f : α → β) : (1 : Filter α).map f = pure (f 1) :=
  rfl

Image of Principal Filter at One under a Function

Informal description

For any function $f : \alpha \to \beta$, the image filter of the principal filter at $1 \in \alpha$ under $f$ is equal to the principal filter at $f(1) \in \beta$. In other words, $\text{map}\, f\, (\text{pure}\, 1) = \text{pure}\, (f\, 1)$.

Filter.le_one_iff theorem

: f ≤ 1 ↔ (1 : Set α) ∈ f

Full source

@[to_additive (attr := simp)]
theorem le_one_iff : f ≤ 1 ↔ (1 : Set α) ∈ f :=
  le_pure_iff

Characterization of Filter Inclusion in Principal Filter at Identity: $f \leq 1 \leftrightarrow \{1\} \in f$

Informal description

For any filter $f$ on a type $\alpha$, the filter $f$ is less than or equal to the principal filter at the multiplicative identity $1$ if and only if the singleton set $\{1\}$ belongs to $f$.

Filter.NeBot.le_one_iff theorem

(h : f.NeBot) : f ≤ 1 ↔ f = 1

Full source

@[to_additive]
protected theorem NeBot.le_one_iff (h : f.NeBot) : f ≤ 1 ↔ f = 1 :=
  h.le_pure_iff

Characterization of Principal Filter at Identity for Non-Trivial Filters: $f \leq 1 \leftrightarrow f = 1$

Informal description

For any non-trivial filter $f$ on a type $\alpha$ (i.e., $f$ does not contain the empty set), the filter $f$ is less than or equal to the principal filter at the multiplicative identity $1$ if and only if $f$ is equal to the principal filter at $1$.

Filter.eventually_one theorem

{p : α → Prop} : (∀ᶠ x in 1, p x) ↔ p 1

Full source

@[to_additive (attr := simp)]
theorem eventually_one {p : α → Prop} : (∀ᶠ x in 1, p x) ↔ p 1 :=
  eventually_pure

Eventual Truth in Principal Filter at One

Informal description

For any predicate $p : \alpha \to \text{Prop}$, the property $p$ holds eventually with respect to the filter $1$ (the principal filter at the multiplicative identity) if and only if $p(1)$ holds. In other words, $\forallᶠ x \text{ in } 1, p x \leftrightarrow p 1$.

Filter.tendsto_one theorem

{a : Filter β} {f : β → α} : Tendsto f a 1 ↔ ∀ᶠ x in a, f x = 1

Full source

@[to_additive (attr := simp)]
theorem tendsto_one {a : Filter β} {f : β → α} : TendstoTendsto f a 1 ↔ ∀ᶠ x in a, f x = 1 :=
  tendsto_pure

Characterization of Tendency to Principal Filter at One: $f \to 1$ iff $f(x) = 1$ Eventually

Informal description

For any filter $a$ on a type $\beta$ and any function $f : \beta \to \alpha$, the function $f$ tends to the principal filter $1$ (generated by $\{1\}$) with respect to $a$ if and only if $f(x) = 1$ holds eventually for all $x$ in $a$.

Filter.one_prod_one theorem

[One β] : (1 : Filter α) ×ˢ (1 : Filter β) = 1

Full source

@[to_additive zero_prod_zero]
theorem one_prod_one [One β] : (1 : Filter α) ×ˢ (1 : Filter β) = 1 :=
  prod_pure_pure

Product of Principal Filters at Identity Equals Identity Filter

Informal description

For types $\alpha$ and $\beta$ each equipped with a multiplicative identity element $1$, the product filter $(1 : \text{Filter } \alpha) \timesˢ (1 : \text{Filter } \beta)$ equals the principal filter $1$ on $\alpha \times \beta$.

Filter.pureOneHom definition

: OneHom α (Filter α)

Full source

/-- `pure` as a `OneHom`. -/
@[to_additive "`pure` as a `ZeroHom`."]
def pureOneHom : OneHom α (Filter α) where
  toFun := pure; map_one' := pure_one

Identity-preserving homomorphism from elements to principal filters

Informal description

The function `pureOneHom` maps the multiplicative identity element $1$ of a type $\alpha$ to the principal filter generated by the singleton set $\{1\}$ in $\text{Filter } \alpha$. It is a homomorphism preserving the identity element, i.e., it satisfies $\text{pureOneHom}(1) = 1$.

Filter.coe_pureOneHom theorem

: (pureOneHom : α → Filter α) = pure

Full source

@[to_additive (attr := simp)]
theorem coe_pureOneHom : (pureOneHom : α → Filter α) = pure :=
  rfl

Equality of `pureOneHom` and `pure` functions

Informal description

The function `pureOneHom` from a type $\alpha$ to the filter space $\text{Filter } \alpha$ is equal to the `pure` function, which maps an element $a \in \alpha$ to the principal filter generated by the singleton set $\{a\}$.

Filter.pureOneHom_apply theorem

(a : α) : pureOneHom a = pure a

Full source

@[to_additive (attr := simp)]
theorem pureOneHom_apply (a : α) : pureOneHom a = pure a :=
  rfl

Equality of `pureOneHom` and Principal Filter for Any Element

Informal description

For any element $a$ of a type $\alpha$, the function `pureOneHom` evaluated at $a$ is equal to the principal filter generated by the singleton set $\{a\}$, i.e., $\text{pureOneHom}(a) = \text{pure } a$.

Filter.map_one theorem

[FunLike F α β] [OneHomClass F α β] (φ : F) : map φ 1 = 1

Full source

@[to_additive]
protected theorem map_one [FunLike F α β] [OneHomClass F α β] (φ : F) : map φ 1 = 1 := by
  simp

Preservation of Principal Filter at Identity under Homomorphism

Informal description

For any homomorphism $\varphi$ from a type $\alpha$ to a type $\beta$ that preserves the multiplicative identity (i.e., $\varphi(1) = 1$), the image of the principal filter at $1$ under $\varphi$ is equal to the principal filter at $1$ in $\beta$, i.e., $\text{map } \varphi \ 1 = 1$.

Filter.instInv instance

: Inv (Filter α)

Full source

/-- The inverse of a filter is the pointwise preimage under `⁻¹` of its sets. -/
@[to_additive "The negation of a filter is the pointwise preimage under `-` of its sets."]
instance instInv : Inv (Filter α) :=
  ⟨map Inv.inv⟩

Inversion Operation on Filters

Informal description

For any type $\alpha$ with an inversion operation, the filters on $\alpha$ can be equipped with an inversion operation where the inverse of a filter $f$ is the filter generated by the pointwise inverses of all sets in $f$.

Filter.map_inv theorem

: f.map Inv.inv = f⁻¹

Full source

@[to_additive (attr := simp)]
protected theorem map_inv : f.map Inv.inv = f⁻¹ :=
  rfl

Image of Filter under Inversion Equals Pointwise Inverse Filter

Informal description

For any filter $f$ on a type $\alpha$ with an inversion operation, the image of $f$ under the inversion map $\text{Inv.inv} : \alpha \to \alpha$ is equal to the pointwise inverse filter $f^{-1}$.

Filter.mem_inv theorem

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

Full source

@[to_additive]
theorem mem_inv : s ∈ f⁻¹s ∈ f⁻¹ ↔ Inv.inv ⁻¹' s ∈ f :=
  Iff.rfl

Membership in Inverse Filter via Preimage

Informal description

For any set $s$ and any filter $f$ on a type $\alpha$ equipped with an inversion operation, the set $s$ belongs to the inverse filter $f^{-1}$ if and only if the preimage of $s$ under the inversion operation belongs to $f$.

Filter.inv_le_inv theorem

(hf : f ≤ g) : f⁻¹ ≤ g⁻¹

Full source

@[to_additive]
protected theorem inv_le_inv (hf : f ≤ g) : f⁻¹ ≤ g⁻¹ :=
  map_mono hf

Monotonicity of Filter Inversion: $f \leq g$ implies $f^{-1} \leq g^{-1}$

Informal description

For any two filters $f$ and $g$ on a type $\alpha$ equipped with an inversion operation, if $f \leq g$, then the inverse filter $f^{-1}$ is less than or equal to the inverse filter $g^{-1}$.

Filter.inv_pure theorem

: (pure a : Filter α)⁻¹ = pure a⁻¹

Full source

@[to_additive (attr := simp)]
theorem inv_pure : (pure a : Filter α)⁻¹ = pure a⁻¹ :=
  rfl

Inverse of Pure Filter Equals Pure Filter of Inverse

Informal description

For any element $a$ of a type $\alpha$ equipped with an inversion operation, the inverse of the pure filter generated by $a$ is equal to the pure filter generated by the inverse of $a$, i.e., $(\text{pure } a)^{-1} = \text{pure } (a^{-1})$.

Filter.inv_eq_bot_iff theorem

: f⁻¹ = ⊥ ↔ f = ⊥

Full source

@[to_additive (attr := simp)]
theorem inv_eq_bot_iff : f⁻¹f⁻¹ = ⊥ ↔ f = ⊥ :=
  map_eq_bot_iff

Inverse Filter is Bottom iff Original Filter is Bottom

Informal description

For any filter $f$ on a type $\alpha$ equipped with an inversion operation, the inverse filter $f^{-1}$ is equal to the bottom filter $\bot$ if and only if $f$ itself is equal to $\bot$.

Filter.neBot_inv_iff theorem

: f⁻¹.NeBot ↔ NeBot f

Full source

@[to_additive (attr := simp)]
theorem neBot_inv_iff : f⁻¹f⁻¹.NeBot ↔ NeBot f :=
  map_neBot_iff _

Non-triviality of Inverse Filter $\leftrightarrow$ Non-triviality of Original Filter

Informal description

For any filter $f$ on a type $\alpha$ equipped with an inversion operation, the inverse filter $f^{-1}$ is non-trivial if and only if $f$ itself is non-trivial.

Filter.NeBot.inv theorem

: f.NeBot → f⁻¹.NeBot

Full source

@[to_additive]
protected theorem NeBot.inv : f.NeBot → f⁻¹.NeBot := fun h => h.map _

Non-triviality Preservation under Filter Inversion

Informal description

For any non-trivial filter $f$ on a type $\alpha$ with an inversion operation, the inverse filter $f^{-1}$ is also non-trivial.

Filter.inv.instNeBot theorem

[NeBot f] : NeBot f⁻¹

Full source

@[to_additive neg.instNeBot]
lemma inv.instNeBot [NeBot f] : NeBot f⁻¹ := .inv ‹_›

Non-triviality Preservation under Filter Inversion

Informal description

For any non-trivial filter $f$ on a type $\alpha$ with an inversion operation, the inverse filter $f^{-1}$ is also non-trivial.

Filter.comap_inv theorem

: comap Inv.inv f = f⁻¹

Full source

@[to_additive (attr := simp)]
protected lemma comap_inv : comap Inv.inv f = f⁻¹ :=
  .symm <| map_eq_comap_of_inverse (inv_comp_inv _) (inv_comp_inv _)

Preimage of Filter under Inversion Equals Inverse Filter

Informal description

For any filter $f$ on a type $\alpha$ equipped with an inversion operation, the preimage filter of $f$ under the inversion map is equal to the inverse filter of $f$, i.e., \[ \text{comap } (\lambda x, x^{-1}) f = f^{-1}. \]

Filter.inv_mem_inv theorem

(hs : s ∈ f) : s⁻¹ ∈ f⁻¹

Full source

@[to_additive]
theorem inv_mem_inv (hs : s ∈ f) : s⁻¹s⁻¹ ∈ f⁻¹ := by rwa [mem_inv, inv_preimage, inv_inv]

Inverse Set Membership in Inverse Filter

Informal description

For any set $s$ in a filter $f$ on a type $\alpha$ equipped with an inversion operation, the pointwise inverse set $s^{-1}$ belongs to the inverse filter $f^{-1}$.

Filter.instInvolutiveInv definition

: InvolutiveInv (Filter α)

Full source

/-- Inversion is involutive on `Filter α` if it is on `α`. -/
@[to_additive "Negation is involutive on `Filter α` if it is on `α`."]
protected def instInvolutiveInv : InvolutiveInv (Filter α) :=
  { Filter.instInv with
    inv_inv := fun f => map_map.trans <| by rw [inv_involutive.comp_self, map_id] }

Involutive inversion of filters

Informal description

The inversion operation on filters is involutive, meaning that for any filter $f$ on a type $\alpha$ equipped with an involutive inversion operation, the double inversion of $f$ returns $f$ itself. That is, $(f^{-1})^{-1} = f$.

Filter.inv_le_inv_iff theorem

: f⁻¹ ≤ g⁻¹ ↔ f ≤ g

Full source

@[to_additive (attr := simp)]
protected theorem inv_le_inv_iff : f⁻¹f⁻¹ ≤ g⁻¹ ↔ f ≤ g :=
  ⟨fun h => inv_inv f ▸ inv_inv g ▸ Filter.inv_le_inv h, Filter.inv_le_inv⟩

Inversion Preserves Filter Order: $f^{-1} \leq g^{-1} \leftrightarrow f \leq g$

Informal description

For any two filters $f$ and $g$ on a type $\alpha$ equipped with an inversion operation, the inverse filter $f^{-1}$ is less than or equal to the inverse filter $g^{-1}$ if and only if $f$ is less than or equal to $g$.

Filter.inv_le_iff_le_inv theorem

: f⁻¹ ≤ g ↔ f ≤ g⁻¹

Full source

@[to_additive]
theorem inv_le_iff_le_inv : f⁻¹f⁻¹ ≤ g ↔ f ≤ g⁻¹ := by rw [← Filter.inv_le_inv_iff, inv_inv]

Inversion Order Equivalence: $f^{-1} \leq g \leftrightarrow f \leq g^{-1}$

Informal description

For any two filters $f$ and $g$ on a type $\alpha$ equipped with an inversion operation, the inverse filter $f^{-1}$ is less than or equal to $g$ if and only if $f$ is less than or equal to the inverse filter $g^{-1}$.

Filter.inv_le_self theorem

: f⁻¹ ≤ f ↔ f⁻¹ = f

Full source

@[to_additive (attr := simp)]
theorem inv_le_self : f⁻¹f⁻¹ ≤ f ↔ f⁻¹ = f :=
  ⟨fun h => h.antisymm <| inv_le_iff_le_inv.1 h, Eq.le⟩

Inversion Order Equality: $f^{-1} \leq f \leftrightarrow f^{-1} = f$

Informal description

For any filter $f$ on a type $\alpha$ equipped with an inversion operation, the inverse filter $f^{-1}$ is less than or equal to $f$ if and only if $f^{-1}$ is equal to $f$.

Filter.inv_atTop theorem

{G : Type*} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : (atTop : Filter G)⁻¹ = atBot

Full source

@[to_additive (attr := simp)]
lemma inv_atTop {G : Type*} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] :
    (atTop : Filter G)⁻¹ = atBot :=
  (OrderIso.inv G).map_atTop

Inversion of `atTop` Filter Equals `atBot` in Ordered Commutative Groups

Informal description

Let $G$ be a commutative group equipped with a partial order such that it forms an ordered monoid. Then the inverse of the filter `atTop` (the filter representing the limit at positive infinity) is equal to the filter `atBot` (the filter representing the limit at negative infinity), i.e., $$ (\text{atTop} : \text{Filter } G)^{-1} = \text{atBot}. $$

Filter.instMul definition

: Mul (Filter α)

Full source

/-- The filter `f * g` is generated by `{s * t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
@[to_additive "The filter `f + g` is generated by `{s + t | s ∈ f, t ∈ g}` in locale `Pointwise`."]
protected def instMul : Mul (Filter α) :=
  ⟨/- This is defeq to `map₂ (· * ·) f g`, but the hypothesis unfolds to `t₁ * t₂ ⊆ s` rather
  than all the way to `Set.image2 (· * ·) t₁ t₂ ⊆ s`. -/
  fun f g => { map₂ (· * ·) f g with sets := { s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s } }⟩

Multiplication of filters

Informal description

The multiplication operation on filters on a type $\alpha$ with a multiplication operation is defined as follows: for any two filters $f$ and $g$ on $\alpha$, the product filter $f * g$ is the filter generated by all sets of the form $t_1 * t_2$ where $t_1 \in f$ and $t_2 \in g$. Here, $t_1 * t_2$ denotes the pointwise product $\{x * y \mid x \in t_1, y \in t_2\}$.

Filter.map₂_mul theorem

: map₂ (· * ·) f g = f * g

Full source

@[to_additive (attr := simp)]
theorem map₂_mul : map₂ (· * ·) f g = f * g :=
  rfl

Equality of Pointwise Multiplication Image and Product Filter

Informal description

For any filters $f$ and $g$ on a type $\alpha$ with a multiplication operation, the image of the pointwise multiplication operation under `map₂` is equal to the product filter $f * g$. That is, $\text{map}_2 (\cdot * \cdot) f g = f * g$.

Filter.mem_mul theorem

: s ∈ f * g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s

Full source

@[to_additive]
theorem mem_mul : s ∈ f * gs ∈ f * g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s :=
  Iff.rfl

Characterization of Membership in Product Filter

Informal description

A subset $s$ of a type $\alpha$ belongs to the product filter $f * g$ if and only if there exist subsets $t_1 \in f$ and $t_2 \in g$ such that the pointwise product $t_1 * t_2$ is contained in $s$. Here, $t_1 * t_2$ denotes the set $\{x * y \mid x \in t_1, y \in t_2\}$.

Filter.mul_mem_mul theorem

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

Full source

@[to_additive]
theorem mul_mem_mul : s ∈ f → t ∈ g → s * t ∈ f * g :=
  image2_mem_map₂

Product of Filter Members Belongs to Product Filter

Informal description

For any subsets $s$ and $t$ of a type $\alpha$ with a multiplication operation, if $s$ belongs to a filter $f$ and $t$ belongs to a filter $g$, then the pointwise product set $s * t$ belongs to the product filter $f * g$. Here, $s * t$ denotes the set $\{x * y \mid x \in s, y \in t\}$.

Filter.bot_mul theorem

: ⊥ * g = ⊥

Full source

@[to_additive (attr := simp)]
theorem bot_mul : ⊥ * g = ⊥ :=
  map₂_bot_left

Bottom filter is absorbing under multiplication: $\bot * g = \bot$

Informal description

For any filter $g$ on a type $\alpha$ with a multiplication operation, the product of the bottom filter $\bot$ (the filter containing all subsets of $\alpha$) with $g$ is equal to the bottom filter $\bot$.

Filter.mul_bot theorem

: f * ⊥ = ⊥

Full source

@[to_additive (attr := simp)]
theorem mul_bot : f * ⊥ = ⊥ :=
  map₂_bot_right

Right Multiplication by Bottom Filter Yields Bottom Filter

Informal description

For any filter $f$ on a type $\alpha$, the product of $f$ with the bottom filter $\bot$ is equal to $\bot$, i.e., $f * \bot = \bot$.

Filter.mul_eq_bot_iff theorem

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

Full source

@[to_additive (attr := simp)]
theorem mul_eq_bot_iff : f * g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
  map₂_eq_bot_iff

Product Filter is Bottom if and only if One Factor is Bottom

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the product filter $f * g$ is equal to the bottom filter $\bot$ if and only if either $f$ or $g$ is equal to $\bot$.

Filter.mul_neBot_iff theorem

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

Full source

@[to_additive (attr := simp)] -- TODO: make this a scoped instance in the `Pointwise` namespace
lemma mul_neBot_iff : (f * g).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff

Product Filter is Non-Trivial if and only if Both Factors Are Non-Trivial

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the product filter $f * g$ is non-trivial if and only if both $f$ and $g$ are non-trivial. In other words, $(f * g).\text{NeBot} \leftrightarrow f.\text{NeBot} \wedge g.\text{NeBot}$.

Filter.NeBot.mul theorem

: NeBot f → NeBot g → NeBot (f * g)

Full source

@[to_additive]
protected theorem NeBot.mul : NeBot f → NeBot g → NeBot (f * g) :=
  NeBot.map₂

Non-triviality of the Product of Non-trivial Filters

Informal description

If two filters $f$ and $g$ on a type $\alpha$ are both non-trivial (i.e., neither is the bottom filter), then their product filter $f * g$ is also non-trivial.

Filter.NeBot.of_mul_left theorem

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

Full source

@[to_additive]
theorem NeBot.of_mul_left : (f * g).NeBot → f.NeBot :=
  NeBot.of_map₂_left

Non-triviality of Left Factor in Filter Multiplication

Informal description

If the product filter $f * g$ is non-trivial, then the filter $f$ is non-trivial.

Filter.NeBot.of_mul_right theorem

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

Full source

@[to_additive]
theorem NeBot.of_mul_right : (f * g).NeBot → g.NeBot :=
  NeBot.of_map₂_right

Non-triviality of Right Factor in Filter Multiplication

Informal description

If the product filter $f * g$ is non-trivial, then the filter $g$ is non-trivial.

Filter.mul.instNeBot theorem

[NeBot f] [NeBot g] : NeBot (f * g)

Full source

@[to_additive add.instNeBot]
protected lemma mul.instNeBot [NeBot f] [NeBot g] : NeBot (f * g) := .mul ‹_› ‹_›

Non-triviality of the Product of Non-trivial Filters

Informal description

If $f$ and $g$ are non-trivial filters on a type $\alpha$, then their product filter $f * g$ is also non-trivial.

Filter.pure_mul theorem

: pure a * g = g.map (a * ·)

Full source

@[to_additive (attr := simp)]
theorem pure_mul : pure a * g = g.map (a * ·) :=
  map₂_pure_left

Pure Filter Multiplication Equals Left Multiplication Image Filter

Informal description

For any element $a$ in a type $\alpha$ with a multiplication operation and any filter $g$ on $\alpha$, the product of the pure filter at $a$ and $g$ is equal to the image filter of $g$ under the left multiplication map $x \mapsto a * x$.

Filter.mul_pure theorem

: f * pure b = f.map (· * b)

Full source

@[to_additive (attr := simp)]
theorem mul_pure : f * pure b = f.map (· * b) :=
  map₂_pure_right

Right Multiplication by Pure Element in Filter Multiplication

Informal description

For any filter $f$ on a type $\alpha$ with a multiplication operation and any element $b \in \alpha$, the product filter $f * \text{pure } b$ is equal to the image filter of $f$ under the right multiplication map $x \mapsto x * b$.

Filter.pure_mul_pure theorem

: (pure a : Filter α) * pure b = pure (a * b)

Full source

@[to_additive]
theorem pure_mul_pure : (pure a : Filter α) * pure b = pure (a * b) := by simp

Product of Pure Filters Equals Pure Filter of Product

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with a multiplication operation, the product of the pure filters at $a$ and $b$ is equal to the pure filter at the product $a * b$. In other words, $\{a\} * \{b\} = \{a * b\}$ in the filter algebra.

Filter.le_mul_iff theorem

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

Full source

@[to_additive (attr := simp)]
theorem le_mul_iff : h ≤ f * g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s * t ∈ h :=
  le_map₂_iff

Characterization of Filter Inequality via Pointwise Multiplication

Informal description

For filters $f$, $g$, and $h$ on a type $\alpha$ with a multiplication operation, the filter $h$ is less than or equal to the product filter $f * g$ if and only if for every set $s$ in $f$ and every set $t$ in $g$, the pointwise product set $s * t$ is in $h$.

Filter.mulLeftMono instance

: MulLeftMono (Filter α)

Full source

@[to_additive]
instance mulLeftMono : MulLeftMono (Filter α) :=
  ⟨fun _ _ _ => map₂_mono_left⟩

Monotonicity of Left Multiplication in Filters

Informal description

For any type $\alpha$ with a multiplication operation, the collection of filters on $\alpha$ satisfies the property that left multiplication is monotone. That is, for any filters $f$, $g$, and $h$ on $\alpha$, if $g \leq h$ (meaning $h \subseteq g$ in the inclusion order), then $f * g \leq f * h$ (meaning the product filter $f * h$ is contained in $f * g$).

Filter.mulRightMono instance

: MulRightMono (Filter α)

Full source

@[to_additive]
instance mulRightMono : MulRightMono (Filter α) :=
  ⟨fun _ _ _ => map₂_mono_right⟩

Monotonicity of Right Multiplication by a Filter

Informal description

For any type $\alpha$ with a multiplication operation, the operation of right multiplication by a filter on $\alpha$ is monotone with respect to the inclusion order on filters. That is, for any filters $f, g, h$ on $\alpha$, if $f \leq g$, then $f * h \leq g * h$.

Filter.map_mul theorem

[FunLike F α β] [MulHomClass F α β] (m : F) : (f₁ * f₂).map m = f₁.map m * f₂.map m

Full source

@[to_additive]
protected theorem map_mul [FunLike F α β] [MulHomClass F α β] (m : F) :
    (f₁ * f₂).map m = f₁.map m * f₂.map m :=
  map_map₂_distrib <| map_mul m

Pushforward of Filter Multiplication Preserves Multiplication

Informal description

For any multiplicative homomorphism $m \colon \alpha \to \beta$ between types $\alpha$ and $\beta$ with multiplication operations, and for any filters $f_1$ and $f_2$ on $\alpha$, the image filter of the product filter $f_1 * f_2$ under $m$ is equal to the product of the image filters $m(f_1) * m(f_2)$. In other words, the following equality holds: $$ m_*(f_1 * f_2) = m_*(f_1) * m_*(f_2) $$ where $m_*$ denotes the pushforward (image) filter under $m$.

Filter.pureMulHom definition

: α →ₙ* Filter α

Full source

/-- `pure` operation as a `MulHom`. -/
@[to_additive "The singleton operation as an `AddHom`."]
def pureMulHom : α →ₙ* Filter α where
  toFun := pure; map_mul' _ _ := pure_mul_pure.symm

Multiplicative homomorphism from elements to principal filters

Informal description

The function `pureMulHom` maps an element $a$ of a multiplicative structure $\alpha$ to the principal filter $\{a\}$ (i.e., the filter generated by the singleton set $\{a\}$), and it preserves multiplication in the sense that $\text{pure}(a * b) = \text{pure}(a) * \text{pure}(b)$ for all $a, b \in \alpha$.

Filter.coe_pureMulHom theorem

: (pureMulHom : α → Filter α) = pure

Full source

@[to_additive (attr := simp)]
theorem coe_pureMulHom : (pureMulHom : α → Filter α) = pure :=
  rfl

Equality of `pureMulHom` and `pure` Functions

Informal description

The function `pureMulHom` from elements of a multiplicative structure $\alpha$ to filters on $\alpha$ is equal to the `pure` function, which maps each element $a \in \alpha$ to the principal filter generated by $\{a\}$.

Filter.pureMulHom_apply theorem

(a : α) : pureMulHom a = pure a

Full source

@[to_additive (attr := simp)]
theorem pureMulHom_apply (a : α) : pureMulHom a = pure a :=
  rfl

Evaluation of `pureMulHom` as Principal Filter

Informal description

For any element $a$ in a multiplicative structure $\alpha$, the multiplicative homomorphism `pureMulHom` evaluated at $a$ is equal to the principal filter generated by $\{a\}$, i.e., $\text{pureMulHom}(a) = \text{pure}(a)$.

Filter.instDiv definition

: Div (Filter α)

Full source

/-- The filter `f / g` is generated by `{s / t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
@[to_additive "The filter `f - g` is generated by `{s - t | s ∈ f, t ∈ g}` in locale `Pointwise`."]
protected def instDiv : Div (Filter α) :=
  ⟨/- This is defeq to `map₂ (· / ·) f g`, but the hypothesis unfolds to `t₁ / t₂ ⊆ s`
  rather than all the way to `Set.image2 (· / ·) t₁ t₂ ⊆ s`. -/
  fun f g => { map₂ (· / ·) f g with sets := { s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s } }⟩

Division of filters

Informal description

The division operation on filters is defined such that for any two filters $ f $ and $ g $ on a type $ \alpha $, the filter $ f / g $ is generated by all sets of the form $ t_1 / t_2 $ where $ t_1 \in f $ and $ t_2 \in g $. Here, $ t_1 / t_2 $ denotes the pointwise division of the sets $ t_1 $ and $ t_2 $, i.e., $ \{ x / y \mid x \in t_1, y \in t_2 \} $.

Filter.map₂_div theorem

: map₂ (· / ·) f g = f / g

Full source

@[to_additive (attr := simp)]
theorem map₂_div : map₂ (· / ·) f g = f / g :=
  rfl

Equality of Pointwise Division and Filter Division via `map₂`

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the filter obtained by applying the pointwise division operation via `map₂` is equal to the division of the filters $f / g$. That is, $\text{map}_2 (\cdot / \cdot) f g = f / g$.

Filter.mem_div theorem

: s ∈ f / g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s

Full source

@[to_additive]
theorem mem_div : s ∈ f / gs ∈ f / g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s :=
  Iff.rfl

Membership Criterion for Division Filter: $s \in f / g$

Informal description

A set $s$ belongs to the division filter $f / g$ if and only if there exist sets $t_1 \in f$ and $t_2 \in g$ such that the pointwise division $t_1 / t_2$ is a subset of $s$.

Filter.div_mem_div theorem

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

Full source

@[to_additive]
theorem div_mem_div : s ∈ f → t ∈ g → s / t ∈ f / g :=
  image2_mem_map₂

Membership of Pointwise Division in Filter Division

Informal description

For any sets $s$ and $t$ in a type $\alpha$, if $s$ belongs to a filter $f$ and $t$ belongs to a filter $g$, then the pointwise division set $s / t$ belongs to the filter $f / g$.

Filter.bot_div theorem

: ⊥ / g = ⊥

Full source

@[to_additive (attr := simp)]
theorem bot_div : ⊥ / g = ⊥ :=
  map₂_bot_left

Bottom Filter Divided by Any Filter is Bottom

Informal description

For any filter $g$ on a type $\alpha$, the division of the bottom filter $\bot$ by $g$ equals the bottom filter, i.e., $\bot / g = \bot$.

Filter.div_bot theorem

: f / ⊥ = ⊥

Full source

@[to_additive (attr := simp)]
theorem div_bot : f / ⊥ = ⊥ :=
  map₂_bot_right

Division by Bottom Filter Yields Bottom Filter

Informal description

For any filter $f$ on a type $\alpha$, the division of $f$ by the bottom filter $\bot$ is equal to the bottom filter, i.e., $f / \bot = \bot$.

Filter.div_eq_bot_iff theorem

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

Full source

@[to_additive (attr := simp)]
theorem div_eq_bot_iff : f / g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
  map₂_eq_bot_iff

Division Filter is Bottom if and only if Either Filter is Bottom

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the division filter $f / g$ is equal to the bottom filter $\bot$ if and only if either $f$ is $\bot$ or $g$ is $\bot$.

Filter.div_neBot_iff theorem

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

Full source

@[to_additive (attr := simp)]
theorem div_neBot_iff : (f / g).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff

Non-triviality of Filter Division: $(f / g).\text{NeBot} \leftrightarrow f.\text{NeBot} \land g.\text{NeBot}$

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the filter $f / g$ is non-trivial if and only if both $f$ and $g$ are non-trivial.

Filter.NeBot.div theorem

: NeBot f → NeBot g → NeBot (f / g)

Full source

@[to_additive]
protected theorem NeBot.div : NeBot f → NeBot g → NeBot (f / g) :=
  NeBot.map₂

Non-triviality of Filter Division

Informal description

If $f$ and $g$ are non-trivial filters on a type $\alpha$, then their division $f / g$ is also a non-trivial filter.

Filter.NeBot.of_div_left theorem

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

Full source

@[to_additive]
theorem NeBot.of_div_left : (f / g).NeBot → f.NeBot :=
  NeBot.of_map₂_left

Non-triviality of the Left Filter in Division

Informal description

If the division of two filters $f$ and $g$ is non-trivial, then $f$ is non-trivial.

Filter.NeBot.of_div_right theorem

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

Full source

@[to_additive]
theorem NeBot.of_div_right : (f / g).NeBot → g.NeBot :=
  NeBot.of_map₂_right

Non-triviality of Right Filter in Division of Filters

Informal description

If the division of two filters $f$ and $g$ is non-trivial (i.e., $f / g \neq \bot$), then the filter $g$ is also non-trivial (i.e., $g \neq \bot$).

Filter.div.instNeBot theorem

[NeBot f] [NeBot g] : NeBot (f / g)

Full source

@[to_additive sub.instNeBot]
lemma div.instNeBot [NeBot f] [NeBot g] : NeBot (f / g) := .div ‹_› ‹_›

Non-triviality of Filter Division

Informal description

For any two non-trivial filters $f$ and $g$ on a type $\alpha$, the division filter $f / g$ is also non-trivial.

Filter.pure_div theorem

: pure a / g = g.map (a / ·)

Full source

@[to_additive (attr := simp)]
theorem pure_div : pure a / g = g.map (a / ·) :=
  map₂_pure_left

Pure Filter Division Equals Image Filter under Division by Constant

Informal description

For any element $a$ in a type $\alpha$ and any filter $g$ on $\alpha$, the division of the pure filter at $a$ by $g$ is equal to the image filter of $g$ under the function $x \mapsto a / x$.

Filter.div_pure theorem

: f / pure b = f.map (· / b)

Full source

@[to_additive (attr := simp)]
theorem div_pure : f / pure b = f.map (· / b) :=
  map₂_pure_right

Division of a Filter by a Singleton Filter Equals Mapping by Division

Informal description

For any filter $f$ on a type $\alpha$ and any element $b \in \alpha$, the division of $f$ by the principal filter generated by $\{b\}$ is equal to the image filter of $f$ under the function $x \mapsto x / b$.

Filter.pure_div_pure theorem

: (pure a : Filter α) / pure b = pure (a / b)

Full source

@[to_additive]
theorem pure_div_pure : (pure a : Filter α) / pure b = pure (a / b) := by simp

Division of Principal Filters Yields Principal Filter of Division

Informal description

For any elements $a$ and $b$ in a type $\alpha$, the division of the principal filter generated by $\{a\}$ by the principal filter generated by $\{b\}$ equals the principal filter generated by $\{a / b\}$.

Filter.div_le_div theorem

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

Full source

@[to_additive]
protected theorem div_le_div : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ / g₁ ≤ f₂ / g₂ :=
  map₂_mono

Monotonicity of Filter Division

Informal description

For any filters $f_1, f_2, g_1, g_2$ on a type $\alpha$, if $f_1 \leq f_2$ and $g_1 \leq g_2$, then the filter division satisfies $f_1 / g_1 \leq f_2 / g_2$.

Filter.div_le_div_left theorem

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

Full source

@[to_additive]
protected theorem div_le_div_left : g₁ ≤ g₂ → f / g₁ ≤ f / g₂ :=
  map₂_mono_left

Monotonicity of Filter Division in the Second Argument

Informal description

For any filters $g₁$ and $g₂$ on a type $\alpha$, if $g₁ \leq g₂$ in the partial order of filters, then for any filter $f$ on $\alpha$, the filter division satisfies $f / g₁ \leq f / g₂$.

Filter.div_le_div_right theorem

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

Full source

@[to_additive]
protected theorem div_le_div_right : f₁ ≤ f₂ → f₁ / g ≤ f₂ / g :=
  map₂_mono_right

Monotonicity of Filter Division in the First Argument

Informal description

For any filters $f_1$, $f_2$, and $g$ on a type $\alpha$, if $f_1 \leq f_2$ in the partial order of filters, then the division of filters satisfies $f_1 / g \leq f_2 / g$.

Filter.le_div_iff theorem

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

Full source

@[to_additive (attr := simp)]
protected theorem le_div_iff : h ≤ f / g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s / t ∈ h :=
  le_map₂_iff

Characterization of Filter Division Order: $h \leq f / g$ iff $s / t \in h$ for all $s \in f$, $t \in g$

Informal description

For filters $h$, $f$, and $g$ on a type $\alpha$, the inequality $h \leq f / g$ holds if and only if for every set $s \in f$ and every set $t \in g$, the pointwise division set $s / t$ is an element of $h$.

Filter.covariant_div instance

: CovariantClass (Filter α) (Filter α) (· / ·) (· ≤ ·)

Full source

@[to_additive]
instance covariant_div : CovariantClass (Filter α) (Filter α) (· / ·) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_left⟩

Covariance of Filter Division with Respect to Partial Order

Informal description

For any type $\alpha$ with a division operation, the division operation on filters over $\alpha$ is covariant with respect to the partial order $\leq$ on filters. That is, for any filters $f_1, f_2, g$ on $\alpha$, if $f_1 \leq f_2$, then $f_1 / g \leq f_2 / g$.

Filter.covariant_swap_div instance

: CovariantClass (Filter α) (Filter α) (swap (· / ·)) (· ≤ ·)

Full source

@[to_additive]
instance covariant_swap_div : CovariantClass (Filter α) (Filter α) (swap (· / ·)) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_right⟩

Covariance of Filter Division in the Second Argument

Informal description

For any type $\alpha$ with a division operation, the operation of division on filters over $\alpha$ is covariant in its second argument with respect to the partial order $\leq$ on filters. That is, for any filters $f$, $g$, and $h$ on $\alpha$, if $g \leq h$, then $f / g \leq f / h$.

Filter.instNSMul definition

[Zero α] [Add α] : SMul ℕ (Filter α)

Full source

/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Filter`. See
Note [pointwise nat action]. -/
protected def instNSMul [Zero α] [Add α] : SMul ℕ (Filter α) :=
  ⟨nsmulRec⟩

Natural number scalar multiplication on filters

Informal description

For a type $\alpha$ with a zero element and an addition operation, the natural number scalar multiplication operation on filters over $\alpha$ is defined by repeated pointwise addition. Specifically, for a natural number $n$ and a filter $f$ on $\alpha$, the scalar multiplication $n \bullet f$ is the filter generated by all sets obtained by adding $n$ copies of any set in $f$ to itself.

Filter.instNPow definition

[One α] [Mul α] : Pow (Filter α) ℕ

Full source

/-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
`Filter`. See Note [pointwise nat action]. -/
@[to_additive existing]
protected def instNPow [One α] [Mul α] : Pow (Filter α) ℕ :=
  ⟨fun s n => npowRec n s⟩

Natural number power of a filter

Informal description

The natural number power operation on filters over a type $\alpha$ with a multiplicative identity $1$ and a multiplication operation is defined recursively as follows: for any filter $f$ on $\alpha$ and any natural number $n$, the power $f^n$ is obtained by applying the recursive power operation `npowRec` to $f$ and $n$. Specifically: - $f^0$ is the principal filter at $1$. - $f^{n+1}$ is the product filter $f^n * f$. This operation corresponds to repeated pointwise multiplication of the filter $f$ with itself $n$ times.

Filter.instZSMul definition

[Zero α] [Add α] [Neg α] : SMul ℤ (Filter α)

Full source

/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
addition/subtraction!) of a `Filter`. See Note [pointwise nat action]. -/
protected def instZSMul [Zero α] [Add α] [Neg α] : SMul ℤ (Filter α) :=
  ⟨zsmulRec⟩

Integer scalar multiplication of filters

Informal description

The definition of scalar multiplication of a filter by an integer, where for an integer $n$ and a filter $f$ on a type $\alpha$ with zero, addition, and negation, the scalar multiplication $n \bullet f$ is defined recursively as repeated pointwise addition or subtraction (depending on the sign of $n$) of the filter $f$ with itself. This operation is implemented using the function `zsmulRec`.

Filter.instZPow definition

[One α] [Mul α] [Inv α] : Pow (Filter α) ℤ

Full source

/-- Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a `Filter`. See Note [pointwise nat action]. -/
@[to_additive existing]
protected def instZPow [One α] [Mul α] [Inv α] : Pow (Filter α) ℤ :=
  ⟨fun s n => zpowRec npowRec n s⟩

Integer power operation on filters

Informal description

For a type $\alpha$ equipped with a multiplicative identity $1$, a multiplication operation, and an inversion operation, the type `Filter α` of filters on $\alpha$ can be equipped with an integer power operation. Specifically, for any filter $f$ on $\alpha$ and any integer $n$, the power $f^n$ is defined using the recursive integer power operation `zpowRec` applied to $f$ and $n$.

Filter.semigroup definition

[Semigroup α] : Semigroup (Filter α)

Full source

/-- `Filter α` is a `Semigroup` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddSemigroup` under pointwise operations if `α` is."]
protected def semigroup [Semigroup α] : Semigroup (Filter α) where
  mul := (· * ·)
  mul_assoc _ _ _ := map₂_assoc mul_assoc

Semigroup structure on filters under pointwise multiplication

Informal description

For a type $\alpha$ equipped with a semigroup structure (i.e., an associative multiplication operation), the type `Filter α` of filters on $\alpha$ inherits a semigroup structure under pointwise multiplication. Specifically, the multiplication of two filters $f$ and $g$ is the filter generated by all sets of the form $s * t$ where $s \in f$ and $t \in g$, and this operation is associative.

Filter.commSemigroup definition

[CommSemigroup α] : CommSemigroup (Filter α)

Full source

/-- `Filter α` is a `CommSemigroup` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddCommSemigroup` under pointwise operations if `α` is."]
protected def commSemigroup [CommSemigroup α] : CommSemigroup (Filter α) :=
  { Filter.semigroup with mul_comm := fun _ _ => map₂_comm mul_comm }

Commutative semigroup structure on filters under pointwise multiplication

Informal description

For a type $\alpha$ equipped with a commutative semigroup structure (i.e., an associative and commutative multiplication operation), the type `Filter α` of filters on $\alpha$ inherits a commutative semigroup structure under pointwise multiplication. Specifically, the multiplication of two filters $f$ and $g$ is the filter generated by all sets of the form $s * t$ where $s \in f$ and $t \in g$, and this operation is both associative and commutative.

Filter.mulOneClass definition

: MulOneClass (Filter α)

Full source

/-- `Filter α` is a `MulOneClass` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddZeroClass` under pointwise operations if `α` is."]
protected def mulOneClass : MulOneClass (Filter α) where
  one := 1
  mul := (· * ·)
  one_mul := map₂_left_identity one_mul
  mul_one := map₂_right_identity mul_one

Multiplicative structure with identity on filters

Informal description

The type `Filter α` of filters on a type `α` inherits a multiplicative structure with identity from `α`. Specifically: - The multiplicative identity is the principal filter generated by the singleton set `{1}` where `1` is the multiplicative identity in `α`. - The multiplication operation on filters is defined pointwise: for any two filters `f` and `g`, their product `f * g` is the filter generated by all sets of the form `s * t` where `s ∈ f` and `t ∈ g`, with `s * t` being the pointwise product `{x * y | x ∈ s, y ∈ t}`. This structure satisfies the multiplicative identity axioms `1 * f = f` and `f * 1 = f` for any filter `f`.

Filter.mapMonoidHom definition

[MonoidHomClass F α β] (φ : F) : Filter α →* Filter β

Full source

/-- If `φ : α →* β` then `mapMonoidHom φ` is the monoid homomorphism
`Filter α →* Filter β` induced by `map φ`. -/
@[to_additive "If `φ : α →+ β` then `mapAddMonoidHom φ` is the monoid homomorphism
 `Filter α →+ Filter β` induced by `map φ`."]
def mapMonoidHom [MonoidHomClass F α β] (φ : F) : FilterFilter α →* Filter β where
  toFun := map φ
  map_one' := Filter.map_one φ
  map_mul' _ _ := Filter.map_mul φ

Induced monoid homomorphism on filters

Informal description

Given a monoid homomorphism $\varphi \colon \alpha \to \beta$, the function $\text{mapMonoidHom} \varphi$ is the induced monoid homomorphism from the monoid of filters on $\alpha$ to the monoid of filters on $\beta$, defined by mapping each filter $f$ on $\alpha$ to its image filter $\text{map} \varphi f$ on $\beta$. This homomorphism preserves the multiplicative identity and the multiplication operation on filters.

Filter.comap_mul_comap_le theorem

[MulHomClass F α β] (m : F) {f g : Filter β} : f.comap m * g.comap m ≤ (f * g).comap m

Full source

@[to_additive]
theorem comap_mul_comap_le [MulHomClass F α β] (m : F) {f g : Filter β} :
    f.comap m * g.comap m ≤ (f * g).comap m := fun _ ⟨_, ⟨t₁, ht₁, t₂, ht₂, t₁t₂⟩, mt⟩ =>
  ⟨m ⁻¹' t₁, ⟨t₁, ht₁, Subset.rfl⟩, m ⁻¹' t₂, ⟨t₂, ht₂, Subset.rfl⟩,
    (preimage_mul_preimage_subset _).trans <| (preimage_mono t₁t₂).trans mt⟩

Preimage Filter Multiplication Inequality under Homomorphism

Informal description

Let $F$ be a type of homomorphisms between multiplicative structures $\alpha$ and $\beta$ that preserve multiplication. For any homomorphism $m \in F$ and any filters $f, g$ on $\beta$, the product of the preimage filters $f \circ m^{-1}$ and $g \circ m^{-1}$ is contained in the preimage of the product filter $(f * g) \circ m^{-1}$. In other words, the following inequality holds for filters on $\alpha$: $$ (f \circ m^{-1}) * (g \circ m^{-1}) \leq (f * g) \circ m^{-1} $$

Filter.Tendsto.mul_mul theorem

 [MulHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β} :
  Tendsto m f₁ f₂ → Tendsto m g₁ g₂ → Tendsto m (f₁ * g₁) (f₂ * g₂)

Full source

@[to_additive]
theorem Tendsto.mul_mul [MulHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β} :
    Tendsto m f₁ f₂ → Tendsto m g₁ g₂ → Tendsto m (f₁ * g₁) (f₂ * g₂) := fun hf hg =>
  (Filter.map_mul m).trans_le <| mul_le_mul' hf hg

Preservation of Filter Products under Multiplication-Preserving Maps

Informal description

Let $\alpha$ and $\beta$ be types with multiplication operations, and let $F$ be a type of multiplication-preserving homomorphisms from $\alpha$ to $\beta$. Given a homomorphism $m \in F$ and filters $f_1, g_1$ on $\alpha$ and $f_2, g_2$ on $\beta$, if $m$ tends to map $f_1$ to $f_2$ and $g_1$ to $g_2$ (in the sense that preimages of $f_2$-large sets are $f_1$-large, and similarly for $g_1$ and $g_2$), then $m$ also tends to map the product filter $f_1 * g_1$ to the product filter $f_2 * g_2$.

Filter.pureMonoidHom definition

: α →* Filter α

Full source

/-- `pure` as a `MonoidHom`. -/
@[to_additive "`pure` as an `AddMonoidHom`."]
def pureMonoidHom : α →* Filter α :=
  { pureMulHom, pureOneHom with }

Monoid homomorphism from elements to principal filters

Informal description

The function maps an element $a$ of a monoid $\alpha$ to the principal filter $\{a\}$ (i.e., the filter generated by the singleton set $\{a\}$), and it preserves both the multiplicative identity and multiplication. Specifically, it satisfies: 1. $\text{pure}(1) = 1$ (where $1$ on the right is the principal filter $\{1\}$). 2. $\text{pure}(a * b) = \text{pure}(a) * \text{pure}(b)$ for all $a, b \in \alpha$. This is the bundled version of the monoid homomorphism from $\alpha$ to $\text{Filter } \alpha$.

Filter.coe_pureMonoidHom theorem

: (pureMonoidHom : α → Filter α) = pure

Full source

@[to_additive (attr := simp)]
theorem coe_pureMonoidHom : (pureMonoidHom : α → Filter α) = pure :=
  rfl

Equality of `pureMonoidHom` and `pure` functions

Informal description

The monoid homomorphism `pureMonoidHom` from a monoid $\alpha$ to the monoid of filters on $\alpha$ is equal to the `pure` function, which maps each element $a \in \alpha$ to the principal filter generated by the singleton set $\{a\}$.

Filter.pureMonoidHom_apply theorem

(a : α) : pureMonoidHom a = pure a

Full source

@[to_additive (attr := simp)]
theorem pureMonoidHom_apply (a : α) : pureMonoidHom a = pure a :=
  rfl

Principal filter as monoid homomorphism evaluation

Informal description

For any element $a$ of a monoid $\alpha$, the monoid homomorphism `pureMonoidHom` maps $a$ to the principal filter generated by the singleton set $\{a\}$, i.e., $\text{pureMonoidHom}(a) = \text{pure}(a)$.

Filter.monoid definition

: Monoid (Filter α)

Full source

/-- `Filter α` is a `Monoid` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddMonoid` under pointwise operations if `α` is."]
protected def monoid : Monoid (Filter α) :=
  { Filter.mulOneClass, Filter.semigroup, @Filter.instNPow α _ _ with }

Monoid structure on filters under pointwise operations

Informal description

The type `Filter α` of filters on a type `α` forms a monoid under pointwise operations when `α` is a monoid. Specifically: - The multiplication operation is defined pointwise: for any two filters `f` and `g`, their product `f * g` is the filter generated by all sets of the form `s * t` where `s ∈ f` and `t ∈ g`. - The multiplicative identity is the principal filter generated by the singleton set `{1}`, where `1` is the multiplicative identity in `α`. - The power operation `f^n` is defined as the pointwise multiplication of `f` with itself `n` times. This structure satisfies the monoid axioms: associativity of multiplication, and the identity laws `1 * f = f * 1 = f`.

Filter.pow_mem_pow theorem

(hs : s ∈ f) : ∀ n : ℕ, s ^ n ∈ f ^ n

Full source

@[to_additive]
theorem pow_mem_pow (hs : s ∈ f) : ∀ n : ℕ, s ^ n ∈ f ^ n
  | 0 => by
    rw [pow_zero]
    exact one_mem_one
  | n + 1 => by
    rw [pow_succ]
    exact mul_mem_mul (pow_mem_pow hs n) hs

Power sets belong to power filters: $s \in f \Rightarrow s^n \in f^n$ for all $n \in \mathbb{N}$

Informal description

For any subset $s$ of a type $\alpha$ with a monoid structure, if $s$ belongs to a filter $f$ on $\alpha$, then for every natural number $n$, the $n$-th power set $s^n$ (defined as $\{x^n \mid x \in s\}$) belongs to the $n$-th power filter $f^n$ (defined as the $n$-fold pointwise product of $f$ with itself).

Filter.bot_pow theorem

{n : ℕ} (hn : n ≠ 0) : (⊥ : Filter α) ^ n = ⊥

Full source

@[to_additive (attr := simp) nsmul_bot]
theorem bot_pow {n : ℕ} (hn : n ≠ 0) : (⊥ : Filter α) ^ n = ⊥ := by
  rw [← Nat.sub_one_add_one hn, pow_succ', bot_mul]

Bottom Filter is Absorbing under Powers: $\bot^n = \bot$ for $n \neq 0$

Informal description

For any natural number $n \neq 0$ and any type $\alpha$, the $n$-th power of the bottom filter $\bot$ (the filter containing all subsets of $\alpha$) is equal to $\bot$, i.e., $\bot^n = \bot$.

Filter.mul_top_of_one_le theorem

(hf : 1 ≤ f) : f * ⊤ = ⊤

Full source

@[to_additive]
theorem mul_top_of_one_le (hf : 1 ≤ f) : f * ⊤ = ⊤ := by
  refine top_le_iff.1 fun s => ?_
  simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]
  rintro ⟨t, ht, hs⟩
  rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

Product with Top Filter Yields Top When One is Contained

Informal description

For any filter $f$ on a monoid $\alpha$ such that the principal filter at $1$ is contained in $f$ (i.e., $1 \leq f$), the product filter $f * \top$ equals the top filter $\top$.

Filter.top_mul_of_one_le theorem

(hf : 1 ≤ f) : ⊤ * f = ⊤

Full source

@[to_additive]
theorem top_mul_of_one_le (hf : 1 ≤ f) : ⊤ * f = ⊤ := by
  refine top_le_iff.1 fun s => ?_
  simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]
  rintro ⟨t, ht, hs⟩
  rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

Product of Top Filter with Filter Containing One is Top

Informal description

For any filter $f$ on a type $\alpha$ with a multiplicative identity $1$, if the principal filter at $1$ is contained in $f$ (i.e., $1 \leq f$), then the product of the top filter (containing all subsets of $\alpha$) with $f$ is equal to the top filter, i.e., $\top * f = \top$.

Filter.top_mul_top theorem

: (⊤ : Filter α) * ⊤ = ⊤

Full source

@[to_additive (attr := simp)]
theorem top_mul_top : (⊤ : Filter α) * ⊤ = ⊤ :=
  mul_top_of_one_le le_top

Top Filter Multiplication: $\top * \top = \top$

Informal description

For any type $\alpha$ with a multiplication operation, the product of the top filter with itself equals the top filter, i.e., $\top * \top = \top$ in the filter lattice on $\alpha$.

Filter.top_pow theorem

: ∀ {n : ℕ}, n ≠ 0 → (⊤ : Filter α) ^ n = ⊤

Full source

@[to_additive nsmul_top]
theorem top_pow : ∀ {n : ℕ}, n ≠ 0 → (⊤ : Filter α) ^ n = ⊤
  | 0 => fun h => (h rfl).elim
  | 1 => fun _ => pow_one _
  | n + 2 => fun _ => by rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]

Top Filter Power Identity: $\top^n = \top$ for $n \neq 0$

Informal description

For any natural number $n \neq 0$, the $n$-th power of the top filter $\top$ on a type $\alpha$ (with a monoid structure) is equal to the top filter, i.e., $\top^n = \top$.

IsUnit.filter theorem

: IsUnit a → IsUnit (pure a : Filter α)

Full source

@[to_additive]
protected theorem _root_.IsUnit.filter : IsUnit a → IsUnit (pure a : Filter α) :=
  IsUnit.map (pureMonoidHom : α →* Filter α)

Units in Monoid Lift to Units in Filter Monoid

Informal description

If an element $a$ of a monoid $\alpha$ is a unit (i.e., has a multiplicative inverse), then the principal filter $\{a\}$ is also a unit in the monoid of filters on $\alpha$.

Filter.commMonoid definition

[CommMonoid α] : CommMonoid (Filter α)

Full source

/-- `Filter α` is a `CommMonoid` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddCommMonoid` under pointwise operations if `α` is."]
protected def commMonoid [CommMonoid α] : CommMonoid (Filter α) :=
  { Filter.mulOneClass, Filter.commSemigroup with }

Commutative monoid structure on filters under pointwise operations

Informal description

For a type $\alpha$ equipped with a commutative monoid structure (i.e., an associative and commutative multiplication operation with an identity element), the type $\text{Filter}(\alpha)$ of filters on $\alpha$ inherits a commutative monoid structure under pointwise operations. Specifically: - The multiplication of two filters $f$ and $g$ is the filter generated by all sets of the form $s \cdot t$ where $s \in f$ and $t \in g$. - The multiplicative identity is the principal filter generated by the singleton set $\{1\}$ where $1$ is the multiplicative identity in $\alpha$. - The multiplication operation is both associative and commutative.

Filter.mul_eq_one_iff theorem

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

Full source

@[to_additive]
protected theorem mul_eq_one_iff : f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1 := by
  refine ⟨fun hfg => ?_, ?_⟩
  · obtain ⟨t₁, h₁, t₂, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm ▸ one_mem_one
    have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
    rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h
    obtain ⟨a, b, rfl, rfl, h⟩ := h
    refine ⟨a, b, ?_, ?_, h⟩
    · rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]
    · rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]
  · rintro ⟨a, b, rfl, rfl, h⟩
    rw [pure_mul_pure, h, pure_one]

Characterization of when the product of two filters equals the principal filter at one

Informal description

For any filters $f$ and $g$ on a type $\alpha$ with a multiplicative identity $1$, the product filter $f * g$ equals the principal filter at $1$ if and only if there exist elements $a, b \in \alpha$ such that: 1. $f$ is the principal filter at $a$, 2. $g$ is the principal filter at $b$, and 3. $a * b = 1$ in $\alpha$.

Filter.divisionMonoid definition

: DivisionMonoid (Filter α)

Full source

/-- `Filter α` is a division monoid under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is a subtraction monoid under pointwise operations if
 `α` is."]
protected def divisionMonoid : DivisionMonoid (Filter α) :=
  { Filter.monoid, Filter.instInvolutiveInv, Filter.instDiv, Filter.instZPow (α := α) with
    mul_inv_rev := fun _ _ => map_map₂_antidistrib mul_inv_rev
    inv_eq_of_mul := fun s t h => by
      obtain ⟨a, b, rfl, rfl, hab⟩ := Filter.mul_eq_one_iff.1 h
      rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
    div_eq_mul_inv := fun _ _ => map_map₂_distrib_right div_eq_mul_inv }

Division monoid structure on filters under pointwise operations

Informal description

The type `Filter α` of filters on a type `α` forms a division monoid under pointwise operations when `α` is a division monoid. This means: 1. The multiplication of two filters $f$ and $g$ is the filter generated by all sets of the form $s \cdot t$ where $s \in f$ and $t \in g$. 2. The inversion operation maps a filter $f$ to the filter of all sets $s^{-1}$ where $s \in f$. 3. The division operation is defined as $f / g = f \cdot g^{-1}$. 4. The structure satisfies the division monoid axioms, including: - $(f \cdot g)^{-1} = g^{-1} \cdot f^{-1}$ (reverse order of inverses) - If $f \cdot g = 1$, then $f^{-1} = g$ - $f / g = f \cdot g^{-1}$ Here, $1$ denotes the principal filter generated by the singleton set $\{1\}$ where $1$ is the multiplicative identity in $\alpha$.

Filter.isUnit_iff theorem

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

Full source

@[to_additive]
theorem isUnit_iff : IsUnitIsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a := by
  constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, pure_injective ?_⟩, rfl⟩
    rw [← pure_mul_pure, ← ha, ← hb]
    exact u.inv_mul
  · rintro ⟨a, rfl, ha⟩
    exact ha.filter

Characterization of Units in the Filter Monoid: $f$ is a Unit if and only if it is a Principal Filter at a Unit Element

Informal description

A filter $f$ on a type $\alpha$ with a multiplicative structure is a unit (i.e., has a multiplicative inverse) if and only if there exists an element $a \in \alpha$ such that: 1. $f$ is the principal filter generated by $\{a\}$, and 2. $a$ is a unit in $\alpha$ (i.e., $a$ has a multiplicative inverse in $\alpha$).

Filter.divisionCommMonoid definition

[DivisionCommMonoid α] : DivisionCommMonoid (Filter α)

Full source

/-- `Filter α` is a commutative division monoid under pointwise operations if `α` is. -/
@[to_additive subtractionCommMonoid
      "`Filter α` is a commutative subtraction monoid under pointwise operations if `α` is."]
protected def divisionCommMonoid [DivisionCommMonoid α] : DivisionCommMonoid (Filter α) :=
  { Filter.divisionMonoid, Filter.commSemigroup with }

Commutative division monoid structure on filters under pointwise operations

Informal description

For a type $\alpha$ equipped with a commutative division monoid structure (i.e., an associative, commutative multiplication operation with a pseudo-inversion operation satisfying the division monoid axioms), the type `Filter α` of filters on $\alpha$ inherits a commutative division monoid structure under pointwise operations. Specifically: 1. The multiplication of two filters $f$ and $g$ is the filter generated by all sets of the form $s \cdot t$ where $s \in f$ and $t \in g$, and this operation is both associative and commutative. 2. The inversion operation maps a filter $f$ to the filter of all sets $s^{-1}$ where $s \in f$. 3. The division operation is defined as $f / g = f \cdot g^{-1}$. 4. The structure satisfies the division monoid axioms, including: - $(f \cdot g)^{-1} = g^{-1} \cdot f^{-1}$ (reverse order of inverses) - If $f \cdot g = 1$, then $f^{-1} = g$ - $f / g = f \cdot g^{-1}$ Here, $1$ denotes the principal filter generated by the singleton set $\{1\}$ where $1$ is the multiplicative identity in $\alpha$.

Filter.instDistribNeg definition

[Mul α] [HasDistribNeg α] : HasDistribNeg (Filter α)

Full source

/-- `Filter α` has distributive negation if `α` has. -/
protected def instDistribNeg [Mul α] [HasDistribNeg α] : HasDistribNeg (Filter α) :=
  { Filter.instInvolutiveNeg with
    neg_mul := fun _ _ => map₂_map_left_comm neg_mul
    mul_neg := fun _ _ => map_map₂_right_comm mul_neg }

Distributive negation on filters

Informal description

Given a type $\alpha$ with a multiplication operation and a negation operation that satisfies the distributive property over multiplication (i.e., $-(x * y) = (-x) * y = x * (-y)$ for all $x, y \in \alpha$), the filter type `Filter α` inherits a distributive negation operation. Specifically, for any filters $f$ and $g$ on $\alpha$, the negation of their product satisfies $-(f * g) = (-f) * g = f * (-g)$.

Filter.mul_add_subset theorem

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

Full source

theorem mul_add_subset : f * (g + h) ≤ f * g + f * h :=
  map₂_distrib_le_left mul_add

Subdistributivity of Filter Multiplication over Addition: $f * (g + h) \subseteq f * g + f * h$

Informal description

For any filters $f$, $g$, and $h$ on a type $\alpha$ with a multiplication operation, the filter $f * (g + h)$ is contained in the sum of the filters $f * g$ and $f * h$, i.e., $f * (g + h) \subseteq f * g + f * h$.

Filter.add_mul_subset theorem

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

Full source

theorem add_mul_subset : (f + g) * h ≤ f * h + g * h :=
  map₂_distrib_le_right add_mul

Subdistributivity of Filter Multiplication over Addition: $(f + g) * h \leq f * h + g * h$

Informal description

For any filters $f$, $g$, and $h$ on a type $\alpha$ equipped with addition and multiplication operations, the product filter $(f + g) * h$ is contained in the sum of the product filters $f * h + g * h$. In other words, every set in $f * h + g * h$ is also in $(f + g) * h$.

Filter.NeBot.mul_zero_nonneg theorem

(hf : f.NeBot) : 0 ≤ f * 0

Full source

theorem NeBot.mul_zero_nonneg (hf : f.NeBot) : 0 ≤ f * 0 :=
  le_mul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
    ⟨_, ha, _, h₂, mul_zero _⟩

Non-trivial Filter Product with Zero is Non-negative: $0 \leq f * 0$

Informal description

For any non-trivial filter $f$ on a type $\alpha$ with a multiplication operation, the zero filter $0$ is less than or equal to the product filter $f * 0$.

Filter.NeBot.zero_mul_nonneg theorem

(hg : g.NeBot) : 0 ≤ 0 * g

Full source

theorem NeBot.zero_mul_nonneg (hg : g.NeBot) : 0 ≤ 0 * g :=
  le_mul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, hb⟩ := hg.nonempty_of_mem h₂
    ⟨_, h₁, _, hb, zero_mul _⟩

Non-trivial Filter Implies $0 \leq 0 * g$

Informal description

For any non-trivial filter $g$ on a type $\alpha$ with a multiplication operation, the zero filter $0$ is less than or equal to the product filter $0 * g$. In other words, every set in $0 * g$ is also in $0$.

Filter.one_le_div_iff theorem

: 1 ≤ f / g ↔ ¬Disjoint f g

Full source

@[to_additive (attr := simp 1100)]
protected theorem one_le_div_iff : 1 ≤ f / g ↔ ¬Disjoint f g := by
  refine ⟨fun h hfg => ?_, ?_⟩
  · obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅∅ ∈ ⊥)
    exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)
  · rintro h s ⟨t₁, h₁, t₂, h₂, hs⟩
    exact hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)

Characterization of Non-Disjoint Filters via Division Inequality: $1 \leq f/g \leftrightarrow \neg\text{Disjoint}(f,g)$

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the inequality $1 \leq f / g$ holds if and only if $f$ and $g$ are not disjoint.

Filter.not_one_le_div_iff theorem

: ¬1 ≤ f / g ↔ Disjoint f g

Full source

@[to_additive]
theorem not_one_le_div_iff : ¬1 ≤ f / g¬1 ≤ f / g ↔ Disjoint f g :=
  Filter.one_le_div_iff.not_left

Disjointness of Filters via Division Inequality: $1 \not\leq f/g \leftrightarrow \text{Disjoint}(f,g)$

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the inequality $1 \not\leq f / g$ holds if and only if $f$ and $g$ are disjoint.

Filter.NeBot.one_le_div theorem

(h : f.NeBot) : 1 ≤ f / f

Full source

@[to_additive]
theorem NeBot.one_le_div (h : f.NeBot) : 1 ≤ f / f := by
  rintro s ⟨t₁, h₁, t₂, h₂, hs⟩
  obtain ⟨a, ha₁, ha₂⟩ := Set.not_disjoint_iff.1 (h.not_disjoint h₁ h₂)
  rw [mem_one, ← div_self' a]
  exact hs (Set.div_mem_div ha₁ ha₂)

Non-trivial Filters Satisfy $1 \leq f / f$

Informal description

For any non-trivial filter $f$ (i.e., $f \neq \bot$), the inequality $1 \leq f / f$ holds, where $1$ is the principal filter at the multiplicative identity and $f / f$ denotes the division of $f$ by itself.

Filter.isUnit_pure theorem

(a : α) : IsUnit (pure a : Filter α)

Full source

@[to_additive]
theorem isUnit_pure (a : α) : IsUnit (pure a : Filter α) :=
  (Group.isUnit a).filter

Principal Filter of a Singleton is a Unit in Filter Monoid

Informal description

For any element $a$ in a monoid $\alpha$, the principal filter $\{a\}$ is a unit in the monoid of filters on $\alpha$.

Filter.isUnit_iff_singleton theorem

: IsUnit f ↔ ∃ a, f = pure a

Full source

@[simp]
theorem isUnit_iff_singleton : IsUnitIsUnit f ↔ ∃ a, f = pure a := by
  simp only [isUnit_iff, Group.isUnit, and_true]

Characterization of Unit Filters as Principal Filters of Singletons

Informal description

A filter $f$ on a type $\alpha$ is a unit (i.e., has a multiplicative inverse) if and only if there exists an element $a \in \alpha$ such that $f$ is the principal filter generated by the singleton $\{a\}$.

Filter.map_inv' theorem

: f⁻¹.map m = (f.map m)⁻¹

Full source

@[to_additive]
theorem map_inv' : f⁻¹.map m = (f.map m)⁻¹ :=
  Semiconj.filter_map (map_inv m) f

Image of Inverse Filter Equals Inverse of Image Filter: $\text{map}_m(f^{-1}) = (\text{map}_m f)^{-1}$

Informal description

For any function $m \colon \alpha \to \beta$ and any filter $f$ on $\alpha$, the image filter of the inverse filter $f^{-1}$ under $m$ is equal to the inverse of the image filter of $f$ under $m$, i.e., \[ \text{map}_m(f^{-1}) = (\text{map}_m f)^{-1}. \]

Filter.Tendsto.inv_inv theorem

: Tendsto m f₁ f₂ → Tendsto m f₁⁻¹ f₂⁻¹

Full source

@[to_additive]
protected theorem Tendsto.inv_inv : Tendsto m f₁ f₂ → Tendsto m f₁⁻¹ f₂⁻¹ := fun hf =>
  (Filter.map_inv' m).trans_le <| Filter.inv_le_inv hf

Preservation of Tendency under Inversion: $\text{Tendsto } m f_1^{-1} f_2^{-1}$ given $\text{Tendsto } m f_1 f_2$

Informal description

For any function $m \colon \alpha \to \beta$ and filters $f_1$ on $\alpha$ and $f_2$ on $\beta$, if $m$ tends to $f_2$ along $f_1$, then $m$ also tends to the inverse filter $f_2^{-1}$ along the inverse filter $f_1^{-1}$.

Filter.map_div theorem

: (f / g).map m = f.map m / g.map m

Full source

@[to_additive]
protected theorem map_div : (f / g).map m = f.map m / g.map m :=
  map_map₂_distrib <| map_div m

Image of Filter Division under a Function: $\text{map } m (f / g) = (\text{map } m f) / (\text{map } m g)$

Informal description

For any function $m : \alpha \to \beta$ and any filters $f$ and $g$ on $\alpha$, the image filter of the division filter $f / g$ under $m$ is equal to the division of the image filters $f.map \, m$ and $g.map \, m$, i.e., \[ \text{map } m (f / g) = (\text{map } m f) / (\text{map } m g). \]

Filter.Tendsto.div_div theorem

(hf : Tendsto m f₁ f₂) (hg : Tendsto m g₁ g₂) : Tendsto m (f₁ / g₁) (f₂ / g₂)

Full source

@[to_additive]
protected theorem Tendsto.div_div (hf : Tendsto m f₁ f₂) (hg : Tendsto m g₁ g₂) :
    Tendsto m (f₁ / g₁) (f₂ / g₂) :=
  (Filter.map_div m).trans_le <| Filter.div_le_div hf hg

Preservation of Filter Division under Tendency: $\text{Tendsto } m (f_1 / g_1) (f_2 / g_2)$ given $\text{Tendsto } m f_1 f_2$ and $\text{Tendsto } m g_1 g_2$

Informal description

For any function $m : \alpha \to \beta$ and filters $f_1, f_2$ on $\alpha$ and $g_1, g_2$ on $\beta$, if $m$ tends to $f_2$ along $f_1$ and $m$ tends to $g_2$ along $g_1$, then $m$ tends to the filter division $f_2 / g_2$ along the filter division $f_1 / g_1$. In other words, the following implication holds: \[ (\lim_{f_1} m \in f_2) \land (\lim_{g_1} m \in g_2) \implies \lim_{f_1 / g_1} m \in f_2 / g_2. \]

Filter.NeBot.div_zero_nonneg theorem

(hf : f.NeBot) : 0 ≤ f / 0

Full source

theorem NeBot.div_zero_nonneg (hf : f.NeBot) : 0 ≤ f / 0 :=
  Filter.le_div_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
    ⟨_, ha, _, h₂, div_zero _⟩

Non-trivial Filter Divided by Zero is Non-negative

Informal description

For any non-trivial filter $f$ on a type $\alpha$, the division filter $f / 0$ is greater than or equal to the zero filter, i.e., $0 \leq f / 0$.

Filter.NeBot.zero_div_nonneg theorem

(hg : g.NeBot) : 0 ≤ 0 / g

Full source

theorem NeBot.zero_div_nonneg (hg : g.NeBot) : 0 ≤ 0 / g :=
  Filter.le_div_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, hb⟩ := hg.nonempty_of_mem h₂
    ⟨_, h₁, _, hb, zero_div _⟩

Non-negativity of Zero Divided by a Non-trivial Filter

Informal description

For any non-trivial filter $g$ on a type $\alpha$, the filter $0 / g$ is non-negative, i.e., $0 \leq 0 / g$.

Filter.instSMul definition

: SMul (Filter α) (Filter β)

Full source

/-- The filter `f • g` is generated by `{s • t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
@[to_additive "The filter `f +ᵥ g` is generated by `{s +ᵥ t | s ∈ f, t ∈ g}` in locale
 `Pointwise`."]
protected def instSMul : SMul (Filter α) (Filter β) :=
  ⟨/- This is defeq to `map₂ (· • ·) f g`, but the hypothesis unfolds to `t₁ • t₂ ⊆ s`
  rather than all the way to `Set.image2 (· • ·) t₁ t₂ ⊆ s`. -/
  fun f g => { map₂ (· • ·) f g with sets := { s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ s } }⟩

Scalar multiplication of filters

Informal description

The scalar multiplication operation on filters is defined such that for any filters $ f $ on $ \alpha $ and $ g $ on $ \beta $, the filter $ f \bullet g $ is generated by all subsets $ t $ of $ \beta $ for which there exist subsets $ t_1 \in f $ and $ t_2 \in g $ such that the pointwise scalar multiplication $ t_1 \bullet t_2 $ is contained in $ t $.

Filter.map₂_smul theorem

: map₂ (· • ·) f g = f • g

Full source

@[to_additive (attr := simp)]
theorem map₂_smul : map₂ (· • ·) f g = f • g :=
  rfl

Equality of Pointwise Scalar Multiplication and Filter Scalar Multiplication

Informal description

For any filters $f$ and $g$, the filter generated by the pointwise scalar multiplication of sets from $f$ and $g$ is equal to the scalar multiplication of the filters $f$ and $g$, i.e., $\text{map}_2 (\cdot \bullet \cdot) f g = f \bullet g$.

Filter.mem_smul theorem

: t ∈ f • g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ t

Full source

@[to_additive]
theorem mem_smul : t ∈ f • gt ∈ f • g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ t :=
  Iff.rfl

Membership Criterion for Scalar Multiplication of Filters

Informal description

A subset $t$ belongs to the scalar multiplication filter $f \bullet g$ if and only if there exist subsets $t_1 \in f$ and $t_2 \in g$ such that the pointwise scalar multiplication $t_1 \bullet t_2$ is contained in $t$.

Filter.smul_mem_smul theorem

: s ∈ f → t ∈ g → s • t ∈ f • g

Full source

@[to_additive]
theorem smul_mem_smul : s ∈ f → t ∈ g → s • t ∈ f • g :=
  image2_mem_map₂

Membership Preservation under Pointwise Scalar Multiplication of Filters

Informal description

For any subsets $s$ of $\alpha$ and $t$ of $\beta$, if $s$ belongs to the filter $f$ on $\alpha$ and $t$ belongs to the filter $g$ on $\beta$, then the pointwise scalar multiplication $s \bullet t$ belongs to the filter $f \bullet g$ on $\beta$.

Filter.bot_smul theorem

: (⊥ : Filter α) • g = ⊥

Full source

@[to_additive (attr := simp)]
theorem bot_smul : (⊥ : Filter α) • g = ⊥ :=
  map₂_bot_left

Bottom filter scalar multiplication: $\bot \bullet g = \bot$

Informal description

For any filter $g$ on a type $\beta$, the scalar multiplication of the bottom filter $\bot$ on $\alpha$ with $g$ equals the bottom filter on $\beta$, i.e., $\bot \bullet g = \bot$.

Filter.smul_bot theorem

: f • (⊥ : Filter β) = ⊥

Full source

@[to_additive (attr := simp)]
theorem smul_bot : f • (⊥ : Filter β) = ⊥ :=
  map₂_bot_right

Scalar Multiplication with Bottom Filter Yields Bottom Filter

Informal description

For any filter $f$ on a type $\alpha$, the scalar multiplication of $f$ with the bottom filter $\bot$ on a type $\beta$ equals the bottom filter $\bot$ on $\beta$, i.e., $f \bullet \bot = \bot$.

Filter.smul_eq_bot_iff theorem

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

Full source

@[to_additive (attr := simp)]
theorem smul_eq_bot_iff : f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
  map₂_eq_bot_iff

Scalar Multiplication Filter is Trivial if and only if Either Factor is Trivial

Informal description

For any filters $f$ on a type $\alpha$ and $g$ on a type $\beta$, the scalar multiplication filter $f \bullet g$ is equal to the bottom filter $\bot$ if and only if either $f$ or $g$ is equal to $\bot$.

Filter.smul_neBot_iff theorem

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

Full source

@[to_additive (attr := simp)]
theorem smul_neBot_iff : (f • g).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff

Non-triviality of Scalar Multiplication Filter: $f \bullet g$ is non-trivial iff $f$ and $g$ are non-trivial

Informal description

For any filters $f$ on a type $\alpha$ and $g$ on a type $\beta$, the scalar multiplication filter $f \bullet g$ is non-trivial if and only if both $f$ and $g$ are non-trivial filters.

Filter.NeBot.smul theorem

: NeBot f → NeBot g → NeBot (f • g)

Full source

@[to_additive]
protected theorem NeBot.smul : NeBot f → NeBot g → NeBot (f • g) :=
  NeBot.map₂

Non-triviality of scalar multiplication of non-trivial filters

Informal description

If $f$ and $g$ are non-trivial filters on types $\alpha$ and $\beta$ respectively, then their scalar multiplication $f \bullet g$ is also a non-trivial filter on $\beta$.

Filter.NeBot.of_smul_left theorem

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

Full source

@[to_additive]
theorem NeBot.of_smul_left : (f • g).NeBot → f.NeBot :=
  NeBot.of_map₂_left

Non-triviality of left factor in scalar multiplication of filters

Informal description

If the scalar multiplication filter $f \bullet g$ is non-trivial, then the filter $f$ is non-trivial.

Filter.NeBot.of_smul_right theorem

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

Full source

@[to_additive]
theorem NeBot.of_smul_right : (f • g).NeBot → g.NeBot :=
  NeBot.of_map₂_right

Non-triviality of right filter in scalar multiplication

Informal description

If the scalar multiplication filter $f \bullet g$ is non-trivial (i.e., does not contain the empty set), then the filter $g$ must also be non-trivial.

Filter.smul.instNeBot theorem

[NeBot f] [NeBot g] : NeBot (f • g)

Full source

@[to_additive vadd.instNeBot]
lemma smul.instNeBot [NeBot f] [NeBot g] : NeBot (f • g) := .smul ‹_› ‹_›

Non-triviality of scalar multiplication of non-trivial filters

Informal description

If $f$ is a non-trivial filter on a type $\alpha$ and $g$ is a non-trivial filter on a type $\beta$, then their scalar multiplication $f \bullet g$ is also a non-trivial filter on $\beta$.

Filter.pure_smul theorem

: (pure a : Filter α) • g = g.map (a • ·)

Full source

@[to_additive (attr := simp)]
theorem pure_smul : (pure a : Filter α) • g = g.map (a • ·) :=
  map₂_pure_left

Scalar multiplication of pure filter equals image under scalar action

Informal description

For any element $a$ of type $\alpha$ and any filter $g$ on type $\beta$, the scalar multiplication of the pure filter $\text{pure } a$ with $g$ is equal to the image filter of $g$ under the function $x \mapsto a \bullet x$.

Filter.smul_pure theorem

: f • pure b = f.map (· • b)

Full source

@[to_additive (attr := simp)]
theorem smul_pure : f • pure b = f.map (· • b) :=
  map₂_pure_right

Scalar Multiplication of Filter with Pure Filter: $f \bullet \text{pure } b = \text{map } (\lambda a, a \bullet b) f$

Informal description

For any filter $f$ on a type $\alpha$ and any element $b$ of a type $\beta$, the scalar multiplication of $f$ with the pure filter generated by $b$ is equal to the image filter of $f$ under the function $\lambda a, a \bullet b$.

Filter.pure_smul_pure theorem

: (pure a : Filter α) • (pure b : Filter β) = pure (a • b)

Full source

@[to_additive]
theorem pure_smul_pure : (pure a : Filter α) • (pure b : Filter β) = pure (a • b) := by simp

Pure Filter Scalar Multiplication Identity: $\text{pure } a \bullet \text{pure } b = \text{pure } (a \bullet b)$

Informal description

For any elements $a$ in type $\alpha$ and $b$ in type $\beta$, the scalar multiplication of the pure filter generated by $a$ with the pure filter generated by $b$ equals the pure filter generated by the scalar product $a \bullet b$. In other words, $\text{pure } a \bullet \text{pure } b = \text{pure } (a \bullet b)$.

Filter.smul_le_smul theorem

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

Full source

@[to_additive]
theorem smul_le_smul : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ • g₁ ≤ f₂ • g₂ :=
  map₂_mono

Monotonicity of Pointwise Scalar Multiplication of Filters

Informal description

For any filters $f_1, f_2$ on a type $\alpha$ and $g_1, g_2$ on a type $\beta$, if $f_1 \leq f_2$ and $g_1 \leq g_2$, then the pointwise scalar multiplication satisfies $f_1 \bullet g_1 \leq f_2 \bullet g_2$.

Filter.smul_le_smul_left theorem

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

Full source

@[to_additive]
theorem smul_le_smul_left : g₁ ≤ g₂ → f • g₁ ≤ f • g₂ :=
  map₂_mono_left

Monotonicity of scalar multiplication of filters with respect to the right operand

Informal description

For any filters $g_1$ and $g_2$ on a type $\beta$ and any filter $f$ on a type $\alpha$, if $g_1 \leq g_2$ in the partial order of filters, then the scalar multiplication $f \bullet g_1 \leq f \bullet g_2$.

Filter.smul_le_smul_right theorem

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

Full source

@[to_additive]
theorem smul_le_smul_right : f₁ ≤ f₂ → f₁ • g ≤ f₂ • g :=
  map₂_mono_right

Monotonicity of scalar multiplication with respect to the right filter

Informal description

For any filters $f_1$, $f_2$ on a type $\alpha$ and any filter $g$ on a type $\beta$, if $f_1 \leq f_2$ in the partial order of filters, then the scalar multiplication $f_1 \bullet g \leq f_2 \bullet g$ in the partial order of filters on $\beta$.

Filter.le_smul_iff theorem

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

Full source

@[to_additive (attr := simp)]
theorem le_smul_iff : h ≤ f • g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s • t ∈ h :=
  le_map₂_iff

Characterization of Filter Inequality under Pointwise Scalar Multiplication

Informal description

For filters $h$, $f$, and $g$ on appropriate types, the filter $h$ is less than or equal to the pointwise scalar multiplication filter $f \bullet g$ if and only if for every set $s$ in $f$ and every set $t$ in $g$, the pointwise scalar multiplication $s \bullet t$ is in $h$.

Filter.covariant_smul instance

: CovariantClass (Filter α) (Filter β) (· • ·) (· ≤ ·)

Full source

@[to_additive]
instance covariant_smul : CovariantClass (Filter α) (Filter β) (· • ·) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_left⟩

Order-Preserving Property of Pointwise Scalar Multiplication on Filters

Informal description

For any type $\alpha$ acting on a type $\beta$ via a scalar multiplication operation $\cdot \bullet \cdot$, the operation of pointwise scalar multiplication on filters preserves the partial order relation $\leq$ on filters. That is, for any filters $f_1, f_2$ on $\alpha$ and $g$ on $\beta$, if $f_1 \leq f_2$, then $f_1 \bullet g \leq f_2 \bullet g$.

Filter.instVSub definition

: VSub (Filter α) (Filter β)

Full source

/-- The filter `f -ᵥ g` is generated by `{s -ᵥ t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
protected def instVSub : VSub (Filter α) (Filter β) :=
  ⟨/- This is defeq to `map₂ (-ᵥ) f g`, but the hypothesis unfolds to `t₁ -ᵥ t₂ ⊆ s` rather than all
  the way to `Set.image2 (-ᵥ) t₁ t₂ ⊆ s`. -/
  fun f g => { map₂ (· -ᵥ ·) f g with sets := { s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s } }⟩

Pointwise subtraction of filters

Informal description

The filter $ f -ᵥ g $ is generated by all sets of the form $ s -ᵥ t $ where $ s \in f $ and $ t \in g $, i.e., it consists of all subsets $ U $ of $ \alpha $ for which there exist $ s \in f $ and $ t \in g $ such that the pointwise subtraction $ s -ᵥ t $ is contained in $ U $.

Filter.map₂_vsub theorem

: map₂ (· -ᵥ ·) f g = f -ᵥ g

Full source

@[simp]
theorem map₂_vsub : map₂ (· -ᵥ ·) f g = f -ᵥ g :=
  rfl

Equality of Mapped Pointwise Subtraction and Filter Subtraction

Informal description

For any filters $f$ and $g$ on a type $\alpha$, the image of the pointwise subtraction operation under the `map₂` function equals the pointwise subtraction of the filters, i.e., $\text{map}_2 (· -ᵥ ·) f g = f -ᵥ g$.

Filter.mem_vsub theorem

{s : Set α} : s ∈ f -ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s

Full source

theorem mem_vsub {s : Set α} : s ∈ f -ᵥ gs ∈ f -ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s :=
  Iff.rfl

Membership Criterion for Pointwise Subtraction Filter

Informal description

A set $s$ belongs to the pointwise subtraction filter $f -ᵥ g$ if and only if there exist sets $t_1 \in f$ and $t_2 \in g$ such that the pointwise subtraction $t_1 -ᵥ t_2$ is a subset of $s$.

Filter.vsub_mem_vsub theorem

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

Full source

theorem vsub_mem_vsub : s ∈ f → t ∈ g → s -ᵥ ts -ᵥ t ∈ f -ᵥ g :=
  image2_mem_map₂

Pointwise subtraction of sets in filters

Informal description

For any sets $s$ and $t$ in the filters $f$ and $g$ respectively, the pointwise subtraction $s -ᵥ t$ belongs to the filter $f -ᵥ g$.

Filter.bot_vsub theorem

: (⊥ : Filter β) -ᵥ g = ⊥

Full source

@[simp]
theorem bot_vsub : (⊥ : Filter β) -ᵥ g = ⊥ :=
  map₂_bot_left

Bottom Filter is Absorbing under Pointwise Subtraction

Informal description

For any filter $g$ on a type $\beta$, the pointwise subtraction of the bottom filter $\bot$ (the filter containing all subsets of $\beta$) with $g$ is equal to the bottom filter, i.e., $\bot -ᵥ g = \bot$.

Filter.vsub_bot theorem

: f -ᵥ (⊥ : Filter β) = ⊥

Full source

@[simp]
theorem vsub_bot : f -ᵥ (⊥ : Filter β) = ⊥ :=
  map₂_bot_right

Pointwise Subtraction with Bottom Filter Yields Bottom Filter

Informal description

For any filter $f$ on a type $\alpha$, the pointwise subtraction of $f$ with the bottom filter $\bot$ on a type $\beta$ is equal to the bottom filter, i.e., $f -ᵥ \bot = \bot$.

Filter.vsub_eq_bot_iff theorem

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

Full source

@[simp]
theorem vsub_eq_bot_iff : f -ᵥ gf -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
  map₂_eq_bot_iff

Characterization of Triviality in Pointwise Subtraction of Filters

Informal description

For filters $f$ and $g$, the pointwise subtraction filter $f -ᵥ g$ is equal to the bottom filter $\bot$ if and only if either $f$ is the bottom filter or $g$ is the bottom filter. In other words, $f -ᵥ g = \bot \leftrightarrow f = \bot \lor g = \bot$.

Filter.vsub_neBot_iff theorem

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

Full source

@[simp]
theorem vsub_neBot_iff : (f -ᵥ g : Filter α).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff

Non-triviality of Pointwise Subtraction Filter: $f -ᵥ g \neq \bot \leftrightarrow f \neq \bot \land g \neq \bot$

Informal description

The pointwise subtraction filter $f -ᵥ g$ is non-trivial if and only if both filters $f$ and $g$ are non-trivial.

Filter.NeBot.vsub theorem

: NeBot f → NeBot g → NeBot (f -ᵥ g)

Full source

protected theorem NeBot.vsub : NeBot f → NeBot g → NeBot (f -ᵥ g) :=
  NeBot.map₂

Non-triviality of Pointwise Subtraction of Non-trivial Filters

Informal description

If $f$ and $g$ are non-trivial filters on a type $\alpha$, then their pointwise subtraction $f -ᵥ g$ is also a non-trivial filter.

Filter.NeBot.of_vsub_left theorem

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

Full source

theorem NeBot.of_vsub_left : (f -ᵥ g : Filter α).NeBot → f.NeBot :=
  NeBot.of_map₂_left

Non-triviality of the left filter in pointwise subtraction

Informal description

If the pointwise subtraction filter $f -ᵥ g$ on a type $\alpha$ is non-trivial (i.e., does not contain the empty set), then the filter $f$ is also non-trivial.

Filter.NeBot.of_vsub_right theorem

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

Full source

theorem NeBot.of_vsub_right : (f -ᵥ g : Filter α).NeBot → g.NeBot :=
  NeBot.of_map₂_right

Non-triviality of Right Filter in Pointwise Subtraction

Informal description

If the pointwise subtraction filter $f -ᵥ g$ on a type $\alpha$ is non-trivial (i.e., does not contain the empty set), then the filter $g$ on $\beta$ is also non-trivial.

Filter.vsub.instNeBot theorem

[NeBot f] [NeBot g] : NeBot (f -ᵥ g)

Full source

lemma vsub.instNeBot [NeBot f] [NeBot g] : NeBot (f -ᵥ g) := .vsub ‹_› ‹_›

Non-triviality of pointwise subtraction of non-trivial filters

Informal description

If $f$ and $g$ are non-trivial filters, then their pointwise subtraction $f -ᵥ g$ is also non-trivial.

Filter.pure_vsub theorem

: (pure a : Filter β) -ᵥ g = g.map (a -ᵥ ·)

Full source

@[simp]
theorem pure_vsub : (pure a : Filter β) -ᵥ g = g.map (a -ᵥ ·) :=
  map₂_pure_left

Pointwise subtraction of pure filter equals image under subtraction function

Informal description

For any element $a$ in $\beta$ and any filter $g$ on $\beta$, the pointwise subtraction of the pure filter $\text{pure } a$ and $g$ is equal to the image filter of $g$ under the function $x \mapsto a -ᵥ x$.

Filter.vsub_pure theorem

: f -ᵥ pure b = f.map (· -ᵥ b)

Full source

@[simp]
theorem vsub_pure : f -ᵥ pure b = f.map (· -ᵥ b) :=
  map₂_pure_right

Pointwise subtraction of a filter by a pure element equals image under subtraction by $b$

Informal description

For any filter $f$ on a type $\beta$ and any element $b \in \beta$, the pointwise subtraction filter $f -ᵥ \text{pure } b$ is equal to the image filter of $f$ under the function $x \mapsto x -ᵥ b$.

Filter.pure_vsub_pure theorem

: (pure a : Filter β) -ᵥ pure b = (pure (a -ᵥ b) : Filter α)

Full source

theorem pure_vsub_pure : (pure a : Filter β) -ᵥ pure b = (pure (a -ᵥ b) : Filter α) := by simp

Pointwise subtraction of pure filters: $\text{pure } a -ᵥ \text{pure } b = \text{pure } (a -ᵥ b)$

Informal description

For any elements $a$ in $\beta$ and $b$ in $\beta$, the pointwise subtraction of the pure filter $\text{pure } a$ and the pure filter $\text{pure } b$ is equal to the pure filter generated by the single element $a -ᵥ b$.

Filter.vsub_le_vsub theorem

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

Full source

theorem vsub_le_vsub : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ -ᵥ g₁ ≤ f₂ -ᵥ g₂ :=
  map₂_mono

Monotonicity of Pointwise Subtraction of Filters

Informal description

For any filters $f_1, f_2$ on a type $\alpha$ and $g_1, g_2$ on a type $\beta$, if $f_1 \leq f_2$ and $g_1 \leq g_2$, then the pointwise subtraction filter $f_1 -ᵥ g_1$ is less than or equal to $f_2 -ᵥ g_2$.

Filter.vsub_le_vsub_left theorem

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

Full source

theorem vsub_le_vsub_left : g₁ ≤ g₂ → f -ᵥ g₁ ≤ f -ᵥ g₂ :=
  map₂_mono_left

Monotonicity of Filter Subtraction in Second Argument

Informal description

For any filters $g₁$ and $g₂$ on a type $\beta$, if $g₁ \leq g₂$, then for any filter $f$ on $\beta$, the pointwise subtraction $f -ᵥ g₁$ is less than or equal to $f -ᵥ g₂$.

Filter.vsub_le_vsub_right theorem

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

Full source

theorem vsub_le_vsub_right : f₁ ≤ f₂ → f₁ -ᵥ g ≤ f₂ -ᵥ g :=
  map₂_mono_right

Monotonicity of pointwise subtraction in the first argument

Informal description

For any filters $f_1$, $f_2$, and $g$ on types $\alpha$ and $\beta$, if $f_1 \subseteq f_2$, then the pointwise subtraction filter $f_1 -ᵥ g$ is contained in $f_2 -ᵥ g$.

Filter.le_vsub_iff theorem

: h ≤ f -ᵥ g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s -ᵥ t ∈ h

Full source

@[simp]
theorem le_vsub_iff : h ≤ f -ᵥ g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s -ᵥ t ∈ h :=
  le_map₂_iff

Characterization of Filter Inequality via Pointwise Subtraction

Informal description

For filters $h$, $f$, and $g$ on appropriate types, the inequality $h \leq f -ᵥ g$ holds if and only if for every set $s$ in $f$ and every set $t$ in $g$, the pointwise subtraction $s -ᵥ t$ is in $h$.

Filter.instSMulFilter definition

: SMul α (Filter β)

Full source

/-- `a • f` is the map of `f` under `a •` in locale `Pointwise`. -/
@[to_additive "`a +ᵥ f` is the map of `f` under `a +ᵥ` in locale `Pointwise`."]
protected def instSMulFilter : SMul α (Filter β) :=
  ⟨fun a => map (a • ·)⟩

Scalar multiplication of a filter by an element

Informal description

Given a scalar multiplication operation `•` between types `α` and `β`, the scalar multiplication of a filter `f` on `β` by an element `a` of `α` is defined as the image filter of `f` under the function `a • · : β → β`. In other words, a set `s` is in the filter `a • f` if and only if the preimage of `s` under the function `b ↦ a • b` is in `f`.

Filter.map_smul theorem

: map (fun b => a • b) f = a • f

Full source

@[to_additive (attr := simp)]
protected theorem map_smul : map (fun b => a • b) f = a • f :=
  rfl

Image Filter under Scalar Multiplication Equals Scalar Multiplication of Filter

Informal description

For any element $a$ of type $\alpha$ and any filter $f$ on type $\beta$, the image filter of $f$ under the function $b \mapsto a \cdot b$ is equal to the scalar multiplication of $f$ by $a$, i.e., $\text{map} (b \mapsto a \cdot b) f = a \cdot f$.

Filter.mem_smul_filter theorem

: s ∈ a • f ↔ (a • ·) ⁻¹' s ∈ f

Full source

@[to_additive]
theorem mem_smul_filter : s ∈ a • fs ∈ a • f ↔ (a • ·) ⁻¹' s ∈ f := Iff.rfl

Membership Criterion for Scalar Multiplication of a Filter: $s \in a \bullet f \leftrightarrow (a \bullet \cdot)^{-1}(s) \in f$

Informal description

For a scalar multiplication operation `•` between types `α` and `β`, a set `s` belongs to the filter `a • f` (where `a ∈ α` and `f` is a filter on `β`) if and only if the preimage of `s` under the function `b ↦ a • b` belongs to `f`. In other words, $s \in a \bullet f \leftrightarrow \{b \in \beta \mid a \bullet b \in s\} \in f$.

Filter.smul_set_mem_smul_filter theorem

: s ∈ f → a • s ∈ a • f

Full source

@[to_additive]
theorem smul_set_mem_smul_filter : s ∈ f → a • s ∈ a • f :=
  image_mem_map

Scaled Set Belongs to Scaled Filter

Informal description

For any element $a$ of type $\alpha$ and any set $s$ in a filter $f$ on type $\beta$, the scaled set $a \cdot s$ belongs to the scaled filter $a \cdot f$.

Filter.smul_filter_bot theorem

: a • (⊥ : Filter β) = ⊥

Full source

@[to_additive (attr := simp)]
theorem smul_filter_bot : a • (⊥ : Filter β) = ⊥ :=
  map_bot

Scalar multiplication preserves the bottom filter

Informal description

For any scalar $a$ in type $\alpha$ and the bottom filter $\bot$ on type $\beta$, the scalar multiplication of $\bot$ by $a$ equals $\bot$, i.e., $a \bullet \bot = \bot$.

Filter.smul_filter_eq_bot_iff theorem

: a • f = ⊥ ↔ f = ⊥

Full source

@[to_additive (attr := simp)]
theorem smul_filter_eq_bot_iff : a • f = ⊥ ↔ f = ⊥ :=
  map_eq_bot_iff

Scalar Multiplication of Filter is Bottom iff Original Filter is Bottom

Informal description

For any scalar $a$ in a type $\alpha$ and any filter $f$ on a type $\beta$, the scalar-multiplied filter $a \bullet f$ is equal to the bottom filter $\bot$ if and only if $f$ is equal to $\bot$.

Filter.smul_filter_neBot_iff theorem

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

Full source

@[to_additive (attr := simp)]
theorem smul_filter_neBot_iff : (a • f).NeBot ↔ f.NeBot :=
  map_neBot_iff _

Non-triviality of Scalar-Multiplied Filter $\leftrightarrow$ Non-triviality of Original Filter

Informal description

For any scalar $a$ and any filter $f$ on a type $\beta$, the scalar-multiplied filter $a \bullet f$ is non-trivial if and only if $f$ is non-trivial.

Filter.NeBot.smul_filter theorem

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

Full source

@[to_additive]
theorem NeBot.smul_filter : f.NeBot → (a • f).NeBot := fun h => h.map _

Non-triviality Preservation under Scalar Multiplication of Filters

Informal description

If a filter $f$ on a type $\beta$ is non-trivial, then for any scalar $a$ in a type $\alpha$, the scalar-multiplied filter $a \bullet f$ is also non-trivial.

Filter.NeBot.of_smul_filter theorem

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

Full source

@[to_additive]
theorem NeBot.of_smul_filter : (a • f).NeBot → f.NeBot :=
  NeBot.of_map

Non-triviality of Original Filter from Non-triviality of Scalar-Multiplied Filter

Informal description

For any scalar $a$ and any filter $f$ on a type $\beta$, if the scalar-multiplied filter $a \bullet f$ is non-trivial, then $f$ is non-trivial.

Filter.smul_filter.instNeBot theorem

[NeBot f] : NeBot (a • f)

Full source

@[to_additive vadd_filter.instNeBot]
lemma smul_filter.instNeBot [NeBot f] : NeBot (a • f) := .smul_filter ‹_›

Non-triviality preservation under scalar multiplication of filters

Informal description

If a filter $f$ on a type $\beta$ is non-trivial (i.e., does not contain the empty set), then for any scalar $a$ in a type $\alpha$, the scalar-multiplied filter $a \bullet f$ is also non-trivial.

Filter.smul_filter_le_smul_filter theorem

(hf : f₁ ≤ f₂) : a • f₁ ≤ a • f₂

Full source

@[to_additive]
theorem smul_filter_le_smul_filter (hf : f₁ ≤ f₂) : a • f₁ ≤ a • f₂ :=
  map_mono hf

Monotonicity of Scalar Multiplication on Filters

Informal description

For any filters $f_1$ and $f_2$ on a type $\beta$ and any element $a$ of a type $\alpha$, if $f_1 \leq f_2$ in the partial order of filters, then the scalar multiplication $a \bullet f_1 \leq a \bullet f_2$.

Filter.covariant_smul_filter instance

: CovariantClass α (Filter β) (· • ·) (· ≤ ·)

Full source

@[to_additive]
instance covariant_smul_filter : CovariantClass α (Filter β) (· • ·) (· ≤ ·) :=
  ⟨fun _ => @map_mono β β _⟩

Scalar Multiplication Preserves Filter Order

Informal description

For any type $\alpha$ acting on a type $\beta$ via a scalar multiplication operation $\cdot \bullet \cdot : \alpha \to \beta \to \beta$, the scalar multiplication operation on filters preserves the partial order relation $\leq$ on filters. That is, for any $a \in \alpha$ and any filters $f_1, f_2$ on $\beta$, if $f_1 \leq f_2$, then $a \bullet f_1 \leq a \bullet f_2$.

Filter.smulCommClass_filter instance

[SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Filter γ)

Full source

@[to_additive]
instance smulCommClass_filter [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass α β (Filter γ) :=
  ⟨fun _ _ _ => map_comm (funext <| smul_comm _ _) _⟩

Commutativity of Scalar Multiplication on Filters

Informal description

Given types $\alpha$, $\beta$, and $\gamma$ equipped with scalar multiplication operations, if the scalar multiplications on $\alpha$ and $\beta$ commute when acting on $\gamma$ (i.e., $a \bullet (b \bullet c) = b \bullet (a \bullet c)$ for all $a \in \alpha$, $b \in \beta$, $c \in \gamma$), then the scalar multiplication operations on $\alpha$ and $\beta$ also commute when acting on filters over $\gamma$.

Filter.smulCommClass_filter' instance

[SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Filter β) (Filter γ)

Full source

@[to_additive]
instance smulCommClass_filter' [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass α (Filter β) (Filter γ) :=
  ⟨fun a _ _ => map_map₂_distrib_right <| smul_comm a⟩

Commutativity of Scalar Multiplication with Filter Scalar Multiplication

Informal description

Given types $\alpha$, $\beta$, and $\gamma$ with scalar multiplication operations, if the scalar multiplications on $\alpha$ and $\beta$ commute when acting on $\gamma$ (i.e., $a \bullet (b \bullet c) = b \bullet (a \bullet c)$ for all $a \in \alpha$, $b \in \beta$, $c \in \gamma$), then the scalar multiplication by elements of $\alpha$ commutes with the filter scalar multiplication by filters over $\beta$ when acting on filters over $\gamma$.

Filter.smulCommClass_filter'' instance

[SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Filter α) β (Filter γ)

Full source

@[to_additive]
instance smulCommClass_filter'' [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass (Filter α) β (Filter γ) :=
  haveI := SMulCommClass.symm α β γ
  SMulCommClass.symm _ _ _

Commutativity of Filter Scalar Multiplication with Element Scalar Multiplication

Informal description

For types $\alpha$, $\beta$, and $\gamma$ equipped with scalar multiplication operations, if the scalar multiplications on $\alpha$ and $\beta$ commute when acting on $\gamma$ (i.e., $a \bullet (b \bullet c) = b \bullet (a \bullet c)$ for all $a \in \alpha$, $b \in \beta$, $c \in \gamma$), then the scalar multiplication by filters over $\alpha$ commutes with the scalar multiplication by elements of $\beta$ when acting on filters over $\gamma$.

Filter.smulCommClass instance

[SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Filter α) (Filter β) (Filter γ)

Full source

@[to_additive]
instance smulCommClass [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass (Filter α) (Filter β) (Filter γ) :=
  ⟨fun _ _ _ => map₂_left_comm smul_comm⟩

Commutativity of Scalar Multiplication on Filters

Informal description

For any types $\alpha$, $\beta$, and $\gamma$ equipped with scalar multiplication operations, if the scalar multiplications on $\alpha$ and $\beta$ commute with each other when acting on $\gamma$, then the corresponding scalar multiplication operations on filters over $\alpha$, $\beta$, and $\gamma$ also commute.

Filter.isScalarTower instance

[SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Filter γ)

Full source

@[to_additive]
instance isScalarTower [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower α β (Filter γ) :=
  ⟨fun a b f => by simp only [← Filter.map_smul, map_map, smul_assoc]; rfl⟩

Scalar Tower Property for Filters with Fixed Scalars

Informal description

For types $\alpha$, $\beta$, and $\gamma$ equipped with scalar multiplication operations, if the scalar multiplications satisfy the scalar tower property $(a \cdot b) \cdot c = a \cdot (b \cdot c)$ for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, then the scalar multiplication operations on filters over $\gamma$ also satisfy the scalar tower property with respect to $\alpha$ and $\beta$. That is, for any $a \in \alpha$, $b \in \beta$, and filter $h$ on $\gamma$, the scalar multiplication operations satisfy $(a \cdot b) \bullet h = a \bullet (b \bullet h)$.

Filter.isScalarTower' instance

[SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α (Filter β) (Filter γ)

Full source

@[to_additive]
instance isScalarTower' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower α (Filter β) (Filter γ) :=
  ⟨fun a f g => by
    refine (map_map₂_distrib_left fun _ _ => ?_).symm
    exact (smul_assoc a _ _).symm⟩

Scalar Tower Property for Filters with Fixed First Argument

Informal description

For types $\alpha$, $\beta$, and $\gamma$ equipped with scalar multiplication operations, if the scalar multiplications satisfy the scalar tower property $(a \cdot b) \cdot c = a \cdot (b \cdot c)$ for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, then the scalar multiplication operations on filters over these types also satisfy the scalar tower property. That is, for any filter $f$ on $\alpha$ and filters $g$ on $\beta$ and $h$ on $\gamma$, the scalar multiplication operations satisfy $(f \bullet g) \bullet h = f \bullet (g \bullet h)$.

Filter.isScalarTower'' instance

[SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower (Filter α) (Filter β) (Filter γ)

Full source

@[to_additive]
instance isScalarTower'' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower (Filter α) (Filter β) (Filter γ) :=
  ⟨fun _ _ _ => map₂_assoc smul_assoc⟩

Scalar Tower Property for Filters

Informal description

For types $\alpha$, $\beta$, and $\gamma$ equipped with scalar multiplication operations and satisfying the scalar tower property $[SMul \alpha \beta]$, $[SMul \alpha \gamma]$, $[SMul \beta \gamma]$, and $[IsScalarTower \alpha \beta \gamma]$, the filters on these types also satisfy the scalar tower property. That is, for any filters $f$ on $\alpha$, $g$ on $\beta$, and $h$ on $\gamma$, the scalar multiplication operations satisfy $(f \bullet g) \bullet h = f \bullet (g \bullet h)$.

Filter.isCentralScalar instance

[SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Filter β)

Full source

@[to_additive]
instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] :
    IsCentralScalar α (Filter β) :=
  ⟨fun _ f => (congr_arg fun m => map m f) <| funext fun _ => op_smul_eq_smul _ _⟩

Central Scalar Property for Filters

Informal description

For types $\alpha$ and $\beta$ equipped with scalar multiplication operations, if $\beta$ has a central scalar property with respect to $\alpha$ (meaning the scalar multiplication by $\alpha$ and its multiplicative opposite $\alpha^\text{op}$ coincide on $\beta$), then the filters on $\beta$ also satisfy the central scalar property with respect to $\alpha$. In other words, for any filter $f$ on $\beta$, the scalar multiplication operations by $\alpha$ and $\alpha^\text{op}$ coincide on $f$.

Filter.mulAction definition

[Monoid α] [MulAction α β] : MulAction (Filter α) (Filter β)

Full source

/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
`Filter α` on `Filter β`. -/
@[to_additive "An additive action of an additive monoid `α` on a type `β` gives an additive action
 of `Filter α` on `Filter β`"]
protected def mulAction [Monoid α] [MulAction α β] : MulAction (Filter α) (Filter β) where
  one_smul f := map₂_pure_left.trans <| by simp_rw [one_smul, map_id']
  mul_smul _ _ _ := map₂_assoc mul_smul

Multiplicative action of filters induced by a monoid action

Informal description

Given a monoid $\alpha$ acting on a type $\beta$, this defines a multiplicative action of the filter space $\text{Filter } \alpha$ on the filter space $\text{Filter } \beta$. Specifically, for any filter $f$ on $\alpha$ and filter $g$ on $\beta$, the action $f \bullet g$ is the filter generated by all sets of the form $s \bullet t$ where $s \in f$ and $t \in g$. This action satisfies: 1. The identity filter $\{1\}$ acts trivially: $\{1\} \bullet g = g$. 2. The action is associative: $(f_1 * f_2) \bullet g = f_1 \bullet (f_2 \bullet g)$ for any filters $f_1, f_2$ on $\alpha$ and $g$ on $\beta$.

Filter.mulActionFilter definition

[Monoid α] [MulAction α β] : MulAction α (Filter β)

Full source

/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Filter β`.
-/
@[to_additive "An additive action of an additive monoid on a type `β` gives an additive action on
 `Filter β`."]
protected def mulActionFilter [Monoid α] [MulAction α β] : MulAction α (Filter β) where
  mul_smul a b f := by simp only [← Filter.map_smul, map_map, Function.comp_def, ← mul_smul]
  one_smul f := by simp only [← Filter.map_smul, one_smul, map_id']

Multiplicative action of a monoid on filters

Informal description

Given a monoid $\alpha$ acting on a type $\beta$, this defines a multiplicative action of $\alpha$ on the filters of $\beta$. Specifically, for any element $a \in \alpha$ and filter $f$ on $\beta$, the action $a \cdot f$ is the filter generated by the sets $\{a \cdot x \mid x \in s\}$ for all $s \in f$. This action satisfies the usual properties: 1. $1 \cdot f = f$ for the identity element $1$ of $\alpha$, 2. $(a \cdot b) \cdot f = a \cdot (b \cdot f)$ for any $a, b \in \alpha$.

Filter.distribMulActionFilter definition

[Monoid α] [AddMonoid β] [DistribMulAction α β] : DistribMulAction α (Filter β)

Full source

/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
multiplicative action on `Filter β`. -/
protected def distribMulActionFilter [Monoid α] [AddMonoid β] [DistribMulAction α β] :
    DistribMulAction α (Filter β) where
  smul_add _ _ _ := map_map₂_distrib <| smul_add _
  smul_zero _ := (map_pure _ _).trans <| by rw [smul_zero, pure_zero]

Distributive multiplicative action on filters

Informal description

Given a monoid $\alpha$ acting distributively on an additive monoid $\beta$, this defines a distributive multiplicative action of $\alpha$ on the filters of $\beta$. Specifically, for any element $a \in \alpha$ and filter $f$ on $\beta$, the action $a \cdot f$ is the filter generated by the sets $\{a \cdot x \mid x \in s\}$ for all $s \in f$. This action satisfies the following properties: 1. $a \cdot (f + g) = a \cdot f + a \cdot g$ for any filters $f, g$ on $\beta$, 2. $a \cdot 0 = 0$ where $0$ is the zero filter.

Filter.mulDistribMulActionFilter definition

[Monoid α] [Monoid β] [MulDistribMulAction α β] : MulDistribMulAction α (Set β)

Full source

/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`. -/
protected def mulDistribMulActionFilter [Monoid α] [Monoid β] [MulDistribMulAction α β] :
    MulDistribMulAction α (Set β) where
  smul_mul _ _ _ := image_image2_distrib <| smul_mul' _
  smul_one _ := image_singleton.trans <| by rw [smul_one, singleton_one]

Pointwise multiplicative distributive action on power sets

Informal description

Given a monoid $\alpha$ acting on a monoid $\beta$ via a multiplicative distributive action (i.e., the action distributes over multiplication in $\beta$), this defines a multiplicative distributive action of $\alpha$ on the power set $\mathcal{P}(\beta)$. The action is defined pointwise: for $a \in \alpha$ and $S \subseteq \beta$, the action $a \cdot S$ is the set $\{a \cdot x \mid x \in S\}$, and it satisfies the distributive property over multiplication in $\beta$.

Filter.NeBot.smul_zero_nonneg theorem

(hf : f.NeBot) : 0 ≤ f • (0 : Filter β)

Full source

theorem NeBot.smul_zero_nonneg (hf : f.NeBot) : 0 ≤ f • (0 : Filter β) :=
  le_smul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
    ⟨_, ha, _, h₂, smul_zero _⟩

Nonnegativity of Scalar Multiplication of Non-trivial Filter with Zero Filter

Informal description

For any non-trivial filter $f$ on a type $\alpha$, the pointwise scalar multiplication of $f$ with the zero filter on a type $\beta$ is nonnegative, i.e., $0 \leq f \bullet (0 : \text{Filter } \beta)$.

Filter.NeBot.zero_smul_nonneg theorem

(hg : g.NeBot) : 0 ≤ (0 : Filter α) • g

Full source

theorem NeBot.zero_smul_nonneg (hg : g.NeBot) : 0 ≤ (0 : Filter α) • g :=
  le_smul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, hb⟩ := hg.nonempty_of_mem h₂
    ⟨_, h₁, _, hb, zero_smul _ _⟩

Nonnegativity of Zero Scalar Multiplication by Non-trivial Filter: $0 \leq 0 \bullet g$

Informal description

For any non-trivial filter $g$ on a type $\beta$, the scalar multiplication of $g$ by the zero filter on $\alpha$ is nonnegative, i.e., $0 \leq (0 : \text{Filter } \alpha) \bullet g$.

Filter.zero_smul_filter_nonpos theorem

: (0 : α) • g ≤ 0

Full source

theorem zero_smul_filter_nonpos : (0 : α) • g ≤ 0 := by
  refine fun s hs => mem_smul_filter.2 ?_
  convert @univ_mem _ g
  refine eq_univ_iff_forall.2 fun a => ?_
  rwa [mem_preimage, zero_smul]

Nonpositivity of Zero Scalar Multiplication of a Filter: $(0 : \alpha) \bullet g \leq 0$

Informal description

For any filter $g$ on a type $\beta$ and a scalar multiplication operation `•` between types $\alpha$ and $\beta$, the scalar multiplication of $g$ by the zero element $0 \in \alpha$ is less than or equal to the zero filter on $\beta$, i.e., $(0 : \alpha) \bullet g \leq 0$.

Filter.zero_smul_filter theorem

(hg : g.NeBot) : (0 : α) • g = 0

Full source

theorem zero_smul_filter (hg : g.NeBot) : (0 : α) • g = 0 :=
  zero_smul_filter_nonpos.antisymm <|
    le_map_iff.2 fun s hs => by
      simp_rw [zero_smul, (hg.nonempty_of_mem hs).image_const]
      exact zero_mem_zero

Zero Scalar Multiplication of Non-trivial Filter Yields Zero Filter

Informal description

For any non-trivial filter $g$ on a type $\beta$ and a scalar multiplication operation $\bullet$ between types $\alpha$ and $\beta$, the scalar multiplication of $g$ by the zero element $0 \in \alpha$ equals the zero filter on $\beta$, i.e., $(0 : \alpha) \bullet g = 0$.

Mathlib.Order.Filter.Pointwise

Main declarations

Implementation notes

Tags