no goals
𝕜 : Type u_1
𝕝 : Type ?u.6901
E : Type u_2
ι : Sort ?u.6907
κ : ι → Sort ?u.6912
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
⊢ Absorbent 𝕜 A ↔ ∀ (x : E), Absorbs 𝕜 A {x}
simp_rw [Absorbs, Absorbent, singleton_subset_iff]