α : Type u
β : Type v
γ : Type ?u.53069
f : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f) → ∀ (f : Filter α), NeBot f → f ≤ g → p f
α : Type u
β : Type v
γ : Type ?u.53069
f : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Filter α), NeBot f → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
refine' ⟨fun H f hf => H f f.neBot hf, _⟩
α : Type u
β : Type v
γ : Type ?u.53069
f✝ : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : NeBot f
hfg : f ≤ g
⊢ p f
α : Type u
β : Type v
γ : Type ?u.53069
f : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f) → ∀ (f : Filter α), NeBot f → f ≤ g → p f
intro H f hf hfg
no goals
α : Type u
β : Type v
γ : Type ?u.53069
f✝ : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : NeBot f
hfg : f ≤ g
⊢ p f
exact hp (of_le f) (H _ ((of_le f).trans hfg))