case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.1596
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ (⋃ (y : α) (_ : y ≤ x), Accumulate s y) ⊆ ⋃ (y : α) (_ : y ≤ x), s y

case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.1596
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ (⋃ (y : α) (_ : y ≤ x), s y) ⊆ ⋃ (y : α) (_ : y ≤ x), Accumulate s y
α : Type u_1
β : Type u_2
γ : Type ?u.1596
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ (⋃ (y : α) (_ : y ≤ x), Accumulate s y) = ⋃ (y : α) (_ : y ≤ x), s y
apply Subset.antisymm
no goals
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.1596
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ (⋃ (y : α) (_ : y ≤ x), Accumulate s y) ⊆ ⋃ (y : α) (_ : y ≤ x), s y
exact iUnion₂_subset fun y hy => monotone_accumulate hy
no goals
case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.1596
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ (⋃ (y : α) (_ : y ≤ x), s y) ⊆ ⋃ (y : α) (_ : y ≤ x), Accumulate s y
exact iUnion₂_mono fun y _ => subset_accumulate