HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-chj Structured version   Visualization version   GIF version

Definition df-chj 27342
Description: Define Hilbert lattice join. See chjval 27384 for its value and chjcl 27389 for its closure law. Note that we define it over all Hilbert space subsets to allow proving more general theorems. Even for general subsets the join belongs to C; see sshjcl 27387. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.)
Assertion
Ref Expression
df-chj = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥𝑦))))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-chj
StepHypRef Expression
1 chj 26963 . 2 class
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 chil 26949 . . . 4 class
54cpw 4011 . . 3 class 𝒫 ℋ
62cv 1473 . . . . . 6 class 𝑥
73cv 1473 . . . . . 6 class 𝑦
86, 7cun 3442 . . . . 5 class (𝑥𝑦)
9 cort 26960 . . . . 5 class
108, 9cfv 5689 . . . 4 class (⊥‘(𝑥𝑦))
1110, 9cfv 5689 . . 3 class (⊥‘(⊥‘(𝑥𝑦)))
122, 3, 5, 5, 11cmpt2 6427 . 2 class (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥𝑦))))
131, 12wceq 1474 1 wff = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  sshjval  27382
  Copyright terms: Public domain W3C validator