α : Type u_2
β : Type ?u.37048
ι : Type u_1
ι' : Type ?u.37054
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ (∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))) ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j x, t j = a})
α : Type u_2
β : Type ?u.37048
ι : Type u_1
ι' : Type ?u.37054
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j x, t j = a})
rw [independent_def']
no goals
α : Type u_2
β : Type ?u.37048
ι : Type u_1
ι' : Type ?u.37054
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ (∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))) ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j x, t j = a})
aesop