[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
f : Filter α
⊢ smallSets f = generate (powerset '' f.sets)
[PROOFSTEP]
simp_rw [generate_eq_biInf, smallSets, iInf_image]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
f : Filter α
⊢ Filter.lift' f powerset = ⨅ (b : Set α) (_ : b ∈ f.sets), 𝓟 (𝒫 b)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
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
[PROOFSTEP]
rw [smallSets, eventually_lift'_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
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_2 ι : Sort u_3 l l' la : Filter α lb : Filter β p : Set α → Prop ⊢ Monotone powerset
[PROOFSTEP]
rfl
[GOAL]
case hh
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ Monotone powerset
[PROOFSTEP]
exact monotone_powerset
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
⊢ smallSets ⊥ = pure ∅
[PROOFSTEP]
rw [smallSets, lift'_bot, powerset_empty, principal_singleton]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
⊢ Monotone powerset
[PROOFSTEP]
exact monotone_powerset
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
⊢ smallSets ⊤ = ⊤
[PROOFSTEP]
rw [smallSets, lift'_top, powerset_univ, principal_univ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l✝ l' la : Filter α
lb : Filter β
l : Filter α
⊢ NeBot (smallSets l)
[PROOFSTEP]
refine' (lift'_neBot_iff _).2 fun _ _ => powerset_nonempty
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l✝ l' la : Filter α
lb : Filter β
l : Filter α
⊢ Monotone powerset
[PROOFSTEP]
exact monotone_powerset
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
s t : α → Set β
ht : Tendsto t la (smallSets lb)
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ Tendsto s la (smallSets lb)
[PROOFSTEP]
rw [tendsto_smallSets_iff] at ht ⊢
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ (t_1 : Set β), t_1 ∈ lb → ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ (t : Set β), t ∈ lb → ∀ᶠ (x : α) in la, s x ⊆ t
[PROOFSTEP]
exact fun u hu => (ht u hu).mp (hst.mono fun _ hst ht => hst.trans ht)
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : α → Prop
⊢ (∃ s, s ∈ l ∧ ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∃ s, s ∈ l ∧ ∃ t, t ∈ l' ∧ ∀ (x : α), x ∈ t → x ∈ s → p x
[PROOFSTEP]
simp only [eventually_iff_exists_mem]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : α → Prop
⊢ (∃ s, s ∈ l ∧ ∃ t, t ∈ l' ∧ ∀ (x : α), x ∈ t → x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x
[PROOFSTEP]
simp only [eventually_inf, and_comm, mem_inter_iff, ← and_imp]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : α → Prop
⊢ (∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → p x) ↔ ∀ᶠ (x : α) in l, p x
[PROOFSTEP]
simpa only [inf_top_eq, eventually_top] using @eventually_smallSets_eventually α l ⊤ p
