α : Type u_2
β : Type ?u.36290
ι : Type u_1
ι' : Type ?u.36296
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ Independent t ↔ ∀ (i : ι), Disjoint (t i) (⨆ (a : ι) (_ : a ∈ {j | j ≠ i}), t a)
α : Type u_2
β : Type ?u.36290
ι : Type u_1
ι' : Type ?u.36296
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))
simp_rw [sSup_image]
no goals
α : Type u_2
β : Type ?u.36290
ι : Type u_1
ι' : Type ?u.36296
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ Independent t ↔ ∀ (i : ι), Disjoint (t i) (⨆ (a : ι) (_ : a ∈ {j | j ≠ i}), t a)
rfl