Topoloji Elde Etme Yöntemleri-I

Question

$X\neq \emptyset$ küme olmak üzere $i:2^X\to 2^X$ fonksiyonu her $A,B\in 2^X$ için

$I_1)$ $i(X)=X$

$I_2)$ $i(A)\subseteq A$

$I_3)$ $i(A\cap B)=i(A)\cap i(B)$

$I_4)$ $i(i(A))=i(A)$

koşullarını sağlasın.

$\mathbf{a)}$ $i$ fonksiyonu $I_1, I_2$ ve $I_3$ koşullarını sağladığında $X$ kümesinin $i(A)=A$ koşulu sağlayan tüm altkümelerinin oluşturduğu ailenin $X$ kümesi üzerinde bir topoloji olduğunu gösteriniz. Yani $\tau =\left\{A\subseteq X:i(A)=A\right\}\subseteq 2^X$ ailesinin $X$ kümesi üzerinde bir topoloji olduğunu gösteriniz.

$\mathbf{b)}$ $i$ fonksiyonu $I_1, I_2$ ve $I_3$ koşullarına ilave olarak $I_4$ koşulunu da sağladığında $i(A)=A^{\circ}$  $(a$ şıkkında elde edilen $\tau$ topolojisine göre) olduğunu gösteriniz.

Answer 1

$$ i^*(A) := X\setminus i(X\setminus A)$$ kuralı ile verilen $$i^* : 2^X\to 2^X$$ fonksiyonu bir Kuratowski Kapanış Operatörü olup $$\tau^* := \{A : i^*(X\setminus A) = X\setminus A \} = \tau$$ dır.

Answer 2

$\mathbf{a)}$ $\tau$ ailesinin topoloji olma koşullarını sağladığını gösterelim.

 

$\mathbf{T_1)}$ $i(X)\overset{I_1}{=}X\Rightarrow X\in \tau.$

$\left.\begin{array}{rr} i(\emptyset)\overset{I_2}{\subseteq}\emptyset \\ \\ i\in \left(2^X\right)^{\left(2^X\right)}\Rightarrow i(\emptyset)\in 2^X\Rightarrow \emptyset\subseteq i(\emptyset)\end{array}\right\}\Rightarrow i(\emptyset)=\emptyset\Rightarrow \emptyset\in\tau.$

 

$\mathbf{T_2)}$ $A,B\in\tau$ olsun.

$\left.\begin{array}{rr} A\in\tau\Rightarrow i(A)=A\\ \\ B\in\tau\Rightarrow i(B)=B\end{array}\right\}\Rightarrow A\cap B= i(A)\cap (B)\overset{I_3}{=} i(A\cap B)\Rightarrow A\cap B\in\tau.$

 

$\mathbf{T_3)}$ $\mathcal{A}\subseteq\tau$ olsun.

$A\in\mathcal{A}\subseteq\tau\Rightarrow i(A)=A\subseteq \bigcup_{A\in\mathcal{A}}A=\bigcup \mathcal{A}\Rightarrow A=i(A)\overset{*}{\subseteq} i\left(\bigcup \mathcal{A}\right) \Rightarrow\bigcup \mathcal{A} \subseteq i\left(\bigcup \mathcal{A}\right) \ldots (1)$

 

$\mathcal{A}\subseteq\tau \Rightarrow \bigcup\mathcal{A}\in 2^X\overset{I_2}{\Rightarrow} i\left(\bigcup\mathcal{A}\right)\subseteq \bigcup\mathcal{A} \ldots (2)$

 

$(1),(2)\Rightarrow i\left(\bigcup\mathcal{A}\right)=\bigcup\mathcal{A}\Rightarrow\bigcup\mathcal{A}\in\tau.$

 

$\begin{array}{rcl} (*) : A\subseteq B & \Rightarrow & A\cap B=A \\ & \Rightarrow &  i(A\cap B)=i(B) \\ & \overset{I_3}{\Rightarrow} &   i(A)\cap i(B)=i(B) \\ & \Rightarrow & i(A)\subseteq i(B).\end{array}$

 

O halde $\tau$ ailesi, $X$ kümesi üzerinde bir topoloji yani $(X,\tau)$ ikilisi bir topolojik uzaydır.

 

$\mathbf{b)}$ Şimdi de $$i(A)=A^{\circ}$$ yani $$\mathcal{A}:=\{B|(B\subseteq A)(B\in\tau)\}$$ olmak üzere $$i(A)=\cup\mathcal{A}$$ olduğunu yani $$i(A)=\max\mathcal{A}$$ olduğunu gösterelim. Bunun için $$i(A)\in\mathcal{A}$$ ve $$(\forall B\in\mathcal{A})(B\subseteq i(A))$$ olduğunu göstermemiz gerekir.

$\left.\begin{array}{rr} A\in 2^X\overset{I_2}{\Rightarrow} i(A)\subseteq A\\ \\ i(i(A))\overset{I_4}{=}i(A)\Rightarrow i(A)\in\tau \end{array}\right\}\Rightarrow i(A)\in\mathcal{A}\ldots (3)$

 

$B\in\mathcal{A}\Rightarrow (B\subseteq A)(B\in \tau)\overset{*}{\Rightarrow} B=i(B)\subseteq i(A)\ldots (4)$

 

$(3),(4)\Rightarrow i(A)=\max\mathcal{A}.$

 

Not: Buradaki maksimum $\left(2^X,\subseteq\right)$ posetine göre hesaplanmaktadır.

Answer 3

Ben de bu teoremi bilgisayar yardimi ile ispatlamaya calistim. yanlis formalize etmis olabilirim bir kontrol etmekte fayda var ama sanirim basarili oldum. `dafny` adli programlama dilini kullanarak matematiksel ispatlar yapmak mumkun (ve cok eglenceli/sinir bozucu). Su linkten bu dil hakkinda daha fazla bilgiye erisebilirsiniz

Ispati gereksiz uzatmis olabilirim (eminim daha kisa bir dafny programi ile ayni seyi ispatlayabilirz)

Kodu paylasiyorum

module Topoloji {

  ghost predicate TopolojiMi<T(!new)>(X: iset<T>, tau: iset<iset<T>>)
  {
    && X in tau
    && iset{} in tau
    && (forall A, B :: A in tau && B in tau ==> A * B in tau)
    && (forall Aile :: Aile <= tau ==> Birlesim(Aile) in tau)
  }

  ghost function Birlesim<T(!new)>(Aile: iset<iset<T>>): iset<T>
  {
    iset x | BirKumedeVar(x, Aile)
  }

  ghost predicate BirKumedeVar<T(!new)>(x: T, Aile: iset<iset<T>>)
  {
    exists S :: S in Aile && x in S
  }

  ghost predicate I1<T(!new)>(i: iset<T> -> iset<T>, X: iset<T>)
  {
    i(X) == X
  }

  ghost predicate I2<T(!new)>(i: iset<T> -> iset<T>, X: iset<T>)
  {
    forall A :: A <= X ==> i(A) <= A
  }

  ghost predicate I3<T(!new)>(i: iset<T> -> iset<T>, X: iset<T>)
  {
    forall A, B :: A <= X && B <= X ==> i(A * B) == i(A) * i(B)
  }

  ghost predicate I4<T(!new)>(i: iset<T> -> iset<T>, X: iset<T>)
  {
    forall A :: A <= X ==> i(i(A)) == i(A)
  }

  ghost function SabitNoktalar<T(!new)>(i: iset<T> -> iset<T>, X: iset<T>): iset<iset<T>>
  {
    iset A | A <= X && i(A) == A
  }

  ghost function Ic<T(!new)>(tau: iset<iset<T>>, A: iset<T>): iset<T>
  {
    Birlesim(iset B | B in tau && B <= A)
  }

  lemma SoruA<T(!new)>(X: iset<T>, i: iset<T> -> iset<T>)
    requires I1(i, X)
    requires I2(i, X)
    requires I3(i, X)
    ensures TopolojiMi(X, SabitNoktalar(i, X))
  {
    var tau := SabitNoktalar(i, X);
    
    assert i(X) == X;
    assert X in tau;
    
    BosKumeKapali(X, i);
    
    forall A, B | A in tau && B in tau
      ensures A * B in tau
    {
      KesisimKapali(X, i, A, B);
    }
    
    forall Aile | Aile <= tau
      ensures Birlesim(Aile) in tau
    {
      KeyfiBirlesimKapali(X, i, Aile);
    }
  }

  lemma BosKumeKapali<T(!new)>(X: iset<T>, i: iset<T> -> iset<T>)
    requires I2(i, X)
    ensures iset{} in SabitNoktalar(i, X)
  {
    var empty := iset{};
    assert i(empty) <= empty;
    assert empty <= i(empty);
    assert i(empty) == empty;
    assert empty <= X;
    assert empty in SabitNoktalar(i, X);
  }

  lemma KesisimKapali<T(!new)>(
    X: iset<T>, 
    i: iset<T> -> iset<T>, 
    A: iset<T>, 
    B: iset<T>
  )
    requires I3(i, X)
    requires A in SabitNoktalar(i, X)
    requires B in SabitNoktalar(i, X)
    ensures A * B in SabitNoktalar(i, X)
  {
    assert i(A) == A;
    assert i(B) == B;
    assert A <= X && B <= X;
    
    calc {
      i(A * B);
      { assert I3(i, X); }
      i(A) * i(B);
      A * B;
    }
    
    assert A * B <= X;
    assert A * B in SabitNoktalar(i, X);
  }

  lemma KeyfiBirlesimKapali<T(!new)>(
    X: iset<T>, 
    i: iset<T> -> iset<T>, 
    Aile: iset<iset<T>>
  )
    requires I2(i, X)
    requires I3(i, X)
    requires Aile <= SabitNoktalar(i, X)
    ensures Birlesim(Aile) in SabitNoktalar(i, X)
  {
    var U := Birlesim(Aile);
    
    Monoton(X, i);
    
    forall x | x in U
      ensures x in i(U)
    {
      var S :| S in Aile && x in S;
      assert S in SabitNoktalar(i, X);
      assert i(S) == S;
      assert x in S;
      assert S <= U;
      assert S <= X;
      assert U <= X;
      assert i(S) <= i(U);
      assert x in i(U);
    }
    assert U <= i(U);
    
    assert U <= X;
    assert i(U) <= U;
    
    assert i(U) == U;
    assert U in SabitNoktalar(i, X);
  }

  lemma Monoton<T(!new)>(X: iset<T>, i: iset<T> -> iset<T>)
    requires I3(i, X)
    ensures forall A, B :: A <= X && B <= X && A <= B ==> i(A) <= i(B)
  {
    forall A, B | A <= X && B <= X && A <= B
      ensures i(A) <= i(B)
    {
      assert A * B == A;
      
      calc {
        i(A);
        i(A * B);
        { assert I3(i, X); }
        i(A) * i(B);
      }
      
      assert i(A) * i(B) <= i(B);
      assert i(A) <= i(B);
    }
  }

  lemma SoruB<T(!new)>(X: iset<T>, i: iset<T> -> iset<T>, A: iset<T>)
    requires I1(i, X)
    requires I2(i, X)
    requires I3(i, X)
    requires I4(i, X)
    requires A <= X
    ensures var tau := SabitNoktalar(i, X);
            && i(A) in tau
            && i(A) <= A
            && (forall B :: B in tau && B <= A ==> B <= i(A))
            && i(A) == Ic(tau, A)
  {
    var tau := SabitNoktalar(i, X);
    
    assert i(i(A)) == i(A);
    assert i(A) <= X;
    assert i(A) in tau;
    assert i(A) <= A;
    
    Monoton(X, i);
    
    forall B | B in tau && B <= A
      ensures B <= i(A)
    {
      assert i(B) == B;
      assert B <= X;
      assert i(B) <= i(A);
      assert B <= i(A);
    }
    
    IcEsitligi(X, i, A);
  }

  lemma IcEsitligi<T(!new)>(X: iset<T>, i: iset<T> -> iset<T>, A: iset<T>)
    requires I1(i, X)
    requires I2(i, X)
    requires I3(i, X)
    requires I4(i, X)
    requires A <= X
    ensures i(A) == Ic(SabitNoktalar(i, X), A)
  {
    var tau := SabitNoktalar(i, X);
    var AcikAile := iset B | B in tau && B <= A;
    var ic := Ic(tau, A);
    
    assert i(A) in tau && i(A) <= A;
    assert i(A) in AcikAile;
    
    forall x | x in i(A)
      ensures x in ic
    {
      assert x in i(A);
      assert i(A) in AcikAile;
      assert BirKumedeVar(x, AcikAile);
      assert x in ic;
    }
    assert i(A) <= ic;
    
    forall x | x in ic
      ensures x in i(A)
    {
      var B :| B in AcikAile && x in B;
      assert B in tau && B <= A;
      assert i(B) == B;
      Monoton(X, i);
      assert B <= i(A);
      assert x in i(A);
    }
    assert ic <= i(A);
    
    assert i(A) == ic;
  }
}