doc-next-gen

Mathlib.Topology.Bornology.Absorbs

Module docstring

{"# Absorption of sets

Let M act on α, let A and B be sets in α. We say that A absorbs B if for sufficiently large a : M, we have B ⊆ a • A. Formally, \"for sufficiently large a : M\" means \"for all but a bounded set of a\".

Traditionally, this definition is formulated for the action of a (semi)normed ring on a module over that ring.

We formulate it in a more general settings for two reasons:

  • this way we don't have to depend on metric spaces, normed rings etc;
  • some proofs look nicer with this definition than with something like ∃ r : ℝ, ∀ a : R, r ≤ ‖a‖ → B ⊆ a • A.

If M is a GroupWithZero (e.g., a division ring), the sets absorbing a given set form a filter, see Filter.absorbing.

Implementation notes

For now, all theorems assume that we deal with (a generalization of) a module over a division ring. Some lemmas have multiplicative versions for MulDistribMulActions. They can be added later when someone needs them.

Keywords

absorbs, absorbent "}

Absorbs definition
(s t : Set α) : Prop
Full source 
/-- A set `s` absorbs another set `t` if `t` is contained in all scalings of `s`
by all but a bounded set of elements. -/
def Absorbs (s t : Set α) : Prop :=
  ∀ᶠ a in cobounded M, t ⊆ a • s
Absorption of sets under group action
Informal description
A set $s$ in a type $\alpha$ with an action of $M$ is said to *absorb* another set $t$ if for all but a bounded set of elements $a \in M$, the set $t$ is contained in the scaling $a \cdot s$.
Absorbent definition
(s : Set α) : Prop
Full source 
/-- A set is *absorbent* if it absorbs every singleton. -/
def Absorbent (s : Set α) : Prop :=
  ∀ x, Absorbs M s {x}
Absorbent set under monoid action
Informal description
A set $s$ in a type $\alpha$ with an action of a monoid $M$ is called *absorbent* if for every element $x \in \alpha$, the set $s$ absorbs the singleton $\{x\}$. That is, for all but a bounded set of elements $a \in M$, the singleton $\{x\}$ is contained in the scaling $a \cdot s$.
Absorbs.empty theorem
: Absorbs M s ∅
Full source 
protected lemma empty : Absorbs M s ∅ := by simp [Absorbs]
Empty Set is Absorbed by Any Set
Informal description
For any set $s$ in a type $\alpha$ with an action of $M$, the empty set $\emptyset$ is absorbed by $s$.
Absorbs.eventually theorem
(h : Absorbs M s t) : ∀ᶠ a in cobounded M, t ⊆ a • s
Full source 
protected lemma eventually (h : Absorbs M s t) : ∀ᶠ a in cobounded M, t ⊆ a • s := h
Eventual Absorption Property
Informal description
If a set $s$ absorbs another set $t$ under the action of $M$, then for all but a bounded set of elements $a \in M$, the inclusion $t \subseteq a \cdot s$ holds.
Absorbs.of_boundedSpace theorem
[BoundedSpace M] : Absorbs M s t
Full source 
@[simp] lemma of_boundedSpace [BoundedSpace M] : Absorbs M s t := by simp [Absorbs]
Absorption in Bounded Spaces
Informal description
Let $M$ be a bounded space acting on a type $\alpha$. Then for any sets $s, t \subseteq \alpha$, the set $s$ absorbs $t$.
Absorbs.mono_left theorem
(h : Absorbs M s₁ t) (hs : s₁ ⊆ s₂) : Absorbs M s₂ t
Full source 
lemma mono_left (h : Absorbs M s₁ t) (hs : s₁ ⊆ s₂) : Absorbs M s₂ t :=
  h.mono fun _a ha ↦ ha.trans <| smul_set_mono hs
Monotonicity of Absorption on the Left: Larger Sets Absorb More
Informal description
Let $M$ act on a type $\alpha$, and let $s_1, s_2, t$ be subsets of $\alpha$. If $s_1$ absorbs $t$ and $s_1 \subseteq s_2$, then $s_2$ absorbs $t$.
Absorbs.mono_right theorem
(h : Absorbs M s t₁) (ht : t₂ ⊆ t₁) : Absorbs M s t₂
Full source 
lemma mono_right (h : Absorbs M s t₁) (ht : t₂ ⊆ t₁) : Absorbs M s t₂ :=
  h.mono fun _ ↦ ht.trans
Monotonicity of Absorption with Respect to Subset Inclusion
Informal description
Let $M$ act on a type $\alpha$, and let $s, t_1, t_2$ be subsets of $\alpha$. If $s$ absorbs $t_1$ and $t_2 \subseteq t_1$, then $s$ absorbs $t_2$.
Absorbs.mono theorem
(h : Absorbs M s₁ t₁) (hs : s₁ ⊆ s₂) (ht : t₂ ⊆ t₁) : Absorbs M s₂ t₂
Full source 
lemma mono (h : Absorbs M s₁ t₁) (hs : s₁ ⊆ s₂) (ht : t₂ ⊆ t₁) : Absorbs M s₂ t₂ :=
  (h.mono_left hs).mono_right ht
Monotonicity of Absorption under Subset Inclusion
Informal description
Let $M$ act on a type $\alpha$, and let $s_1, s_2, t_1, t_2$ be subsets of $\alpha$. If $s_1$ absorbs $t_1$, $s_1 \subseteq s_2$, and $t_2 \subseteq t_1$, then $s_2$ absorbs $t_2$. That is, if for all but a bounded set of elements $a \in M$, we have $t_1 \subseteq a \cdot s_1$, then for all but a bounded set of elements $a \in M$, we have $t_2 \subseteq a \cdot s_2$.
absorbs_union theorem
: Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂
Full source 
@[simp]
lemma _root_.absorbs_union : AbsorbsAbsorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂ := by
  simp [Absorbs]
Absorption of Union is Equivalent to Absorption of Each Set
Informal description
Let $M$ act on a type $\alpha$, and let $s, t_1, t_2$ be subsets of $\alpha$. Then $s$ absorbs the union $t_1 \cup t_2$ if and only if $s$ absorbs both $t_1$ and $t_2$ individually. In other words, for all but a bounded set of elements $a \in M$, we have $t_1 \cup t_2 \subseteq a \cdot s$ if and only if both $t_1 \subseteq a \cdot s$ and $t_2 \subseteq a \cdot s$ hold for all but a bounded set of $a \in M$.
Absorbs.union theorem
(h₁ : Absorbs M s t₁) (h₂ : Absorbs M s t₂) : Absorbs M s (t₁ ∪ t₂)
Full source 
protected lemma union (h₁ : Absorbs M s t₁) (h₂ : Absorbs M s t₂) : Absorbs M s (t₁ ∪ t₂) :=
  absorbs_union.2 ⟨h₁, h₂⟩
Union of Absorbed Sets is Absorbed
Informal description
Let $M$ act on a type $\alpha$, and let $s, t_1, t_2$ be subsets of $\alpha$. If $s$ absorbs $t_1$ and $s$ absorbs $t_2$, then $s$ absorbs the union $t_1 \cup t_2$. That is, if for all but a bounded set of elements $a \in M$, we have both $t_1 \subseteq a \cdot s$ and $t_2 \subseteq a \cdot s$, then for all but a bounded set of elements $a \in M$, we have $t_1 \cup t_2 \subseteq a \cdot s$.
Set.Finite.absorbs_sUnion theorem
{T : Set (Set α)} (hT : T.Finite) : Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t
Full source 
lemma _root_.Set.Finite.absorbs_sUnion {T : Set (Set α)} (hT : T.Finite) :
    AbsorbsAbsorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t := by
  simp [Absorbs, hT]
Finite Union Absorption Criterion under Group Action
Informal description
Let $M$ act on a type $\alpha$, and let $s$ be a subset of $\alpha$. For any finite collection $T$ of subsets of $\alpha$, the set $s$ absorbs the union $\bigcup₀ T$ if and only if $s$ absorbs every subset $t$ in $T$. In other words, $s$ absorbs $\bigcup₀ T$ precisely when for every $t \in T$, there exists a bounded subset of $M$ such that for all $a \in M$ outside this subset, $t \subseteq a \cdot s$.
Absorbs.sUnion theorem
(hT : T.Finite) (hs : ∀ t ∈ T, Absorbs M s t) : Absorbs M s (⋃₀ T)
Full source 
protected lemma sUnion (hT : T.Finite) (hs : ∀ t ∈ T, Absorbs M s t) :
    Absorbs M s (⋃₀ T) :=
  hT.absorbs_sUnion.2 hs
Absorption of Finite Unions under Group Action
Informal description
Let $M$ act on a type $\alpha$, and let $s$ be a subset of $\alpha$. For any finite collection $T$ of subsets of $\alpha$, if $s$ absorbs every subset $t \in T$, then $s$ absorbs the union $\bigcup_{t \in T} t$.
absorbs_iUnion theorem
{ι : Sort*} [Finite ι] {t : ι → Set α} : Absorbs M s (⋃ i, t i) ↔ ∀ i, Absorbs M s (t i)
Full source 
@[simp]
lemma _root_.absorbs_iUnion {ι : Sort*} [Finite ι] {t : ι → Set α} :
    AbsorbsAbsorbs M s (⋃ i, t i) ↔ ∀ i, Absorbs M s (t i) :=
  (finite_range t).absorbs_sUnion.trans forall_mem_range
Finite Union Absorption Criterion for Group Actions
Informal description
Let $M$ act on a type $\alpha$, and let $s$ be a subset of $\alpha$. For any finite index type $\iota$ and any family of sets $\{t_i\}_{i \in \iota}$ in $\alpha$, the set $s$ absorbs the union $\bigcup_{i \in \iota} t_i$ if and only if $s$ absorbs each $t_i$ for all $i \in \iota$.
Set.Finite.absorbs_biUnion theorem
{ι : Type*} {t : ι → Set α} {I : Set ι} (hI : I.Finite) : Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)
Full source 
lemma _root_.Set.Finite.absorbs_biUnion {ι : Type*} {t : ι → Set α} {I : Set ι} (hI : I.Finite) :
    AbsorbsAbsorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i) := by
  simp [Absorbs, hI]
Finite Union Absorption Criterion for Group Actions
Informal description
Let $M$ act on a type $\alpha$, and let $s$ be a set in $\alpha$. For any finite index set $I$ and any family of sets $\{t_i\}_{i \in I}$ in $\alpha$, the set $s$ absorbs the union $\bigcup_{i \in I} t_i$ if and only if $s$ absorbs each $t_i$ for all $i \in I$.
absorbs_biUnion_finset theorem
{ι : Type*} {t : ι → Set α} {I : Finset ι} : Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)
Full source 
@[simp]
lemma _root_.absorbs_biUnion_finset {ι : Type*} {t : ι → Set α} {I : Finset ι} :
    AbsorbsAbsorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i) :=
  I.finite_toSet.absorbs_biUnion
Absorption Criterion for Finite Unions under Group Action
Informal description
Let $M$ act on a type $\alpha$, and let $s$ be a set in $\alpha$. For any finite index set $I$ (represented as a finset) and any family of sets $\{t_i\}_{i \in I}$ in $\alpha$, the set $s$ absorbs the union $\bigcup_{i \in I} t_i$ if and only if $s$ absorbs each individual set $t_i$ for all $i \in I$.
Absorbs.add theorem
[AddZeroClass E] [DistribSMul M E] (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) : Absorbs M (s₁ + s₂) (t₁ + t₂)
Full source 
protected lemma add [AddZeroClass E] [DistribSMul M E]
    (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) : Absorbs M (s₁ + s₂) (t₁ + t₂) :=
  h₂.mp <| h₁.eventually.mono fun x hx₁ hx₂ ↦ by rw [smul_add]; exact add_subset_add hx₁ hx₂
Absorption of Minkowski Sums under Distributive Scalar Multiplication
Informal description
Let $E$ be a type with an addition operation and a zero element, and let $M$ act on $E$ via a distributive scalar multiplication. If sets $s_1$ and $s_2$ in $E$ absorb sets $t_1$ and $t_2$ respectively under the action of $M$, then the Minkowski sum $s_1 + s_2$ absorbs the Minkowski sum $t_1 + t_2$.
Absorbs.zero theorem
[Zero E] [SMulZeroClass M E] {s : Set E} (hs : 0 ∈ s) : Absorbs M s 0
Full source 
protected lemma zero [Zero E] [SMulZeroClass M E] {s : Set E} (hs : 0 ∈ s) : Absorbs M s 0 :=
  Eventually.of_forall fun _ ↦ zero_subset.2 <| zero_mem_smul_set hs
Absorption of Zero by Any Set Containing Zero
Informal description
Let $E$ be a type with a zero element and a scalar multiplication action of $M$ on $E$ that preserves zero. For any set $s \subseteq E$ containing zero, the set $s$ absorbs the singleton set $\{0\}$ under the action of $M$.
Absorbs.univ theorem
: Absorbs G₀ univ s
Full source 
@[simp]
protected lemma Absorbs.univ : Absorbs G₀ univ s :=
  (eventually_ne_cobounded 0).mono fun a ha ↦ by rw [smul_set_univ₀ ha]; apply subset_univ
Universal Set Absorbs Any Set Under Group With Zero Action
Informal description
For any set $s$ in a type $\alpha$ with an action of a group with zero $G₀$, the universal set $\text{univ}$ absorbs $s$. That is, for all but a bounded set of elements $c \in G₀$, we have $s \subseteq c \cdot \text{univ}$.
absorbs_iff_eventually_cobounded_mapsTo theorem
: Absorbs G₀ s t ↔ ∀ᶠ c in cobounded G₀, MapsTo (c⁻¹ • ·) t s
Full source 
lemma absorbs_iff_eventually_cobounded_mapsTo :
    AbsorbsAbsorbs G₀ s t ↔ ∀ᶠ c in cobounded G₀, MapsTo (c⁻¹ • ·) t s :=
  eventually_congr <| (eventually_ne_cobounded 0).mono fun c hc ↦ by
    rw [← preimage_smul_inv₀ hc]; rfl
Absorption Criterion via Cobounded Maps
Informal description
Let $G₀$ be a group with zero acting on a type $\alpha$, and let $s, t$ be subsets of $\alpha$. Then $s$ absorbs $t$ if and only if for all but a bounded set of elements $c \in G₀$, the function $x \mapsto c^{-1} \cdot x$ maps $t$ into $s$. In other words, $s$ absorbs $t$ precisely when the preimage of $s$ under the scaling action by $c^{-1}$ contains $t$ for all $c$ outside some bounded subset of $G₀$.
absorbs_inter theorem
: Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u
Full source 
@[simp]
lemma absorbs_inter : AbsorbsAbsorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u := by
  simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_inter, eventually_and]
Intersection Absorption Criterion: $s \cap t$ absorbs $u$ iff $s$ and $t$ each absorb $u$
Informal description
Let $G₀$ be a group with zero acting on a type $\alpha$, and let $s, t, u$ be subsets of $\alpha$. Then the intersection $s \cap t$ absorbs $u$ if and only if both $s$ absorbs $u$ and $t$ absorbs $u$. In other words, $u \subseteq c \cdot (s \cap t)$ for all but a bounded set of $c \in G₀$ if and only if $u \subseteq c \cdot s$ and $u \subseteq c \cdot t$ for all but a bounded set of $c \in G₀$.
Absorbs.inter theorem
(hs : Absorbs G₀ s u) (ht : Absorbs G₀ t u) : Absorbs G₀ (s ∩ t) u
Full source 
protected lemma Absorbs.inter (hs : Absorbs G₀ s u) (ht : Absorbs G₀ t u) : Absorbs G₀ (s ∩ t) u :=
  absorbs_inter.2 ⟨hs, ht⟩
Intersection of Absorbing Sets is Absorbing
Informal description
Let $G₀$ be a group with zero acting on a type $\alpha$, and let $s, t, u$ be subsets of $\alpha$. If $s$ absorbs $u$ and $t$ absorbs $u$, then their intersection $s \cap t$ also absorbs $u$. In other words, if for all but a bounded set of elements $c \in G₀$ we have $u \subseteq c \cdot s$ and $u \subseteq c \cdot t$, then for all but a bounded set of $c \in G₀$ we also have $u \subseteq c \cdot (s \cap t)$.
Filter.absorbing definition
: Filter α
Full source 
/-- The filter of sets that absorb `u`. -/
def Filter.absorbing : Filter α where
  sets := {s | Absorbs G₀ s u}
  univ_sets := .univ
  sets_of_superset h := h.mono_left
  inter_sets := .inter
Filter of absorbing sets
Informal description
The filter on a type $\alpha$ consisting of all subsets $s$ that absorb a fixed subset $u$ under the action of a group with zero $G₀$. Here, a set $s$ absorbs $u$ if for all but a bounded set of elements $a \in G₀$, we have $u \subseteq a \cdot s$.
Filter.mem_absorbing theorem
: s ∈ absorbing G₀ u ↔ Absorbs G₀ s u
Full source 
@[simp]
lemma Filter.mem_absorbing : s ∈ absorbing G₀ us ∈ absorbing G₀ u ↔ Absorbs G₀ s u := .rfl
Characterization of Absorbing Sets in Filter
Informal description
A set $s$ belongs to the filter of absorbing sets for a fixed set $u$ under the action of a group with zero $G₀$ if and only if $s$ absorbs $u$, i.e., for all but a bounded set of elements $a \in G₀$, we have $u \subseteq a \cdot s$.
Set.Finite.absorbs_sInter theorem
(hS : S.Finite) : Absorbs G₀ (⋂₀ S) t ↔ ∀ s ∈ S, Absorbs G₀ s t
Full source 
lemma Set.Finite.absorbs_sInter (hS : S.Finite) :
    AbsorbsAbsorbs G₀ (⋂₀ S) t ↔ ∀ s ∈ S, Absorbs G₀ s t :=
  sInter_mem (f := absorbing G₀ t) hS
Finite Intersection Absorption Criterion for Group Action
Informal description
Let $G₀$ be a group with zero acting on a type $\alpha$, let $S$ be a finite collection of subsets of $\alpha$, and let $t$ be another subset of $\alpha$. Then the intersection $\bigcap S$ absorbs $t$ if and only if every set $s \in S$ absorbs $t$.
absorbs_iInter theorem
{ι : Sort*} [Finite ι] {s : ι → Set α} : Absorbs G₀ (⋂ i, s i) t ↔ ∀ i, Absorbs G₀ (s i) t
Full source 
@[simp]
lemma absorbs_iInter {ι : Sort*} [Finite ι] {s : ι → Set α} :
    AbsorbsAbsorbs G₀ (⋂ i, s i) t ↔ ∀ i, Absorbs G₀ (s i) t :=
  iInter_mem (f := absorbing G₀ t)
Intersection of Finite Family Absorbs iff Each Member Absorbs
Informal description
Let $G₀$ be a group with zero acting on a type $\alpha$, and let $\{s_i\}_{i \in \iota}$ be a finite family of subsets of $\alpha$. Then the intersection $\bigcap_{i \in \iota} s_i$ absorbs a subset $t \subseteq \alpha$ if and only if each $s_i$ absorbs $t$. Here, a set $s$ *absorbs* $t$ if for all but a bounded set of elements $a \in G₀$, we have $t \subseteq a \cdot s$.
Set.Finite.absorbs_biInter theorem
{ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set α} : Absorbs G₀ (⋂ i ∈ I, s i) t ↔ ∀ i ∈ I, Absorbs G₀ (s i) t
Full source 
lemma Set.Finite.absorbs_biInter {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set α} :
    AbsorbsAbsorbs G₀ (⋂ i ∈ I, s i) t ↔ ∀ i ∈ I, Absorbs G₀ (s i) t :=
  biInter_mem (f := absorbing G₀ t) hI
Finite Intersection Absorption: $\bigcap_{i \in I} s_i$ absorbs $t$ iff each $s_i$ absorbs $t$ for finite $I$
Informal description
Let $G₀$ be a group with zero acting on a type $\alpha$, $I$ be a finite set of indices, and $\{s_i\}_{i \in I}$ be a family of subsets of $\alpha$. Then the intersection $\bigcap_{i \in I} s_i$ absorbs a subset $t$ of $\alpha$ if and only if for every $i \in I$, the set $s_i$ absorbs $t$. Here, a set $s$ *absorbs* $t$ if for all but a bounded set of elements $a \in G₀$, we have $t \subseteq a \cdot s$.
absorbs_zero_iff theorem
[NeBot (cobounded G₀)] {E : Type*} [AddMonoid E] [DistribMulAction G₀ E] {s : Set E} : Absorbs G₀ s 0 ↔ 0 ∈ s
Full source 
@[simp]
lemma absorbs_zero_iff [NeBot (cobounded G₀)]
    {E : Type*} [AddMonoid E] [DistribMulAction G₀ E] {s : Set E} :
    AbsorbsAbsorbs G₀ s 0 ↔ 0 ∈ s := by
  simp only [absorbs_iff_eventually_cobounded_mapsTo, ← singleton_zero,
    mapsTo_singleton, smul_zero, eventually_const]
Absorption of Zero Element: $s$ absorbs $0$ iff $0 \in s$
Informal description
Let $G₀$ be a group with zero acting on an additive monoid $E$ via a distributive multiplicative action, and let $s$ be a subset of $E$. Then $s$ absorbs the zero element if and only if $0 \in s$. Here, "absorbs" means that for all but a bounded set of elements $a \in G₀$, the zero element is contained in the scaled set $a \cdot s$.
absorbs_neg_neg theorem
{s t : Set E} : Absorbs M (-s) (-t) ↔ Absorbs M s t
Full source 
@[simp]
lemma absorbs_neg_neg {s t : Set E} : AbsorbsAbsorbs M (-s) (-t) ↔ Absorbs M s t := by simp [Absorbs]
Negation Preserves Absorption: $\text{Absorbs}(M, -s, -t) \leftrightarrow \text{Absorbs}(M, s, t)$
Informal description
For any sets $s$ and $t$ in a type $E$ with an action of $M$, the set $-s$ absorbs $-t$ if and only if $s$ absorbs $t$.
Absorbs.sub theorem
{s₁ s₂ t₁ t₂ : Set E} (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) : Absorbs M (s₁ - s₂) (t₁ - t₂)
Full source 
lemma Absorbs.sub {s₁ s₂ t₁ t₂ : Set E} (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) :
    Absorbs M (s₁ - s₂) (t₁ - t₂) := by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_neg
Absorption of Set Differences: $s_1 - s_2$ absorbs $t_1 - t_2$ if $s_1$ absorbs $t_1$ and $s_2$ absorbs $t_2$
Informal description
Let $E$ be a type with an action of a monoid $M$, and let $s_1, s_2, t_1, t_2$ be subsets of $E$. If $s_1$ absorbs $t_1$ and $s_2$ absorbs $t_2$ under the action of $M$, then the set difference $s_1 - s_2$ absorbs the set difference $t_1 - t_2$. Here, a set $s$ *absorbs* a set $t$ if for all but a bounded set of elements $a \in M$, we have $t \subseteq a \cdot s$.
Absorbent.mono theorem
(ht : Absorbent M s) (hsub : s ⊆ t) : Absorbent M t
Full source 
protected theorem mono (ht : Absorbent M s) (hsub : s ⊆ t) : Absorbent M t := fun x ↦
  (ht x).mono_left hsub
Monotonicity of Absorbent Sets: Larger Sets Remain Absorbent
Informal description
Let $M$ be a monoid acting on a type $\alpha$, and let $s$ and $t$ be subsets of $\alpha$. If $s$ is absorbent and $s \subseteq t$, then $t$ is also absorbent.
Absorbent.absorbs theorem
(hs : Absorbent M s) {x : α} : Absorbs M s { x }
Full source 
protected theorem absorbs (hs : Absorbent M s) {x : α} : Absorbs M s {x} := hs x
Absorbent Sets Absorb Singletons
Informal description
Let $M$ be a monoid acting on a type $\alpha$, and let $s$ be an absorbent subset of $\alpha$. Then for any element $x \in \alpha$, the set $s$ absorbs the singleton $\{x\}$. That is, there exists a bounded subset $B \subseteq M$ such that for all $a \in M \setminus B$, we have $\{x\} \subseteq a \cdot s$.
Absorbent.absorbs_finite theorem
(hs : Absorbent M s) (ht : t.Finite) : Absorbs M s t
Full source 
theorem absorbs_finite (hs : Absorbent M s) (ht : t.Finite) : Absorbs M s t := by
  rw [← Set.biUnion_of_singleton t]
  exact .biUnion ht fun _ _ => hs.absorbs
Absorbent Sets Absorb Finite Sets
Informal description
Let $M$ be a monoid acting on a type $\alpha$, and let $s$ be an absorbent subset of $\alpha$. For any finite subset $t \subseteq \alpha$, the set $s$ absorbs $t$. That is, there exists a bounded subset $B \subseteq M$ such that for all $a \in M \setminus B$, we have $t \subseteq a \cdot s$.
Absorbent.vadd_absorbs theorem
{M E : Type*} [Bornology M] [AddZeroClass E] [DistribSMul M E] {s₁ s₂ t : Set E} {x : E} (h₁ : Absorbent M s₁) (h₂ : Absorbs M s₂ t) : Absorbs M (s₁ + s₂) (x +ᵥ t)
Full source 
theorem vadd_absorbs {M E : Type*} [Bornology M] [AddZeroClass E] [DistribSMul M E]
    {s₁ s₂ t : Set E} {x : E} (h₁ : Absorbent M s₁) (h₂ : Absorbs M s₂ t) :
    Absorbs M (s₁ + s₂) (x +ᵥ t) := by
  rw [← singleton_vadd]; exact (h₁ x).add h₂
Absorption of Translated Sets under Minkowski Sum of Absorbent and Absorbing Sets
Informal description
Let $M$ be a monoid with a bornology, $E$ be an additive monoid with a distributive scalar multiplication by $M$, and $s_1, s_2, t$ be subsets of $E$. If $s_1$ is absorbent and $s_2$ absorbs $t$ under the action of $M$, then the Minkowski sum $s_1 + s_2$ absorbs the translation $x + t$ for any $x \in E$.
absorbent_univ theorem
: Absorbent G₀ (univ : Set α)
Full source 
lemma absorbent_univ : Absorbent G₀ (univ : Set α) := fun _ ↦ .univ
Universal Set is Absorbent under Group with Zero Action
Informal description
The universal set $\text{univ}$ in a type $\alpha$ with an action of a group with zero $G₀$ is absorbent. That is, for every element $x \in \alpha$, there exists a co-bounded set of elements $c \in G₀$ such that $c^{-1} \cdot x \in \text{univ}$.
absorbent_iff_inv_smul theorem
{s : Set α} : Absorbent G₀ s ↔ ∀ x, ∀ᶠ c in cobounded G₀, c⁻¹ • x ∈ s
Full source 
lemma absorbent_iff_inv_smul {s : Set α} :
    AbsorbentAbsorbent G₀ s ↔ ∀ x, ∀ᶠ c in cobounded G₀, c⁻¹ • x ∈ s :=
  forall_congr' fun x ↦ by simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_singleton]
Characterization of Absorbent Sets via Inverse Scaling
Informal description
A set $s$ in a type $\alpha$ with an action of a group with zero $G₀$ is *absorbent* if and only if for every element $x \in \alpha$, the inverse scaling $c^{-1} \cdot x$ belongs to $s$ for all but a bounded set of elements $c \in G₀$.
Absorbent.zero_mem theorem
[NeBot (cobounded G₀)] [AddMonoid E] [DistribMulAction G₀ E] {s : Set E} (hs : Absorbent G₀ s) : (0 : E) ∈ s
Full source 
lemma Absorbent.zero_mem [NeBot (cobounded G₀)] [AddMonoid E] [DistribMulAction G₀ E]
    {s : Set E} (hs : Absorbent G₀ s) : (0 : E) ∈ s :=
  absorbs_zero_iff.1 (hs 0)
Zero Element in Absorbent Set under Group Action
Informal description
Let $G₀$ be a group with zero acting on an additive monoid $E$ via a distributive multiplicative action, and let $s$ be a subset of $E$. If $s$ is absorbent, then the zero element $0$ is contained in $s$. Here, "absorbent" means that for every element $x \in E$, the set $s$ absorbs the singleton $\{x\}$ (i.e., for all but a bounded set of elements $a \in G₀$, $\{x\} \subseteq a \cdot s$).
Absorbs.restrict_scalars theorem
{M N α : Type*} [Monoid N] [SMul M N] [SMul M α] [MulAction N α] [IsScalarTower M N α] [Bornology M] [Bornology N] {s t : Set α} (h : Absorbs N s t) (hbdd : Tendsto (· • 1 : M → N) (cobounded M) (cobounded N)) : Absorbs M s t
Full source 
protected theorem Absorbs.restrict_scalars
    {M N α : Type*} [Monoid N] [SMul M N] [SMul M α] [MulAction N α]
    [IsScalarTower M N α] [Bornology M] [Bornology N] {s t : Set α} (h : Absorbs N s t)
    (hbdd : Tendsto (· • 1 : M → N) (cobounded M) (cobounded N)) :
    Absorbs M s t :=
  (hbdd.eventually h).mono <| fun x hx ↦ by rwa [smul_one_smul N x s] at hx
Restriction of Absorption Along Scalar Tower with Boundedness Condition
Informal description
Let $M$ and $N$ be monoids with bornologies, and let $\alpha$ be a type with compatible scalar actions by $M$ and $N$ (forming a scalar tower). Suppose $N$ absorbs $t$ into $s$ (i.e., for all but a bounded set of $n \in N$, $t \subseteq n \cdot s$), and the map $m \mapsto m \cdot 1_N$ from $M$ to $N$ tends to the cobounded filter in $N$ when restricted to the cobounded filter in $M$. Then $M$ also absorbs $t$ into $s$.