absorbs_zero_iff — Mathlib

English

In a suitable setting, Absorbs G0 s 0 is equivalent to 0 ∈ s.

Русский

В соответствующей обстановке Absorbs G0 s 0 эквивалентно нулю принадлежит s.

LaTeX

$$$Absorbs G_0 s 0 \iff 0 \in s$$$

Lean4

@[simp]
theorem absorbs_zero_iff [NeBot (cobounded G₀)] {E : Type*} [AddMonoid E] [DistribMulAction G₀ E] {s : Set E} :
    Absorbs G₀ s 0 ↔ 0 ∈ s := by
  simp only [absorbs_iff_eventually_cobounded_mapsTo, ← singleton_zero, mapsTo_singleton, smul_zero, eventually_const]

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