# 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.

## 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

def Absorbs (M : Type u_1) {α : Type u_2} [] [SMul M α] (s : Set α) (t : Set α) :

A set s absorbs another set t if t is contained in all scalings of s by all but a bounded set of elements.

Equations
Instances For
def Absorbent (M : Type u_1) {α : Type u_2} [] [SMul M α] (s : Set α) :

A set is absorbent if it absorbs every singleton.

Equations
Instances For
theorem Absorbs.empty {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} :
@[deprecated Absorbs.empty]
theorem absorbs_empty {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} :

Alias of Absorbs.empty.

theorem Absorbs.eventually {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {t : Set α} (h : Absorbs M s t) :
∀ᶠ (a : M) in , t a s
@[simp]
theorem Absorbs.of_boundedSpace {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {t : Set α} [] :
Absorbs M s t
theorem Absorbs.mono_left {M : Type u_1} {α : Type u_2} [] [SMul M α] {s₁ : Set α} {s₂ : Set α} {t : Set α} (h : Absorbs M s₁ t) (hs : s₁ s₂) :
Absorbs M s₂ t
theorem Absorbs.mono_right {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {t₁ : Set α} {t₂ : Set α} (h : Absorbs M s t₁) (ht : t₂ t₁) :
Absorbs M s t₂
theorem Absorbs.mono {M : Type u_1} {α : Type u_2} [] [SMul M α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} (h : Absorbs M s₁ t₁) (hs : s₁ s₂) (ht : t₂ t₁) :
Absorbs M s₂ t₂
@[simp]
theorem absorbs_union {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
Absorbs M s (t₁ t₂) Absorbs M s t₁ Absorbs M s t₂
theorem Absorbs.union {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {t₁ : Set α} {t₂ : Set α} (h₁ : Absorbs M s t₁) (h₂ : Absorbs M s t₂) :
Absorbs M s (t₁ t₂)
theorem Set.Finite.absorbs_sUnion {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {T : Set (Set α)} (hT : T.Finite) :
Absorbs M s (⋃₀ T) tT, Absorbs M s t
theorem Absorbs.sUnion {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {T : Set (Set α)} (hT : T.Finite) (hs : tT, Absorbs M s t) :
Absorbs M s (⋃₀ T)
@[simp]
theorem absorbs_iUnion {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {ι : Sort u_3} [] {t : ιSet α} :
Absorbs M s (⋃ (i : ι), t i) ∀ (i : ι), Absorbs M s (t i)
theorem Absorbs.iUnion {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {ι : Sort u_3} [] {t : ιSet α} :
(∀ (i : ι), Absorbs M s (t i))Absorbs M s (⋃ (i : ι), t i)

Alias of the reverse direction of absorbs_iUnion.

theorem Set.Finite.absorbs_biUnion {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {ι : Type u_3} {t : ιSet α} {I : Set ι} (hI : I.Finite) :
Absorbs M s (iI, t i) iI, Absorbs M s (t i)
theorem Absorbs.biUnion {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {ι : Type u_3} {t : ιSet α} {I : Set ι} (hI : I.Finite) :
(iI, Absorbs M s (t i))Absorbs M s (iI, t i)

Alias of the reverse direction of Set.Finite.absorbs_biUnion.

@[deprecated Set.Finite.absorbs_biUnion]
theorem Set.Finite.absorbs_iUnion {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {ι : Type u_3} {t : ιSet α} {I : Set ι} (hI : I.Finite) :
Absorbs M s (iI, t i) iI, Absorbs M s (t i)

Alias of Set.Finite.absorbs_biUnion.

@[simp]
theorem absorbs_biUnion_finset {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {ι : Type u_3} {t : ιSet α} {I : } :
Absorbs M s (iI, t i) iI, Absorbs M s (t i)
theorem Absorbs.biUnion_finset {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {ι : Type u_3} {t : ιSet α} {I : } :
(iI, Absorbs M s (t i))Absorbs M s (iI, t i)

Alias of the reverse direction of absorbs_biUnion_finset.

@[deprecated absorbs_biUnion_finset]
theorem absorbs_iUnion_finset {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {ι : Type u_3} {t : ιSet α} {I : } :
Absorbs M s (iI, t i) iI, Absorbs M s (t i)

Alias of absorbs_biUnion_finset.

theorem Absorbs.add {M : Type u_1} {E : Type u_2} [] {s₁ : Set E} {s₂ : Set E} {t₁ : Set E} {t₂ : Set E} [] [] (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) :
Absorbs M (s₁ + s₂) (t₁ + t₂)
theorem Absorbs.zero {M : Type u_1} {E : Type u_2} [] [Zero E] [] {s : Set E} (hs : 0 s) :
Absorbs M s 0
@[simp]
theorem Absorbs.univ {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {s : Set α} :
Absorbs G₀ Set.univ s
theorem absorbs_iff_eventually_cobounded_mapsTo {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {s : Set α} {t : Set α} :
Absorbs G₀ s t ∀ᶠ (c : G₀) in , Set.MapsTo (fun (x : α) => c⁻¹ x) t s
theorem Absorbs.eventually_cobounded_mapsTo {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {s : Set α} {t : Set α} :
Absorbs G₀ s t∀ᶠ (c : G₀) in , Set.MapsTo (fun (x : α) => c⁻¹ x) t s

Alias of the forward direction of absorbs_iff_eventually_cobounded_mapsTo.

theorem Set.Finite.absorbs_sInter {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {t : Set α} {S : Set (Set α)} (hS : S.Finite) :
Absorbs G₀ (⋂₀ S) t sS, Absorbs G₀ s t
theorem Absorbs.sInter {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {t : Set α} {S : Set (Set α)} (hS : S.Finite) :
(sS, Absorbs G₀ s t)Absorbs G₀ (⋂₀ S) t

Alias of the reverse direction of Set.Finite.absorbs_sInter.

@[simp]
theorem absorbs_inter {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {s : Set α} {t : Set α} {u : Set α} :
Absorbs G₀ (s t) u Absorbs G₀ s u Absorbs G₀ t u
theorem Absorbs.inter {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {s : Set α} {t : Set α} {u : Set α} (hs : Absorbs G₀ s u) (ht : Absorbs G₀ t u) :
Absorbs G₀ (s t) u
@[simp]
theorem absorbs_iInter {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {t : Set α} {ι : Sort u_3} [] {s : ιSet α} :
Absorbs G₀ (⋂ (i : ι), s i) t ∀ (i : ι), Absorbs G₀ (s i) t
theorem Absorbs.iInter {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {t : Set α} {ι : Sort u_3} [] {s : ιSet α} :
(∀ (i : ι), Absorbs G₀ (s i) t)Absorbs G₀ (⋂ (i : ι), s i) t

Alias of the reverse direction of absorbs_iInter.

theorem Set.Finite.absorbs_biInter {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {t : Set α} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ιSet α} :
Absorbs G₀ (iI, s i) t iI, Absorbs G₀ (s i) t
theorem Absorbs.biInter {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {t : Set α} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ιSet α} :
(iI, Absorbs G₀ (s i) t)Absorbs G₀ (iI, s i) t

Alias of the reverse direction of Set.Finite.absorbs_biInter.

@[simp]
theorem absorbs_zero_iff {G₀ : Type u_1} [] [] [().NeBot] {E : Type u_3} [] [] {s : Set E} :
Absorbs G₀ s 0 0 s
@[simp]
theorem absorbs_neg_neg {M : Type u_1} {E : Type u_2} [] [] [] [] {s : Set E} {t : Set E} :
Absorbs M (-s) (-t) Absorbs M s t
theorem Absorbs.of_neg_neg {M : Type u_1} {E : Type u_2} [] [] [] [] {s : Set E} {t : Set E} :
Absorbs M (-s) (-t)Absorbs M s t

Alias of the forward direction of absorbs_neg_neg.

theorem Absorbs.neg_neg {M : Type u_1} {E : Type u_2} [] [] [] [] {s : Set E} {t : Set E} :
Absorbs M s tAbsorbs M (-s) (-t)

Alias of the reverse direction of absorbs_neg_neg.

theorem Absorbs.sub {M : Type u_1} {E : Type u_2} [] [] [] [] {s₁ : Set E} {s₂ : Set E} {t₁ : Set E} {t₂ : Set E} (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) :
Absorbs M (s₁ - s₂) (t₁ - t₂)
theorem Absorbent.mono {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {t : Set α} (ht : ) (hsub : s t) :
@[deprecated Absorbent.mono]
theorem Absorbent.subset {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {t : Set α} (ht : ) (hsub : s t) :

Alias of Absorbent.mono.

theorem absorbent_iff_forall_absorbs_singleton {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} :
∀ (x : α), Absorbs M s {x}
theorem Absorbent.absorbs {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} (hs : ) {x : α} :
Absorbs M s {x}
theorem Absorbent.absorbs_finite {M : Type u_1} {α : Type u_2} [] [SMul M α] {s : Set α} {t : Set α} (hs : ) (ht : t.Finite) :
Absorbs M s t
theorem Absorbent.vadd_absorbs {M : Type u_1} {E : Type u_2} [] [] [] {s₁ : Set E} {s₂ : Set E} {t : Set E} {x : E} (h₁ : Absorbent M s₁) (h₂ : Absorbs M s₂ t) :
Absorbs M (s₁ + s₂) (x +ᵥ t)
theorem absorbent_univ {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] :
Absorbent G₀ Set.univ
theorem absorbent_iff_inv_smul {G₀ : Type u_1} {α : Type u_2} [] [] [MulAction G₀ α] {s : Set α} :
Absorbent G₀ s ∀ (x : α), ∀ᶠ (c : G₀) in , c⁻¹ x s
theorem Absorbent.zero_mem {G₀ : Type u_1} {E : Type u_3} [] [] [().NeBot] [] [] {s : Set E} (hs : Absorbent G₀ s) :
0 s