Metamath Recent Proofs http://us2.metamath.org:8888/mpeuni/mmrecent.html Recent proofs for Metamath proof system en 11262 : ancomd Commutation of conjuncts in consequent. ... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/DDoe4biEJsw/ancomd.html 13-Nov-2009   ⊢ (φ → (ψ ⋀ χ))    ⇒
   ⊢ (φ → (χ ⋀ ψ))
    ]]> http://us2.metamath.org:8888/mpeuni/ancomd.html 11530 : flimfnfcls A filter converges to a point iff every ... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/-u5FOGGxo6s/flimfnfcls.html 12-Nov-2009fclsfnflim 11529, this theorem illustrates the duality between convergence and clustering.
   ⊢ X = ∪J    &
   ⊢ Y = ∪F    ⇒
   ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (A ∈ ((fLim1 ‘J) ‘F) ↔ ∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g))))
    ]]> http://us2.metamath.org:8888/mpeuni/flimfnfcls.html 11529 : fclsfnflim A filter clusters at a point iff a finer... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/w0Ry-4hWSJc/fclsfnflim.html 12-Nov-2009   ⊢ X = ∪J    &
   ⊢ Y = ∪F    ⇒
   ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (A ∈ ((fClus ‘J) ‘F) ↔ ∃g ∈ Fil (X = ∪g ⋀ F ⊆ g ⋀ A ∈ ((fLim1 ‘J) ‘g))))
    ]]> http://us2.metamath.org:8888/mpeuni/fclsfnflim.html 11528 : flimfcls A limit point is a cluster point. ... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/-qvWY0H8664/flimfcls.html 12-Nov-2009   ⊢ X = ∪J    &
   ⊢ Y = ∪F    ⇒
   ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → ((fLim1 ‘J) ‘F) ⊆ ((fClus ‘J) ‘F))
    ]]> http://us2.metamath.org:8888/mpeuni/flimfcls.html 11527 : fcluscf Characterization of fineness of topologi... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/NXSxJeDdOis/fcluscf.html 12-Nov-2009
   ⊢ X = ∪J    &
   ⊢ Y = ∪K    ⇒
   ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ X = Y) → (J ⊆ K ↔ ∀f ∈ Fil (X = ∪f → ((fClus ‘K) ‘f) ⊆ ((fClus ‘J) ‘f))))
    ]]> http://us2.metamath.org:8888/mpeuni/fcluscf.html 11356 : supfil The supersets of a nonempty set which ar... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/Q9ceVO74Y04/supfil.html 12-Nov-2009   ⊢ ((A ∈ C ⋀ B ⊆ A ⋀ B ≠ ∅) → ({x∣(x ⊆ A ⋀ B ⊆ x)} ∈ Fil ⋀ A = ∪{x∣(x ⊆ A ⋀ B ⊆ x)}))
    ]]> http://us2.metamath.org:8888/mpeuni/supfil.html 11526 : fclusss A finer filter has fewer cluster points.... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/-w8D2xUOuEA/fclusss.html 11-Nov-2009   ⊢ X = ∪J    &
   ⊢ Y = ∪F    &
   ⊢ Z = ∪G    ⇒
   ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ G ∈ Fil) ⋀ X = Y ⋀ X = Z) ⋀ F ⊆ G) → ((fClus ‘J) ‘G) ⊆ ((fClus ‘J) ‘F))
    ]]> http://us2.metamath.org:8888/mpeuni/fclusss.html 11525 : fclusneii A neighborhood of a cluster point of a f... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/PQP0SmM3e0g/fclusneii.html 11-Nov-2009   ⊢ X = ∪J    &
   ⊢ Y = ∪F    ⇒
   ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ ((fClus ‘J) ‘F) ⋀ N ∈ ((nei ‘J) ‘{A})) ⋀ S ∈ F) → (N ∩ S) ≠ ∅)
    ]]> http://us2.metamath.org:8888/mpeuni/fclusneii.html 11524 : fclselbas A cluster point is in the base set. ... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/SR0SVFReyfI/fclselbas.html 11-Nov-2009   ⊢ X = ∪J    &
   ⊢ Y = ∪F    ⇒
   ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ ((fClus ‘J) ‘F)) → A ∈ X)
    ]]> http://us2.metamath.org:8888/mpeuni/fclselbas.html 11523 : fclusnei Cluster points in terms of neighborhoods... http://feedproxy.google.com/~r/MetamathRecentProofs/~3/4jvwr2ZGwBY/fclusnei.html 11-Nov-2009   ⊢ X = ∪J    &
   ⊢ Y = ∪F    ⇒
   ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (A ∈ ((fClus ‘J) ‘F) ↔ (A ∈ X ⋀ ∀n ∈ ((nei ‘J) ‘{A})∀s ∈ F (n ∩ s) ≠ ∅)))]]> http://us2.metamath.org:8888/mpeuni/fclusnei.html