α : Type u_2
β : Type ?u.53084
ι : Type u_1
ι' : Type ?u.53090
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
⊢ Independent Subtype.val
α : Type u_2
β : Type ?u.53084
ι : Type u_1
ι' : Type ?u.53090
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
⊢ SetIndependent (range t)
rw [setIndependent_iff]
α : Type u_2
β : Type ?u.53084
ι : Type u_1
ι' : Type ?u.53090
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ : Independent t
ht : Independent (Subtype.val ∘ rangeFactorization t)
⊢ Independent Subtype.val
α : Type u_2
β : Type ?u.53084
ι : Type u_1
ι' : Type ?u.53090
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
⊢ Independent Subtype.val
rw [← coe_comp_rangeFactorization t] at ht
no goals
α : Type u_2
β : Type ?u.53084
ι : Type u_1
ι' : Type ?u.53090
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ : Independent t
ht : Independent (Subtype.val ∘ rangeFactorization t)
⊢ Independent Subtype.val
exact ht.comp' surjective_onto_range