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 21717
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 21716 . 2 class KQ
2 vj . . 3 setvar 𝑗
3 ctop 20917 . . 3 class Top
42cv 1629 . . . 4 class 𝑗
5 vx . . . . 5 setvar 𝑥
64cuni 4572 . . . . 5 class 𝑗
7 vy . . . . . . 7 setvar 𝑦
85, 7wel 2145 . . . . . 6 wff 𝑥𝑦
98, 7, 4crab 3064 . . . . 5 class {𝑦𝑗𝑥𝑦}
105, 6, 9cmpt 4861 . . . 4 class (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})
11 cqtop 16370 . . . 4 class qTop
124, 10, 11co 6792 . . 3 class (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦}))
132, 3, 12cmpt 4861 . 2 class (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
141, 13wceq 1630 1 wff KQ = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
Colors of variables: wff setvar class
This definition is referenced by:  kqval  21749  kqtop  21768  kqf  21770
  Copyright terms: Public domain W3C validator