Skip to content
Journals Garden

Isotonization $\mathcal{A}^\uparrow$ (上方閉化・記法) (Formula II.2.1)

  • Isotonization $\mathcal{A}^\uparrow$ (上方閉化・記法) (Formula II.2.1) #Card
    • $\mathcal{A}^\uparrow := {F \subset X : \exists A \in \mathcal{A},\ F \supset A}$; abbreviation $x^\uparrow := {{x}}^\uparrow$.

Back

Section titled “Back”

If $\mathcal{A} \subset 2^X$, then $$\mathcal{A}^\uparrow := {F \subset X : \exists A \in \mathcal{A},\ F \supset A}$$ （$\mathcal{A}$ の元を含む集合全体——上方閉化 / isotonization）.

  • $\mathcal{A}$ is isotone $\iff \mathcal{A} = \mathcal{A}^\uparrow$；$\mathcal{B}$ is a filter-base of $\mathcal{F}$ $\iff \mathcal{B}^\uparrow = \mathcal{F}$。
  • 略記 $x^\uparrow := {{x}}^\uparrow$（点 $x$ の主ウルトラフィルター）、${B}^\uparrow$ = principal filter。
  • 本書全体で最頻出の記法の一つ（(centered) 公理 $x \in \lim x^\uparrow$ など）。

Lean

Section titled “Lean”

Filter.principal（𝓟 s）が {s}^↑ に対応；𝓟 {x} = pure x が $x^\uparrow$