ι : Type u'
ι' : Type ?u.220541
R : Type u_3
K : Type ?u.220547
M : Type u_2
M' : Type ?u.220553
M'' : Type ?u.220556
V : Type u
V' : Type ?u.220561
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
s : Set η
t : η → Set M
hs : DirectedOn (t ⁻¹'o fun x x_1 => x ⊆ x_1) s
h : ∀ (a : η), a ∈ s → LinearIndependent R fun x => ↑x
⊢ LinearIndependent R fun x => ↑x
ι : Type u'
ι' : Type ?u.220541
R : Type u_3
K : Type ?u.220547
M : Type u_2
M' : Type ?u.220553
M'' : Type ?u.220556
V : Type u
V' : Type ?u.220561
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
s : Set η
t : η → Set M
hs : DirectedOn (t ⁻¹'o fun x x_1 => x ⊆ x_1) s
h : ∀ (a : η), a ∈ s → LinearIndependent R fun x => ↑x
⊢ LinearIndependent R fun x => ↑x
rw [biUnion_eq_iUnion]
no goals
ι : Type u'
ι' : Type ?u.220541
R : Type u_3
K : Type ?u.220547
M : Type u_2
M' : Type ?u.220553
M'' : Type ?u.220556
V : Type u
V' : Type ?u.220561
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
s : Set η
t : η → Set M
hs : DirectedOn (t ⁻¹'o fun x x_1 => x ⊆ x_1) s
h : ∀ (a : η), a ∈ s → LinearIndependent R fun x => ↑x
⊢ LinearIndependent R fun x => ↑x
exact
  linearIndependent_iUnion_of_directed (directed_comp.2 <| hs.directed_val) (by simpa using h)
no goals
ι : Type u'
ι' : Type ?u.220541
R : Type u_3
K : Type ?u.220547
M : Type u_2
M' : Type ?u.220553
M'' : Type ?u.220556
V : Type u
V' : Type ?u.220561
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
s : Set η
t : η → Set M
hs : DirectedOn (t ⁻¹'o fun x x_1 => x ⊆ x_1) s
h : ∀ (a : η), a ∈ s → LinearIndependent R fun x => ↑x
⊢ ∀ (i : ↑s), LinearIndependent R fun x => ↑x
simpa using h