Absorbs — Mathlib

English

If h : Absorbs M s1 t and hs : s1 ⊆ s2, then Absorbs M s2 t.

Русский

Если s1 поглощает t и s1 ⊆ s2, тогда s2 поглощает t.

LaTeX

$$$\operatorname{Absorbs} M s_1 t \Rightarrow s_1 \subseteq s_2 \Rightarrow \operatorname{Absorbs} M s_2 t$$$

Lean4

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

Похожие утверждения