α : Type u_3
β : Type ?u.22024
ι : Type u_1
ι' : Type u_2
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep s fun i => Finset.sup (g i) f
hg : ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f
⊢ SupIndep (Finset.sup s g) f
α : Type u_3
β : Type ?u.22024
ι : Type u_1
ι' : Type u_2
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep s fun i => Finset.sup (g i) f
hg : ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f
⊢ SupIndep (Finset.biUnion s g) f
rw [← sup_eq_biUnion]
no goals
α : Type u_3
β : Type ?u.22024
ι : Type u_1
ι' : Type u_2
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep s fun i => Finset.sup (g i) f
hg : ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f
⊢ SupIndep (Finset.sup s g) f
exact hs.sup hg