Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Browser slow? Try the Unicode version.

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Color key:

Metamath Proof Explorer (1-4957)

Hilbert Space Explorer (4958-5787)

**Statement List for Metamath Proof Explorer -** 5401-5500 - Page 55 of 58
Type	Label	Description
Statement

Theorem	chdmm4 5401	DeMorgan's law for meet in a Hilbert lattice.


Theorem	chdmj1 5402	DeMorgan's law for join in a Hilbert lattice.


Theorem	chdmj2 5403	DeMorgan's law for join in a Hilbert lattice.


Theorem	chdmj3 5404	DeMorgan's law for join in a Hilbert lattice.


Theorem	chdmj4 5405	DeMorgan's law for join in a Hilbert lattice.


Theorem	chnle 5406	Equivalent expressions for "not less than" in the Hilbert lattice.


Theorem	chjass 5407	Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14.


Theorem	chj00 5408	Two Hilbert lattice elements are zero iff their join is zero.
$/\$

Theorem	chjo 5409	The join of a closed subspace and its orthocomplement.


Theorem	chj1 5410	Join with Hilbert lattice unit.


Theorem	chm0 5411	Meet with Hilbert lattice zero.


Theorem	shjshs 5412	Hilbert lattice join equals the double orthocomplement of subspace sum.


Theorem	shjshsel 5413	A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of [MaedaMaeda] p. 136.


Theorem	chj0t 5414	Join with Hilbert lattice zero.


Theorem	chslejt 5415	Subspace sum is smaller than subspace join. Remark of [Kalmbach] p. 65.
$/\$

Theorem	chinclt 5416	Closure of Hilbert lattice intersection.
$/\$

Theorem	chsscon3t 5417	Hilbert lattice contraposition law.
$/\$

Theorem	chsscon1t 5418	Hilbert lattice contraposition law.
$/\$

Theorem	chsscon2t 5419	Hilbert lattice contraposition law.
$/\$

Theorem	chpsscon3t 5420	Hilbert lattice contraposition law for strict ordering.
$/\$

Theorem	chpsscon1t 5421	Hilbert lattice contraposition law for strict ordering.
$/\$

Theorem	chpsscon2t 5422	Hilbert lattice contraposition law for strict ordering.
$/\$

Theorem	chjcomt 5423	Commutative law for Hilbert lattice join.
$/\$

Theorem	chub1t 5424	Hilbert lattice join is greater than or equal to its first argument.
$/\$

Theorem	chub2t 5425	Hilbert lattice join is greater than or equal to its second argument.
$/\$

Theorem	chlubt 5426	Hilbert lattice join is the least upper bound of two elements.
$/\$ $/\$ $/\$

Theorem	chlej1t 5427	Add join to both sides of Hilbert lattice ordering.
$/\$ $/\$

Theorem	chlej2t 5428	Add join to both sides of Hilbert lattice ordering.
$/\$ $/\$

Theorem	chlejb1t 5429	Hilbert lattice ordering in terms of join.
$/\$

Theorem	chlejb2t 5430	Hilbert lattice ordering in terms of join.
$/\$

Theorem	chnlet 5431	Equivalent expressions for "not less than" in the Hilbert lattice.
$/\$

Theorem	chabs1t 5432	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
$/\$

Theorem	chabs2t 5433	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
$/\$

Theorem	chabs1 5434	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.


Theorem	chabs2 5435	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.


Theorem	chjidmt 5436	Idempotent law for Hilbert lattice join.


Theorem	chjidm 5437	Idempotent law for Hilbert lattice join.


Theorem	chdmm1t 5438	DeMorgan's law for meet in a Hilbert lattice.
$/\$

Theorem	chdmm2t 5439	DeMorgan's law for meet in a Hilbert lattice.
$/\$

Theorem	chdmm3t 5440	DeMorgan's law for meet in a Hilbert lattice.
$/\$

Theorem	chdmm4t 5441	DeMorgan's law for meet in a Hilbert lattice.
$/\$

Theorem	chdmj1t 5442	DeMorgan's law for join in a Hilbert lattice.
$/\$

Theorem	chdmj2t 5443	DeMorgan's law for join in a Hilbert lattice.
$/\$

Theorem	chdmj3t 5444	DeMorgan's law for join in a Hilbert lattice.
$/\$

Theorem	chdmj4t 5445	DeMorgan's law for join in a Hilbert lattice.
$/\$

Theorem	chjasst 5446	Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14.
$/\$ $/\$

Theorem	ledi 5447	An ortholattice is distributive in one ordering direction.


Theorem	span0 5448	The span of the empty set is the zero subspace. Remark 11.6.e of [Schechter] p. 276.


Theorem	elspan 5449	Membership in the span of a subset of Hilbert space.


Theorem	spanun 5450	The span of a union is the subspace sum of spans.


Theorem	sshhococ 5451	The join of two Hilbert space subsets (not necessarily closed subspaces) equals the join of their closures (double orthocomplements).


Theorem	chne0t 5452	A non-zero closed subspace has a non-zero vector.


Theorem	chsup0 5453	The supremum of the empty set.
$\/H$

Theorem	h1deot 5454	Membership in orthocomplement of 1-dimensional subspace.
$/\$

Theorem	h1det 5455	Membership in 1-dimensional subspace.
$/\$

Theorem	h1did 5456	A generating vector belongs to the 1-dimensional subspace it generates.


Theorem	h1dn0 5457	A non-zero vector generates a (non-zero) 1-dimensional subspace.
$/\$

Theorem	h1de2 5458	Membership in 1-dimensional subspace. All members are collinear with the generating vector.