ι : Sort ?u.24738
α : Type u_1
β : Type ?u.24744
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
⊢ countableGenerate g ∈ upperBounds {f | CountableInterFilter f ∧ g ⊆ f.sets}
ι : Sort ?u.24738
α : Type u_1
β : Type ?u.24744
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
⊢ IsGreatest {f | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)
refine' ⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, _⟩
case intro
ι : Sort ?u.24738
α : Type u_1
β : Type ?u.24744
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ f ≤ countableGenerate g
ι : Sort ?u.24738
α : Type u_1
β : Type ?u.24744
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
⊢ countableGenerate g ∈ upperBounds {f | CountableInterFilter f ∧ g ⊆ f.sets}
rintro f ⟨fct, hf⟩
no goals
case intro
ι : Sort ?u.24738
α : Type u_1
β : Type ?u.24744
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ f ≤ countableGenerate g
rwa [@le_countableGenerate_iff_of_countableInterFilter _ _ _ fct]