MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-kq Structured version   Unicode version

Definition df-kq 20022
Description: Define the Kolmogorov quotient. This is a function on topologies which maps a topology to its quotient under the topological distinguishability map, which takes a point to the set of open sets that contain it. Two points are mapped to the same image under this function iff they are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.)
Assertion
Ref Expression
df-kq  |- KQ  =  ( j  e.  Top  |->  ( j qTop  ( x  e. 
U. j  |->  { y  e.  j  |  x  e.  y } ) ) )
Distinct variable group:    x, j, y

Detailed syntax breakdown of Definition df-kq
StepHypRef Expression
1 ckq 20021 . 2  class KQ
2 vj . . 3  setvar  j
3 ctop 19201 . . 3  class  Top
42cv 1378 . . . 4  class  j
5 vx . . . . 5  setvar  x
64cuni 4245 . . . . 5  class  U. j
7 vy . . . . . . 7  setvar  y
85, 7wel 1768 . . . . . 6  wff  x  e.  y
98, 7, 4crab 2818 . . . . 5  class  { y  e.  j  |  x  e.  y }
105, 6, 9cmpt 4505 . . . 4  class  ( x  e.  U. j  |->  { y  e.  j  |  x  e.  y } )
11 cqtop 14761 . . . 4  class qTop
124, 10, 11co 6285 . . 3  class  ( j qTop  ( x  e.  U. j  |->  { y  e.  j  |  x  e.  y } ) )
132, 3, 12cmpt 4505 . 2  class  ( j  e.  Top  |->  ( j qTop  ( x  e.  U. j  |->  { y  e.  j  |  x  e.  y } ) ) )
141, 13wceq 1379 1  wff KQ  =  ( j  e.  Top  |->  ( j qTop  ( x  e. 
U. j  |->  { y  e.  j  |  x  e.  y } ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  kqval  20054  kqtop  20073  kqf  20075
  Copyright terms: Public domain W3C validator