α : Type u_3
β : Type ?u.19950
ι : Type u_1
ι' : Type u_2
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f
hg : ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f
⊢ Set.PairwiseDisjoint (↑(Finset.sup s g)) f
α : Type u_3
β : Type ?u.19950
ι : 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
simp_rw [supIndep_iff_pairwiseDisjoint] at hs hg⊢
α : Type u_3
β : Type ?u.19950
ι : Type u_1
ι' : Type u_2
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f
hg : ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f
⊢ Set.PairwiseDisjoint (⋃ (x : ι') (_ : x ∈ ↑s), ↑(g x)) f
α : Type u_3
β : Type ?u.19950
ι : Type u_1
ι' : Type u_2
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f
hg : ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f
⊢ Set.PairwiseDisjoint (↑(Finset.sup s g)) f
rw [sup_eq_biUnion, coe_biUnion]
no goals
α : Type u_3
β : Type ?u.19950
ι : Type u_1
ι' : Type u_2
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f
hg : ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f
⊢ Set.PairwiseDisjoint (⋃ (x : ι') (_ : x ∈ ↑s), ↑(g x)) f
exact hs.biUnion_finset hg