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

Definition df-kq 23689
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 = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
Distinct variable group:   𝑥,𝑗,𝑦

Detailed syntax breakdown of Definition df-kq
StepHypRef Expression
1 ckq 23688 . 2 class KQ
2 vj . . 3 setvar 𝑗
3 ctop 22886 . . 3 class Top
42cv 1533 . . . 4 class 𝑗
5 vx . . . . 5 setvar 𝑥
64cuni 4913 . . . . 5 class 𝑗
7 vy . . . . . . 7 setvar 𝑦
85, 7wel 2100 . . . . . 6 wff 𝑥𝑦
98, 7, 4crab 3419 . . . . 5 class {𝑦𝑗𝑥𝑦}
105, 6, 9cmpt 5236 . . . 4 class (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})
11 cqtop 17518 . . . 4 class qTop
124, 10, 11co 7424 . . 3 class (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦}))
132, 3, 12cmpt 5236 . 2 class (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
141, 13wceq 1534 1 wff KQ = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
Colors of variables: wff setvar class
This definition is referenced by:  kqval  23721  kqtop  23740  kqf  23742
  Copyright terms: Public domain W3C validator