α : Type u_1
β : Type ?u.1327
ι : Sort ?u.1330
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ (∃ t, t ∈ l ∧ ∀ (y : Set α), y ∈ 𝒫 t → p y) ↔ ∃ s, s ∈ l ∧ ∀ (t : Set α), t ⊆ s → p t

case hh
α : Type u_1
β : Type ?u.1327
ι : Sort ?u.1330
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ Monotone powerset
α : Type u_1
β : Type ?u.1327
ι : Sort ?u.1330
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ (∀ᶠ (s : Set α) in smallSets l, p s) ↔ ∃ s, s ∈ l ∧ ∀ (t : Set α), t ⊆ s → p t
rw [smallSets, eventually_lift'_iff]
case hh
α : Type u_1
β : Type ?u.1327
ι : Sort ?u.1330
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ Monotone powerset
α : Type u_1
β : Type ?u.1327
ι : Sort ?u.1330
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ (∃ t, t ∈ l ∧ ∀ (y : Set α), y ∈ 𝒫 t → p y) ↔ ∃ s, s ∈ l ∧ ∀ (t : Set α), t ⊆ s → p t

case hh
α : Type u_1
β : Type ?u.1327
ι : Sort ?u.1330
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ Monotone powerset
rfl
no goals
case hh
α : Type u_1
β : Type ?u.1327
ι : Sort ?u.1330
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ Monotone powerset
exact monotone_powerset