α : Type u
β : Type v
γ : Type w
δ : Type ?u.78074
ι : Sort x
f g : Filter α
s✝ t✝ s t : Set α
⊢ s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s
α : Type u
β : Type v
γ : Type w
δ : Type ?u.78074
ι : Sort x
f g : Filter α
s✝ t✝ s t : Set α
⊢ 𝓟 s = 𝓟 t ↔ s = t
simp only [le_antisymm_iff, le_principal_iff, mem_principal]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.78074
ι : Sort x
f g : Filter α
s✝ t✝ s t : Set α
⊢ s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s
rfl