case mp
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
⊢ IsCountablyGenerated f → ∃ x, HasAntitoneBasis f x

case mpr
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
⊢ (∃ x, HasAntitoneBasis f x) → IsCountablyGenerated f
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
⊢ IsCountablyGenerated f ↔ ∃ x, HasAntitoneBasis f x
constructor
case mp
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
h : IsCountablyGenerated f
⊢ ∃ x, HasAntitoneBasis f x
case mp
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
⊢ IsCountablyGenerated f → ∃ x, HasAntitoneBasis f x
intro h
no goals
case mp
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
h : IsCountablyGenerated f
⊢ ∃ x, HasAntitoneBasis f x
exact f.exists_antitone_basis
case mpr.intro
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
x : ℕ → Set α
h : HasAntitoneBasis f x
⊢ IsCountablyGenerated f
case mpr
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
⊢ (∃ x, HasAntitoneBasis f x) → IsCountablyGenerated f
rintro ⟨x, h⟩
case mpr.intro
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
x : ℕ → Set α
h : HasAntitoneBasis f x
⊢ IsCountablyGenerated (⨅ (i : ℕ), 𝓟 (x i))
case mpr.intro
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
x : ℕ → Set α
h : HasAntitoneBasis f x
⊢ IsCountablyGenerated f
rw [h.1.eq_iInf]
no goals
case mpr.intro
α : Type u_1
β : Type ?u.110685
γ : Type ?u.110688
ι : Type ?u.110691
ι' : Sort ?u.110694
f : Filter α
x : ℕ → Set α
h : HasAntitoneBasis f x
⊢ IsCountablyGenerated (⨅ (i : ℕ), 𝓟 (x i))
exact isCountablyGenerated_seq x