no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.117337
ι : Sort x
f g : Filter α
s✝ t s : Set α
⊢ 𝓟 s ⊓ 𝓟 (sᶜ) = ⊥
rw [inf_principal, inter_compl_self, principal_empty]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.117337
ι : Sort x
f g : Filter α
s✝ t s : Set α
⊢ 𝓟 s ⊔ 𝓟 (sᶜ) = ⊤
rw [sup_principal, union_compl_self, principal_univ]