ι : Sort ?u.107868
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
s : Set (Set α)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set α), a ∈ s → SetIndependent a
⊢ SetIndependent (⋃ (i : ↑s), ↑i)
ι : Sort ?u.107868
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
s : Set (Set α)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set α), a ∈ s → SetIndependent a
⊢ SetIndependent (⋃₀ s)
rw [Set.sUnion_eq_iUnion]
no goals
ι : Sort ?u.107868
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
s : Set (Set α)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set α), a ∈ s → SetIndependent a
⊢ SetIndependent (⋃ (i : ↑s), ↑i)
exact CompleteLattice.setIndependent_iUnion_of_directed hs.directed_val (by simpa using h)
no goals
ι : Sort ?u.107868
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
s : Set (Set α)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set α), a ∈ s → SetIndependent a
⊢ ∀ (i : ↑s), SetIndependent ↑i
simpa using h