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

Definition df-kq 20633
 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 qTop
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-kq
StepHypRef Expression
1 ckq 20632 . 2 KQ
2 vj . . 3
3 ctop 19841 . . 3
42cv 1436 . . . 4
5 vx . . . . 5
64cuni 4213 . . . . 5
7 vy . . . . . . 7
85, 7wel 1868 . . . . . 6
98, 7, 4crab 2777 . . . . 5
105, 6, 9cmpt 4475 . . . 4
11 cqtop 15353 . . . 4 qTop
124, 10, 11co 6296 . . 3 qTop
132, 3, 12cmpt 4475 . 2 qTop
141, 13wceq 1437 1 KQ qTop
 Colors of variables: wff setvar class This definition is referenced by:  kqval  20665  kqtop  20684  kqf  20686
 Copyright terms: Public domain W3C validator