coheyting operations on filters

Stream: Is there code for X?

[Aaron Liu]

Is there anything that connects the coheyting operations on filters to some of the more familiar ones? Like for example

import Mathlib

variable {α : Type*} (f : Filter α) (s : Set α)

open Coheyting
namespace Filter

theorem boundary_le_cofinite : boundary f ≤ cofinite := by
  sorry

theorem hnot_hnot : ￢￢f = 𝓟 f.ker := by
  sorry

theorem hnot_def : ￢f = 𝓟 f.kerᶜ := by
  sorry

theorem hnot_principal : ￢𝓟 s = 𝓟 sᶜ := by
  sorry