α : Type u
β : Type v
γ : Type ?u.37751
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
⊢ False
α : Type u
β : Type v
γ : Type ?u.37751
f : Filter α
s : Set α
a : α
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
refine' ⟨fun hf g hg => hg hf, fun H => by_contra fun hf => _⟩
α : Type u
β : Type v
γ : Type ?u.37751
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑(sᶜ) := comap Subtype.val f
⊢ False
α : Type u
β : Type v
γ : Type ?u.37751
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
⊢ False
set g : Filter (sᶜ : Set α) := comap (↑) f
α : Type u
β : Type v
γ : Type ?u.37751
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑(sᶜ) := comap Subtype.val f
this : NeBot g
⊢ False
α : Type u
β : Type v
γ : Type ?u.37751
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑(sᶜ) := comap Subtype.val f
⊢ False
haveI : NeBot g := comap_neBot_iff_compl_range.2 (by simpa [compl_setOf] )
no goals
α : Type u
β : Type v
γ : Type ?u.37751
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑(sᶜ) := comap Subtype.val f
this : NeBot g
⊢ False
simpa using H ((of g).map (↑)) (map_le_iff_le_comap.mpr (of_le g))
no goals
α : Type u
β : Type v
γ : Type ?u.37751
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑(sᶜ) := comap Subtype.val f
⊢ ¬range Subtype.valᶜ ∈ f
simpa [compl_setOf]