𝕜 : Type u_2
𝕝 : Type ?u.10601
E : Type u_1
ι : Sort ?u.10607
κ : ι → Sort ?u.10612
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t u v✝ A B s : Set E
hs : Absorbent 𝕜 s
v : Set E
hv : Set.Finite v
⊢ Absorbs 𝕜 s (⋃ (x : E) (_ : x ∈ v), {x})
𝕜 : Type u_2
𝕝 : Type ?u.10601
E : Type u_1
ι : Sort ?u.10607
κ : ι → Sort ?u.10612
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t u v✝ A B s : Set E
hs : Absorbent 𝕜 s
v : Set E
hv : Set.Finite v
⊢ Absorbs 𝕜 s v
rw [← Set.biUnion_of_singleton v]
no goals
𝕜 : Type u_2
𝕝 : Type ?u.10601
E : Type u_1
ι : Sort ?u.10607
κ : ι → Sort ?u.10612
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t u v✝ A B s : Set E
hs : Absorbent 𝕜 s
v : Set E
hv : Set.Finite v
⊢ Absorbs 𝕜 s (⋃ (x : E) (_ : x ∈ v), {x})
exact hv.absorbs_iUnion.mpr fun _ _ => hs.absorbs