α : Type u
β : Type v
γ : Type w
δ : Type ?u.120295
ι : Sort x
f✝ g : Filter α
s✝ t s : Set α
f : Filter α
⊢ (∀ (V : Set α), V ∈ f → V ∈ 𝓟 s) ↔ ∀ (V : Set α), V ∈ f → s ⊆ V
α : Type u
β : Type v
γ : Type w
δ : Type ?u.120295
ι : Sort x
f✝ g : Filter α
s✝ t s : Set α
f : Filter α
⊢ 𝓟 s ≤ f ↔ ∀ (V : Set α), V ∈ f → s ⊆ V
change (∀ V, V ∈ f → V ∈ _) ↔ _
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.120295
ι : Sort x
f✝ g : Filter α
s✝ t s : Set α
f : Filter α
⊢ (∀ (V : Set α), V ∈ f → V ∈ 𝓟 s) ↔ ∀ (V : Set α), V ∈ f → s ⊆ V
simp_rw [mem_principal]