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

case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.1917
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ (⋃ (x : α), s x) ⊆ ⋃ (x : α), Accumulate s x
α : Type u_1
β : Type u_2
γ : Type ?u.1917
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ (⋃ (x : α), Accumulate s x) = ⋃ (x : α), s x
apply Subset.antisymm
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.1917
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ i, x ∈ s i
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.1917
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ (⋃ (x : α), Accumulate s x) ⊆ ⋃ (x : α), s x
simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.1917
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
z : β
x x' : α
left✝ : x' ≤ x
hz : z ∈ s x'
⊢ ∃ i, z ∈ s i
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.1917
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ i, x ∈ s i
intro z x x' ⟨_, hz⟩
no goals
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.1917
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
z : β
x x' : α
left✝ : x' ≤ x
hz : z ∈ s x'
⊢ ∃ i, z ∈ s i
exact ⟨x', hz⟩
no goals
case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.1917
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ (⋃ (x : α), s x) ⊆ ⋃ (x : α), Accumulate s x
exact iUnion_mono fun i => subset_accumulate