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 21875
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 21874 . 2 class KQ
2 vj . . 3 setvar 𝑗
3 ctop 21075 . . 3 class Top
42cv 1655 . . . 4 class 𝑗
5 vx . . . . 5 setvar 𝑥
64cuni 4660 . . . . 5 class 𝑗
7 vy . . . . . . 7 setvar 𝑦
85, 7wel 2165 . . . . . 6 wff 𝑥𝑦
98, 7, 4crab 3121 . . . . 5 class {𝑦𝑗𝑥𝑦}
105, 6, 9cmpt 4954 . . . 4 class (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})
11 cqtop 16523 . . . 4 class qTop
124, 10, 11co 6910 . . 3 class (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦}))
132, 3, 12cmpt 4954 . 2 class (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
141, 13wceq 1656 1 wff KQ = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
Colors of variables: wff setvar class
This definition is referenced by:  kqval  21907  kqtop  21926  kqf  21928
  Copyright terms: Public domain W3C validator