Skip to content
Journals Garden

Filter Decomposition Theorem (Theorem II.4.1)

  • Filter Decomposition Theorem (Theorem II.4.1) #Card
    • Every filter $\mathcal{F}$ on $X$ can be uniquely decomposed as: $$\mathcal{F} = \mathcal{F}^* \wedge \mathcal{F}^\bullet$$ where $\mathcal{F}^$ is free, $\mathcal{F}^\bullet = (\operatorname{ker} \mathcal{F})^\uparrow$ is principal, and $\mathcal{F}^ \vee \mathcal{F}^\bullet = 2^X$.

Back

Section titled “Back”

Every filter $\mathcal{F}$ on $X$ can be uniquely decomposed as: $$\mathcal{F} = \mathcal{F}^* \wedge \mathcal{F}^\bullet$$ where $\mathcal{F}^$ is free, $\mathcal{F}^\bullet = (\operatorname{ker} \mathcal{F})^\uparrow$ is principal, and $\mathcal{F}^ \vee \mathcal{F}^\bullet = 2^X$.

Lean

Section titled “Lean”

本ノート RoyalRoad.ChapterII.thm_II_4_1（lake build 済み）