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 23718
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 23717 . 2 class KQ
2 vj . . 3 setvar 𝑗
3 ctop 22915 . . 3 class Top
42cv 1536 . . . 4 class 𝑗
5 vx . . . . 5 setvar 𝑥
64cuni 4912 . . . . 5 class 𝑗
7 vy . . . . . . 7 setvar 𝑦
85, 7wel 2107 . . . . . 6 wff 𝑥𝑦
98, 7, 4crab 3433 . . . . 5 class {𝑦𝑗𝑥𝑦}
105, 6, 9cmpt 5231 . . . 4 class (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})
11 cqtop 17550 . . . 4 class qTop
124, 10, 11co 7431 . . 3 class (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦}))
132, 3, 12cmpt 5231 . 2 class (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
141, 13wceq 1537 1 wff KQ = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 𝑗 ↦ {𝑦𝑗𝑥𝑦})))
Colors of variables: wff setvar class
This definition is referenced by:  kqval  23750  kqtop  23769  kqf  23771
  Copyright terms: Public domain W3C validator