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

Definition df-kq 17385
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 17384 . 2  class KQ
2 vj . . 3  set  j
3 ctop 16631 . . 3  class  Top
42cv 1622 . . . 4  class  j
5 vx . . . . 5  set  x
64cuni 3827 . . . . 5  class  U. j
7 vy . . . . . . 7  set  y
85, 7wel 1685 . . . . . 6  wff  x  e.  y
98, 7, 4crab 2547 . . . . 5  class  { y  e.  j  |  x  e.  y }
105, 6, 9cmpt 4077 . . . 4  class  ( x  e.  U. j  |->  { y  e.  j  |  x  e.  y } )
11 cqtop 13406 . . . 4  class qTop
124, 10, 11co 5858 . . 3  class  ( j qTop  ( x  e.  U. j  |->  { y  e.  j  |  x  e.  y } ) )
132, 3, 12cmpt 4077 . 2  class  ( j  e.  Top  |->  ( j qTop  ( x  e.  U. j  |->  { y  e.  j  |  x  e.  y } ) ) )
141, 13wceq 1623 1  wff KQ  =  ( j  e.  Top  |->  ( j qTop  ( x  e. 
U. j  |->  { y  e.  j  |  x  e.  y } ) ) )
Colors of variables: wff set class
This definition is referenced by:  kqval  17417  kqtop  17436  kqf  17438
  Copyright terms: Public domain W3C validator