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 23703
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 23702 . 2 class KQ
2 vj . . 3 setvar 𝑗
3 ctop 22900 . . 3 class Top
42cv 1538 . . . 4 class 𝑗
5 vx . . . . 5 setvar 𝑥
64cuni 4906 . . . . 5 class 𝑗
7 vy . . . . . . 7 setvar 𝑦
85, 7wel 2108 . . . . . 6 wff 𝑥𝑦
98, 7, 4crab 3435 . . . . 5 class {𝑦𝑗𝑥𝑦}
105, 6, 9cmpt 5224 . . . 4 class (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})
11 cqtop 17549 . . . 4 class qTop
124, 10, 11co 7432 . . 3 class (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦}))
132, 3, 12cmpt 5224 . 2 class (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
141, 13wceq 1539 1 wff KQ = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
Colors of variables: wff setvar class
This definition is referenced by:  kqval  23735  kqtop  23754  kqf  23756
  Copyright terms: Public domain W3C validator