no goals
α : Type u_1
β : Type ?u.67094
ι : Type u_2
ι' : Type ?u.67100
inst✝¹ : CompleteLattice α
inst✝ : Fintype ι
f : ι → α
⊢ Independent f ↔ Finset.SupIndep Finset.univ f
classical
  simp [Finset.supIndep_iff_disjoint_erase, CompleteLattice.Independent, Finset.sup_eq_iSup]
no goals
α : Type u_1
β : Type ?u.67094
ι : Type u_2
ι' : Type ?u.67100
inst✝¹ : CompleteLattice α
inst✝ : Fintype ι
f : ι → α
⊢ Independent f ↔ Finset.SupIndep Finset.univ f
simp [Finset.supIndep_iff_disjoint_erase, CompleteLattice.Independent, Finset.sup_eq_iSup]