case intro
𝕜 : Type u_3
𝕝 : Type ?u.5168
E : Type u_2
ι✝ : Sort ?u.5174
κ : ι✝ → Sort ?u.5179
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_1
s : Set E
f : ι → Set E
t : Finset ι
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ ↑t), f i) ↔ ∀ (i : ι), i ∈ ↑t → Absorbs 𝕜 s (f i)
𝕜 : Type u_3
𝕝 : Type ?u.5168
E : Type u_2
ι✝ : Sort ?u.5174
κ : ι✝ → Sort ?u.5179
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_1
s : Set E
t : Set ι
f : ι → Set E
hi : Set.Finite t
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
lift t to Finset ι using hi
case intro
𝕜 : Type u_3
𝕝 : Type ?u.5168
E : Type u_2
ι✝ : Sort ?u.5174
κ : ι✝ → Sort ?u.5179
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_1
s : Set E
f : ι → Set E
t : Finset ι
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
case intro
𝕜 : Type u_3
𝕝 : Type ?u.5168
E : Type u_2
ι✝ : Sort ?u.5174
κ : ι✝ → Sort ?u.5179
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_1
s : Set E
f : ι → Set E
t : Finset ι
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ ↑t), f i) ↔ ∀ (i : ι), i ∈ ↑t → Absorbs 𝕜 s (f i)
simp only [Finset.mem_coe]
no goals
case intro
𝕜 : Type u_3
𝕝 : Type ?u.5168
E : Type u_2
ι✝ : Sort ?u.5174
κ : ι✝ → Sort ?u.5179
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_1
s : Set E
f : ι → Set E
t : Finset ι
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
exact absorbs_iUnion_finset