Benutzer:Daniel5Ko/Zeug

Bookmarks

... Browser- und Arbeitsplatz- unabhängig.

Foo

Konstruktives und ge-curry-tes Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \lnot(\phi\leftrightarrow\lnot\phi)} :

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{align} &q\colon ((\phi\to\bot)\to\phi) \to (\phi\to\phi\to\bot) \to \bot\\ &qfg:= h (f h)\text{ mit}\\ &\,\ h\colon \phi\to\bot \\ &\,\ h x := gxx \end{align} }

Domains

Scott-Topologie einer DCPO

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle (D, \leq)} eine DCPO. (Suprema von gerichteten Teilmengen)
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle U\subseteq D} heißt Scott-offen, wenn
- Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle U} Oberhalbmenge, also Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle x\leq y \Rightarrow (x\in U \Rightarrow y\in U)} ,
- für alle gerichteten Mengen $S\subseteq D$ gilt Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \textstyle\bigvee_D S\in U \Rightarrow S\cap U\neq\emptyset} .

Spezialisierungsordnung eines top. Raumes

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle X} topologischer Raum mit offenen Mengen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal OX} .
Für Punkte Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle p\in X} und Mengen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle V\subseteq X} Notation für Umgebungsrelation: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle p\prec V :\Longleftrightarrow \exists U\in\mathcal OX.\ p\in U\subseteq V}
Auf Punktmenge von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle X} definiere die Spezialisierungsordnung durch Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle x\sqsubseteq y:\Longleftrightarrow \forall V\subseteq X.\ x\prec V\Rightarrow y\prec V}
- Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sqsubseteq} offensichtlich reflexiv, transitiv.
- (Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T_0} -Axiom fordert: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sqsubseteq} ist außerdem antisymmetrisch,
- (Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T_1} -Axiom fordert: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sqsubseteq} ist außerdem antisymmetrisch und symmetrisch.)

Hin und zurück

Ist Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle (D,\leq)} eine DCPO, dann ist die Spezialisierungsordnung Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sqsubseteq} von D-mit-Scott-Topologie wieder $\leq$ .

Ein Satz Definitionen

Im folgenden immer Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle (D,\leq)} eine DCPO.
Way-below: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle {\ll} \subseteq D^2} , Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle x \ll y} falls für alle gerichteten $S\subseteq D$ gilt, $y\leq \bigvee S\Rightarrow \exists s\in S.\ x\leq s$ .
Stetige DCPO: Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle \{x\mid x\ll y\}} ist gerichtet, und Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle \bigvee \{x\mid x\ll y\}=y} .
Stetige Scott-Domain: Stetige DCPO, Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle \bigwedge X} ex. für alle nichtleeren $X\subseteq D$ .
Stetiger Verband: Vollständiger Verband, der stetige DCPO ist. (Oder auch: stetige DCPO, $\bigvee X$ ex. für alle endlichen $X\subseteq D$ ).
Algebraische DCPO: alle $x\in D$ sind darstellbar als ein $\bigvee B$ , wobei für alle $b\in B$ gilt $b\ll b$ und Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle b\leq x} . (Algebraische DCPOs sind stetig).
Scott-Domain: Stetige Scott-Domain, die algebraische DCPO ist.

Test

Lawvere-FP

In einer kart. abgeschl. Kat....

Def.: Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle f\colon X\to Z^{Y}} heißt schwach punktsurjektiv, wenn für alle $g\colon Y\to Z$ ex. ein $x\colon 1\to X$ , sodass für alle Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle y\colon 1\to Y}
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \operatorname{ev}\langle f x,y \rangle = g y} .
Def.: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle Z} hat Fixpunkteigenschaft, wenn für alle Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle t\colon Z\to Z} ein Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle z\colon 1\to Z} , sodass
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle z = tz} .
Satz: Gibt's ein Objekt $Y$ und ein schwach punktsurjektives Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle e\colon Y\to Z^Y} , so hat $Z$ die Fixpunkteigenschaft.
Beweis
- Sei Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle t\colon Z\to Z} beliebig. Definiere Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle g\colon Y \to Z} per Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle g = t\operatorname{ev}\langle e,\operatorname{id}_Y\rangle}
- Sei Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle x\colon 1\to Y} jenes mit für alle Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle y\colon 1\to Y} : Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \operatorname{ev}\langle e x,y \rangle = g y} .
- Dann ist Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \operatorname{ev}\langle e x,x \rangle = g x = t\operatorname{ev}\langle e,\operatorname{id}_Y\rangle x = t\operatorname{ev}\langle ex,x\rangle \quad\square} .
Korollare
- In Set mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle Z=2} und Kontraposition: Satz von Cantor.
- Und noch paar andere, z.B. in Richtung Bbkeit.

Haskell-Typechecker als Mikro-Proof-Assistant...

{-# LANGUAGE RankNTypes #-}
import Prelude hiding (not)
import Control.Arrow ((&&&))

data Absurd = Absurd { efq :: forall a. a }

type Not a = a -> Absurd
not :: (a -> b) -> Not b -> Not a
not = flip (.)

type Classic a = Not (Not a)
classic :: (a -> b) -> Classic a -> Classic b
classic = not . not

tripleNegElim :: Classic (Not a) -> Not a
tripleNegElim = not eta

eta :: a -> Classic a
eta = flip id

mu :: Classic (Classic a) -> Classic a
mu = tripleNegElim

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
s f g x = (f x) (g x)

excludedMiddle :: Classic (Either (Not a) a)
excludedMiddle = s (not Left) (not Right)

doubleNegElim :: Classic (Classic a -> a)
doubleNegElim = classic disjunctiveSyllogism excludedMiddle

disjunctiveSyllogism :: Either a b -> Not a -> b
disjunctiveSyllogism = foo efq

foo :: (Absurd -> b) -> Either a b -> Not a -> b
foo efb = either (flip $ (.) efb) const

-- Some DeMorgan stuff
forth :: (Not a, Not b) -> Not (Either a b)
forth = uncurry either

back :: Not (Either a b) -> (Not a, Not b)
back = not Left &&& not Right

forth2 :: Not (Not a, Not b) -> Classic (Either a b)
forth2 = not back

back2 :: Classic (Either a b) -> Not (Not a, Not b)
back2 = not forth

Das Supremum der Menge der Postfixpunkte einer monotonen Funktion f ist ein Fixpunkt von f...

{-# LANGUAGE RankNTypes, TypeOperators #-}

tarski :: (forall x y z. (x ≤ y, y ≤ z) -> x ≤ z)
       -> (forall x y. x ≤ y -> f x ≤ f y)
       -> (forall x. x ≤ f x -> x ≤ p)
       -> (forall q. (forall x. x ≤ f x -> x ≤ q) -> p ≤ q)
       -> (f p ≤ p, p ≤ f p)
tarski transitive monotone upperBound least = (pre, post) where
    pre  = upperBound (monotone post)
    post = least $ \h -> transitive (h, monotone (upperBound h))

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle (fx\leq a)\Longleftrightarrow (x\sqsubseteq ua)} impliziert Monotonität von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle f} und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle u} ...

aLemma :: (forall x. x ≤ x)
       -> (forall x y z. x ≤ y -> y ≤ z -> x ≤ z)
       -> (forall a. a ⊑ a)
       -> (forall a b c. a ⊑ b -> b ⊑ c -> a ⊑ c)
       -> (forall a x. f x ⊑ a -> x ≤ u a)
       -> (forall a x. x ≤ u a -> f x ⊑ a)
       -> (forall x y. x ≤ y -> f x ⊑ f y, forall a b. a ⊑ b -> u a ≤ u b)
aLemma reflX transX reflA transA phi psi = (foo, bar) where
	foo p = psi(p `transX` phi reflA)
	bar p = phi(psi reflX `transA` p)

Diagramme

2-Zellen

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{matrix} \mathcal C & \xrightarrow{\quad \operatorname{Id}\quad} & \!\mathcal C & \xrightarrow{\quad \operatorname{Id}\quad} & \!\mathcal C\\ \!\!\!F\Bigg\downarrow &\Downarrow \eta & \ \Bigg\uparrow G & \Downarrow \varepsilon & \ \Bigg\downarrow F \\ \mathcal D & \xrightarrow{\quad \operatorname{Id}\quad} & \!\mathcal D & \xrightarrow{\quad \operatorname{Id}\quad} & \!\mathcal D \end{matrix} }

2 Adjunktionen

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{array}{c} \mathcal OX \\ U'\Big\downarrow\!{\dashv}\!\Big\uparrow \mathrm{int} \\ \mathcal PX \\ \mathrm{cl}\Big\downarrow\!{\dashv}\!\Big\uparrow U \\ \mathcal CX \end{array}}

Noch eins.

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{array}{rcccl} 1 & \xrightarrow{\ulcorner h\urcorner} & N & \xrightarrow{\ h\ } & X\\ \ulcorner h\urcorner\Big\downarrow && \!\Delta\Big\downarrow&& \Big\downarrow \operatorname{id} \\ N && N^2 && X \\ h\Big\downarrow && e\Big\downarrow&& \Big\downarrow \operatorname{id} \\ X & \xrightarrow[\ \operatorname{id}\ ]{} & X & \xrightarrow[\ g\ ]{} & X \end{array}}

Bidirektionale ND-Regel u.ä.

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{array}{c} X\times S\to Y\\ \hline\hline X\to Y^S \end{array}(\operatorname{curry}) }

Tabelle

Kat	Ord, a.k.a. Hälfte weggeworfen.
Kategorie Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal C}	Menge Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle C} mit Quasiordnung Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \leq}
Objekt	Element
Morphismus	Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \leq} -"Zeuge" -- mit proof-irrelevance
Funktor Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal C\to\mathcal D}	monotone Funktion Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle C\to D}
nat. Trans Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle F\to G} , jeweils Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal C\to\mathcal D}	Zeuge für Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle F\leq_{D^C} G :\Longleftrightarrow \forall x\in C.\ Fx\leq_D Gx}
Funktorkategorie Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal D^{\mathcal C}}	Elemente: mon. Funktionen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle C\to D} , Ordnung: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \leq_{D^C}}
Monade	Hüllen-Op; d.h. Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T\colon C\to C} monoton, Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \eta: \operatorname{id}_C\leq_{C^C} T} , Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mu\colon T^2\leq_{C^C} T}
Set	Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Sigma := \{0\leq 1\}} scheint für die Zwecke hier zu reichen.
Hom-Funktor	Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle C(-,-)\colon C^{\text{op}}\times C\to \Sigma; C(x,y):=\begin{cases} 1 & x\leq_C y\\0&\text{sonst}\end{cases}}
Yoneda-Lemma	$F\colon C\to \Sigma$ monoton, Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle x\in C} . Dann: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle Fx = \Sigma^C (C(x,-), F)}

Damit zum Beispiel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle |\Sigma^{\Sigma^0}| = 2, |\Sigma^{\Sigma^1}| = 3, |\Sigma^{\Sigma^2}| = 6, |\Sigma^{\Sigma^3}| = 20, |\Sigma^{\Sigma^4}| = 168} (Siehe auch en:Dedekind number) und
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle |\Sigma| = 2, |\Sigma^\Sigma| = 3, |\Sigma^{\Sigma^\Sigma}| = 4, |\Sigma^{\Sigma^{\Sigma^\Sigma}}| = 5} usw.

Baz

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bullet\colon \forall A,B,C\in\mathcal C.\ \mathcal C(B,TC)\times \mathcal C(A,TB) \to \mathcal C(A,TC)} ,
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle f\circ(g\circ h) = (f\circ g)\circ h, \mathrm{id}\circ f = f = f\circ \mathrm{id}} ,
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle f\bullet(g\bullet h) = (f\bullet g)\bullet h, \eta\bullet f = f = f\bullet \eta} ,
$f\circ g=f\bullet (\eta \circ g)$ , (und damit auch Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle (f\bullet g)\circ h = f\bullet(g\circ h)} ).

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle Tf := (\eta\circ f)\bullet\mathrm{id}} ,
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mu := \mathrm{id} \bullet \mathrm{id}} .

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle Tf\circ\eta = ((\eta\circ f)\bullet\mathrm{id})\circ\eta = \eta\circ f} ,
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T\mathrm{id}=(\eta\circ\mathrm{id})\bullet \mathrm{id}= \eta\bullet\mathrm{id} = \mathrm{id}} ,
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T(f\circ g) = (\eta\circ f\circ g)\bullet\mathrm{id} = (Tf\circ\eta\circ g)\bullet\mathrm{id} = (\eta\circ f)\bullet(\eta\circ g)\bullet\mathrm{id} = ((\eta\circ f)\bullet\mathrm{id})\circ ((\eta\circ g)\bullet\mathrm{id}) = Tf\circ Tg, }
(Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mu\circ Tf = (\mathrm{id}\bullet\mathrm{id})\circ((\eta\circ f)\bullet\mathrm{id}) = \mathrm{id}\bullet (\eta\circ f) \bullet \mathrm{id} = f\bullet\mathrm{id}} )
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mu\circ T^2f = Tf\bullet\mathrm{id} = (\eta\circ f)\bullet\mathrm{id}\bullet\mathrm{id} = ((\eta\circ f)\bullet\mathrm{id})\circ(\mathrm{id}\bullet\mathrm{id}) = Tf\circ\mu} ,
Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle \mu \circ \eta =(\mathrm {id} \bullet \mathrm {id} )\circ \eta =\mathrm {id} } ,
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mu\circ T\eta = \eta\bullet\mathrm{id} = \mathrm{id}} ,
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mu\circ T\mu = \mu\bullet\mathrm{id} = \mathrm{id}\bullet\mathrm{id}\bullet\mathrm{id} = (\mathrm{id}\bullet\mathrm{id})\circ(\mathrm{id}\bullet\mathrm{id}) = \mu\circ\mu} .

ohne mathpartir

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{array}{c} \begin{array}{c} \Gamma\vdash M\colon \Pi x\colon A.\ B \\\hline \Gamma,x\colon A \vdash M\colon \Pi x\colon A.\ B \end{array}\ (\text{Weak}) \qquad \begin{array}{c}~\\\hline\Gamma,x\colon A\vdash x\colon A\end{array}\ (\text{Ax}) \\\hline \begin{array}{c} \Gamma,x\colon A\vdash Mx \colon B \\\hline \Gamma\vdash (\lambda x\colon A.\ Mx)\colon \Pi x\colon A.\ B \end{array}\ (\Pi\text{-Intro}) \end{array}\ (\Pi\text{-Elim})}

Merke:

texvc kann Kapitälchen nicht, jedenfalls nicht mit \textsc

Anonym

Suche

Benutzer:Daniel5Ko/Zeug

Namensräume

Mehr

Seitenaktionen

Inhaltsverzeichnis

Bookmarks

Foo

Domains

Scott-Topologie einer DCPO

Spezialisierungsordnung eines top. Raumes

Hin und zurück

Ein Satz Definitionen

Test

Lawvere-FP

Haskell-Typechecker als Mikro-Proof-Assistant...

Diagramme

2-Zellen

2 Adjunktionen

Noch eins.

Bidirektionale ND-Regel u.ä.

Tabelle

Baz

ohne mathpartir

Navigation

Navigation

Mitmachen

Wikiwerkzeuge

Wikiwerkzeuge

Anonym

Suche

Benutzer:Daniel5Ko/Zeug

Bookmarks

Foo

Domains

Scott-Topologie einer DCPO

Spezialisierungsordnung eines top. Raumes

Hin und zurück

Ein Satz Definitionen

Test

Lawvere-FP

Haskell-Typechecker als Mikro-Proof-Assistant...

Diagramme

2-Zellen

2 Adjunktionen

Noch eins.

Bidirektionale ND-Regel u.ä.

Tabelle

Baz

ohne mathpartir

Navigation

Wikiwerkzeuge

Seitenwerkzeuge

Weitere Projekte

Versteckte Kategorien