M.P.E. Home
Theorem List
Metamath Home
Metamath Mirrors
Most Recent Proofs
| M.P.E. Home
Theorem List Metamath Home Metamath Mirrors |
Metamath Proof
Explorer
Most Recent Proofs | A theorem a day prevents mental decay. —mathematician Eric Charles Milner (1928-1997) |
Some users have reported that they cannot always access this page, apparently because port 8888 is sometimes mysteriously blocked. I added two other ports, and this page can now be accessed via ports 88, 443, and 8888. You can discuss this problem here. — Norm 24 Jun 2008
| Color key: |
Metamath Proof Explorer |
Hilbert Space Explorer
(and user's sandboxes at the end) |
| Date | Label | Description |
|---|---|---|
| Theorem | ||
| 23-Jul-2008 | ef01tllem2 7344 | Lemma for ef01tlub 7345. |
| ⊢ F = {⟨j, y⟩∣(j ∈ ℕ0 ⋀ y = ((A↑j) / (! ‘j)))} & ⊢ G = {⟨j, y⟩∣(j ∈ ℕ0 ⋀ y = ((A↑(j − M)) / (! ‘j)))} & ⊢ H = {⟨j, y⟩∣(j ∈ ℕ0 ⋀ y = ((1↑j) / (! ‘j)))} & ⊢ M ∈ ℕ & ⊢ A ∈ (0(,]1) ⇒ ⊢ Σk ∈ (ℤ≥ ‘M)(F ‘k) ≤ ((A↑M) · ((M + 1) / ((! ‘M) · M))) | ||
| 23-Jul-2008 | ef01tllem1 7343 | Lemma for ef01tlub 7345. |
| ⊢ F = {⟨j, y⟩∣(j ∈ ℕ0 ⋀ y = ((A↑j) / (! ‘j)))} & ⊢ G = {⟨j, y⟩∣(j ∈ ℕ0 ⋀ y = ((A↑(j − M)) / (! ‘j)))} & ⊢ M ∈ ℕ & ⊢ A ∈ ℝ & ⊢ A ≠ 0 ⇒ ⊢ (⟨M, + ⟩seqG) ⇝ (Σk ∈ (ℤ≥ ‘M)(F ‘k) / (A↑M)) | ||
| 23-Jul-2008 | nn0opthlem2 6610 | Lemma for nn0opth 6612. |
| ⊢ A ∈ ℕ0 & ⊢ B ∈ ℕ0 & ⊢ C ∈ ℕ0 & ⊢ D ∈ ℕ0 ⇒ ⊢ ((B ≤ A ⋀ D ≤ C) → (A < C → ((C · C) + D) ≠ ((A · A) + B))) | ||
| 23-Jul-2008 | rnex 3357 | The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. |
| ⊢ A ∈ V ⇒ ⊢ ran A ∈ V | ||
| 22-Jul-2008 | idfisf 10671 | The identity functor is a functor. (Part of FL's sandbox.) |
| ⊢ (T ∈ Cat → (I ↾ dom (dom ‘T)) ∈ (Func ‘⟨T, T⟩)) | ||
| 22-Jul-2008 | plimfil 10526 | The predicate "is a limit of a filter". (Part of FL's sandbox.) |
| ⊢ X = ∪J ⇒ ⊢ ((J ∈ Top ⋀ F ∈ (Fil ∩ ℘℘X) ⋀ L ∈ X) → (L ∈ ((fLim1 ‘J) ‘F) ↔ ((nei ‘J) ‘{L}) ⊆ F)) | ||
| 22-Jul-2008 | limfillem2 10525 | The limits of a filter on X. (Part of FL's sandbox.) |
| ⊢ X = ∪J ⇒ ⊢ ((J ∈ Top ⋀ F ∈ (Fil ∩ ℘℘X)) → ((fLim1 ‘J) ‘F) = {l ∈ X∣((nei ‘J) ‘{l}) ⊆ F}) | ||
| 22-Jul-2008 | limfillem1 10524 | The limits of a filter on X. (Part of FL's sandbox.) |
| ⊢ J ∈ Top & ⊢ X = ∪J ⇒ ⊢ (F ∈ (Fil ∩ ℘℘X) → ((fLim1 ‘J) ‘F) = {l ∈ X∣((nei ‘J) ‘{l}) ⊆ F}) | ||
| 22-Jul-2008 | sfvlim 10523 | Functions whose values are the limits of the filters. (Part of FL's sandbox.) |
| ⊢ X = ∪J ⇒ ⊢ (J ∈ Top → (fLim1 ‘J) = {⟨a, b⟩∣(a ∈ (Fil ∩ ℘℘X) ⋀ b = {l ∈ X∣((nei ‘J) ‘{l}) ⊆ a})}) | ||
| 22-Jul-2008 | rcfpfil 10518 | Relative complements of the finite parts of an infinite set is a filter. When A = ℕ the set of the relative complements is called Frechet's filter and is used to define the concept of limit of a sequence. (Part of FL's sandbox.) |
| ⊢ ((A ∈ B ⋀ ¬ ∃x ∈ ω A ≈ x) → {x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))} ∈ Fil) | ||
| 22-Jul-2008 | rcfpfillem6 10517 | Lemma for rcfpfil 10518. (Part of FL's sandbox.) |
| ⊢ ((u ∈ {x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))} ⋀ v ⊆ A ⋀ u ⊆ v) → v ∈ {x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))}) | ||
| 22-Jul-2008 | rcfpfillem5 10516 | Lemma for rcfpfil 10518. (Part of FL's sandbox.) |
| ⊢ (A ∈ B → A ∈ {x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))}) | ||
| 22-Jul-2008 | rcfpfillem4 10515 | Lemma for rcfpfil 10518. (Part of FL's sandbox.) |
| ⊢ (A ∈ B → ∀u ∈ {x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))}∀v ∈ {x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))} (u ∩ v) ∈ {x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))}) | ||
| 22-Jul-2008 | rcfpfillem3 10514 | Lemma for rcfpfil 10518. (Part of FL's sandbox.) |
| ⊢ (A ∈ B → ∪{x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))} = A) | ||
| 22-Jul-2008 | rcfpfillem2 10513 | Lemma for rcfpfil 10518. (Part of FL's sandbox.) |
| ⊢ (¬ ∃x ∈ ω A ≈ x → ¬ ∅ ∈ {x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))}) | ||
| 22-Jul-2008 | rcfpfillem1 10512 | Lemma for rcfpfil 10518. (Part of FL's sandbox.) |
| ⊢ (B ∈ C → (B ∈ {x∣∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ x = (A ∖ b))} ↔ ∃b(b ⊆ A ⋀ ∃z ∈ ω b ≈ z ⋀ B = (A ∖ b)))) | ||
| 22-Jul-2008 | emfin 10431 | The empty set is finite. (Part of FL's sandbox.) |
| ⊢ ∃x ∈ ω ∅ ≈ x | ||
| 22-Jul-2008 | ompfl3 10386 | Remove a hypothesis from the second member of a biimplication. (Part of FL's sandbox.) |
| ⊢ ((φ ⋀ ψ ⋀ χ) → (θ ↔ (χ ⋀ τ))) ⇒ ⊢ ((φ ⋀ ψ ⋀ χ) → (θ ↔ τ)) | ||
| 21-Jul-2008 | nvcni2 8295 | Epsilon-delta property of a continuous operator. (Normed complex vector space version of metcni 7857.) |
| ⊢ X = (Base ‘U) & ⊢ M = (norm ‘U) & ⊢ N = (norm ‘W) & ⊢ R = ( −v ‘U) & ⊢ S = ( −v ‘W) & ⊢ C = (IndMet ‘U) & ⊢ D = (IndMet ‘W) & ⊢ J = (Open ‘C) & ⊢ K = (Open ‘D) ⇒ ⊢ (((U ∈ NrmCVec ⋀ W ∈ NrmCVec ⋀ F ∈ (J Cn K)) ⋀ (P ∈ X ⋀ A ∈ ℝ ⋀ 0 < A)) → ∃x ∈ ℝ (0 < x ⋀ ∀y ∈ X ((M ‘(PRy)) ≤ x → (N ‘((F ‘P)S(F ‘y))) ≤ A))) | ||
| 20-Jul-2008 | nvcnpf 8293 | A continuous function is an operation (normed complex vector space version of cnpf 7724). |
| ⊢ X = (Base ‘U) & ⊢ Y = (Base ‘W) & ⊢ C = (IndMet ‘U) & ⊢ D = (IndMet ‘W) & ⊢ J = (Open ‘C) & ⊢ K = (Open ‘D) ⇒ ⊢ (((U ∈ NrmCVec ⋀ W ∈ NrmCVec ⋀ P ∈ X) ⋀ F ∈ ((J CnP K) ‘P)) → F:X–→Y) | ||
| 19-Jul-2008 | nvoprne 8271 | The vector addition and scalar product operations are not identical. |
| ⊢ (⟨⟨G, S⟩, N⟩ ∈ NrmCVec → G ≠ S) | ||
| 18-Jul-2008 | expnlbndt 6600 | The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. |
| ⊢ ((A ∈ ℝ+ ⋀ B ∈ ℝ ⋀ 1 < B) → ∃k ∈ ℕ (1 / (B↑k)) < A) | ||
| 18-Jul-2008 | rpne0t 6238 | A positive real is nonzero. |
| ⊢ (A ∈ ℝ+ → A ≠ 0) | ||
| 17-Jul-2008 | infpss 7535 | Every infinite set has an equinumerous proper subset. Exercise 7 of [TakeutiZaring] p. 91. |
| ⊢ A ∈ V ⇒ ⊢ (ω ≼ A → ∃x(x ⊂ A ⋀ x ≈ A)) | ||
| 16-Jul-2008 | relelrng 3343 | The second argument of a binary relation belongs to its range. |
| ⊢ ((B ∈ C ⋀ Rel R ⋀ ARB) → B ∈ ran R) | ||
| 15-Jul-2008 | fraclt1t 6189 | The fractional part of a real number is less than one. |
| ⊢ (A ∈ ℝ → (A − (⌊ ‘A)) < 1) | ||
| 15-Jul-2008 | flreclt 6185 | The floor (greatest integer) function is real. |
| ⊢ (A ∈ ℝ → (⌊ ‘A) ∈ ℝ) | ||
| 14-Jul-2008 | dmdbr7at 10308 | Dual modular pair property in terms of atoms. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A Mℋ* B ↔ ∀x ∈ Atoms ((A ∨ℋ B) ∩ x) ⊆ (((x ∨ℋ B) ∩ A) ∨ℋ B)) | ||
| 14-Jul-2008 | syld3an1 870 | A syllogism inference. |
| ⊢ ((φ ⋀ ψ ⋀ χ) → θ) & ⊢ ((τ ⋀ ψ ⋀ χ) → φ) ⇒ ⊢ ((τ ⋀ ψ ⋀ χ) → θ) | ||
| 13-Jul-2008 | dmdbr4at 10305 | Dual modular pair property in terms of atoms. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A Mℋ* B ↔ ∀x ∈ Atoms ((x ∨ℋ B) ∩ (A ∨ℋ B)) ⊆ (((x ∨ℋ B) ∩ A) ∨ℋ B)) | ||
| 12-Jul-2008 | atdmd2 10298 | Two Hilbert lattice elements have the dual modular pair property if the second is an atom. |
| ⊢ ((A ∈ Cℋ ⋀ B ∈ Atoms) → A Mℋ* B) | ||
| 12-Jul-2008 | dmdbr5 10192 | Binary relation expressing the dual modular pair property. |
| ⊢ ((A ∈ Cℋ ⋀ B ∈ Cℋ ) → (A Mℋ* B ↔ ∀x ∈ Cℋ (x ⊆ (A ∨ℋ B) → x ⊆ (((x ∨ℋ B) ∩ A) ∨ℋ B)))) | ||
| 11-Jul-2008 | clmfnn 7047 | Express the predicate F converges to A for an explicit function, using natural numbers. |
| ⊢ ((F:ℕ–→ℂ ⋀ A ∈ ℂ) → (F ⇝ A ↔ ∀x ∈ ℝ+ ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → (abs ‘((F ‘k) − A)) < x))) | ||
| 10-Jul-2008 | metcls 7929 | The closure of a subset of a metric space is equal to its points of convergence. Theorem 1.4-6(a) of [Kreyszig] p. 30. |
| ⊢ X = dom dom D & ⊢ J = (Open ‘D) ⇒ ⊢ ((D ∈ Met ⋀ M ⊆ X) → ((cls ‘J) ‘M) = {x∣∃f(f:ℕ–→M ⋀ f(⇝m ‘D)x)}) | ||
| 10-Jul-2008 | expne0t 6531 | Natural number exponentiation is nonzero iff its mantissa is nonzero. |
| ⊢ ((A ∈ ℂ ⋀ N ∈ ℕ) → ((A↑N) ≠ 0 ↔ A ≠ 0)) | ||
| 9-Jul-2008 | iscaunns 7907 | Express the property "F is a Cauchy sequence of metric D." |
| ⊢ X = dom dom D & ⊢ (k ∈ ℕ → A = (F ‘k)) ⇒ ⊢ ((D ∈ Met ⋀ F:ℕ–→X) → (F ∈ (Cau ‘D) ↔ ∀x ∈ ℝ+ ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → ([j / k]ADA) < x))) | ||
| 8-Jul-2008 | nmopub2tHIL 9792 | An upper bound for an operator norm. |
| ⊢ ((T: ℋ –→ ℋ ⋀ (A ∈ ℝ ⋀ 0 ≤ A) ⋀ ∀x ∈ ℋ (normh ‘(T ‘x)) ≤ (A · (normh ‘x))) → (normop ‘T) ≤ A) | ||
| 8-Jul-2008 | projlemHIL 9174 | Lemma 3.6 of [Beran] p. 101: "Let H be a complete subspace of a (pre-)Hilbert space ℋ and let A ∈ ℋ. Then there exists a vector x ∈ H such that (norm ‘(x −h A)) ≤ (norm ‘(y −h A)) for every y ∈ H." This is a lemma for the projection theorem. |
| ⊢ A ∈ ℋ & ⊢ H ∈ Cℋ ⇒ ⊢ ∃x ∈ H ∀y ∈ H (normh ‘(x −h A)) ≤ (normh ‘(y −h A)) | ||
| 8-Jul-2008 | climabs0OLD 7067 | Convergence to zero of the absolute value implies convergence to zero. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ (k ∈ ℕ → (G ‘k) = (abs ‘(F ‘k))) ⇒ ⊢ ((∀k ∈ ℕ (F ‘k) ∈ ℂ ⋀ G ⇝ 0) → F ⇝ 0) | ||
| 7-Jul-2008 | dmdi2 10188 | Consequence of the dual modular pair property. |
| ⊢ (((A ∈ Cℋ ⋀ B ∈ Cℋ ⋀ C ∈ Cℋ ) ⋀ (A Mℋ* B ⋀ B ⊆ C)) → (C ∩ (A ∨ℋ B)) ⊆ ((C ∩ A) ∨ℋ B)) | ||
| 7-Jul-2008 | spwpr2 8616 | Property of supremum defining condition for an unordered pair. |
| ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ (((R ∈ T ⋀ A = {B, C}) ⋀ (B ∈ U ⋀ C ∈ W)) → (φ ↔ ((BRx ⋀ CRx) ⋀ ∀y ∈ X ((BRy ⋀ CRy) → xRy)))) | ||
| 7-Jul-2008 | 2pwuninel 4476 | The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. |
| ⊢ ¬ ℘℘∪A ∈ A | ||
| 7-Jul-2008 | dmex 3356 | The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. |
| ⊢ A ∈ V ⇒ ⊢ dom A ∈ V | ||
| 6-Jul-2008 | lmbrnns 7905 | Express the binary relation "sequence F converges to point P " in a metric space." |
| ⊢ X = dom dom D & ⊢ (k ∈ ℕ → A = (F ‘k)) ⇒ ⊢ ((D ∈ Met ⋀ P ∈ X ⋀ F:ℕ–→X) → (F(⇝m ‘D)P ↔ ∀x ∈ ℝ+ ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → (ADP) < x))) | ||
| 6-Jul-2008 | releldm 3342 | The first argument of a binary relation belongs to its domain. |
| ⊢ ((Rel R ⋀ ARB) → A ∈ dom R) | ||
| 5-Jul-2008 | pjocco 10063 | Composition of projections of a subspace and its orthocomplement. |
| ⊢ H ∈ Cℋ ⇒ ⊢ ((proj ‘H) ∘ (proj ‘(⊥ ‘H))) = 0hop | ||
| 5-Jul-2008 | leoptrt 10027 | The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49. |
| ⊢ (((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) ⋀ (S ≤op T ⋀ T ≤op U)) → S ≤op U) | ||
| 5-Jul-2008 | iscau4 7903 | Express the property "F is a Cauchy sequence of metric D." |
| ⊢ X = dom dom D ⇒ ⊢ (D ∈ Met → (F ∈ (Cau ‘D) ↔ (F ⊆ (ℂ × X) ⋀ ∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ ℤ (j ≤ k → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x)))))) | ||
| 4-Jul-2008 | bracnlnvalt 10004 | The vector that a continuous linear functional is the bra of. |
| ⊢ (T ∈ (LinFn ∩ ConFn) → T = (bra ‘∪{y ∈ ℋ ∣∀x ∈ ℋ (T ‘x) = (x ·ih y)})) | ||
| 3-Jul-2008 | unisn3 2872 | Union of a singleton in the form of a restricted class abstraction. |
| ⊢ (A ∈ B → ∪{x ∈ B∣x = A} = A) | ||
| 2-Jul-2008 | nmopcoadj0 9993 | An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106. |
| ⊢ T ∈ BndLinOp ⇒ ⊢ ((T ∘ (adjh ‘T)) = 0hop ↔ T = 0hop ) | ||
| 2-Jul-2008 | sylancom 475 | Syllogism inference with commutation of antecents. |
| ⊢ ((φ ⋀ ψ) → χ) & ⊢ ((χ ⋀ ψ) → θ) ⇒ ⊢ ((φ ⋀ ψ) → θ) | ||
| 1-Jul-2008 | supmax 4572 | The greatest element of a set is the supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
| ⊢ R Or A ⇒ ⊢ ((C ∈ A ⋀ C ∈ B ⋀ ∀y ∈ B ¬ CRy) → sup(B, A, R) = C) | ||
| 1-Jul-2008 | supmaxlem 4571 | A set that contains a greatest element satisfies the antecedent in supremum theorems. This allows sup(A, B, R) to be used in some situations without the completeness axiom. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
| ⊢ ((C ∈ A ⋀ C ∈ B ⋀ ∀z ∈ B ¬ CRz) → ∃x ∈ A (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) | ||
| 1-Jul-2008 | opelxpex2 3275 | The second member of an ordered pair of classes in a cross product exists when the order pair doesn't belong to I. |
| ⊢ (⟨A, B⟩ ∈ ((C × D) ∖ I) → B ∈ V) | ||
| 30-Jun-2008 | adjeq0 9981 | An operator is zero iff its adjoint is zero. Theorem 3.11(i) of [Beran] p. 106. |
| ⊢ (T = 0hop ↔ (adjh ‘T) = 0hop ) | ||
| 30-Jun-2008 | hhsshl 9108 | Hilbert space property of a closed subspace. |
| ⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩ & ⊢ H ∈ Cℋ ⇒ ⊢ W ∈ CHil | ||
| 29-Jun-2008 | hhssims2 9102 | Induced metric of a subspace. |
| ⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩ & ⊢ D = (IndMet ‘W) & ⊢ H ∈ Sℋ ⇒ ⊢ D = ((normh ∘ −h ) ↾ (H × H)) | ||
| 29-Jun-2008 | brelrn 3340 | The second argument of a binary relation belongs to its range. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (ACB → B ∈ ran C) | ||
| 29-Jun-2008 | brelrng 3339 | The second argument of a binary relation belongs to its range. |
| ⊢ ((A ∈ F ⋀ B ∈ G ⋀ ACB) → B ∈ ran C) | ||
| 29-Jun-2008 | ordtri3or 2975 | A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38. |
| ⊢ ((Ord A ⋀ Ord B) → (A ∈ B ⋁ A = B ⋁ B ∈ A)) | ||
| 29-Jun-2008 | moi2 1921 | Consequence of "at most one." |
| ⊢ (x = A → (φ ↔ ψ)) ⇒ ⊢ (((A ∈ B ⋀ ∃*xφ) ⋀ (φ ⋀ ψ)) → x = A) | ||
| 28-Jun-2008 | rehaus 7880 | The standard topology on the reals is Hausdorff. |
| ⊢ (topGen ‘ran (,)) ∈ Haus | ||
| 27-Jun-2008 | hhssims 9101 | Induced metric of a subspace. |
| ⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩ & ⊢ H ∈ Sℋ & ⊢ D = ((normh ∘ −h ) ↾ (H × H)) ⇒ ⊢ D = (IndMet ‘W) | ||
| 27-Jun-2008 | hhsssh2 9096 | The predicate "H is a subspace of Hilbert space." |
| ⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩ ⇒ ⊢ (H ∈ Sℋ ↔ (W ∈ NrmCVec ⋀ H ⊆ ℋ )) | ||
| 27-Jun-2008 | pwuninel 4475 | The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. |
| ⊢ ¬ ℘∪A ∈ A | ||
| 26-Jun-2008 | oteqex 2795 | Equivalence of existence implied by equality of ordered triples. |
| ⊢ (⟨⟨A, B⟩, C⟩ = ⟨⟨R, S⟩, T⟩ → (A ∈ V ↔ R ∈ V)) | ||
| 25-Jun-2008 | nvdm 8254 | Two ways to express the set of vectors in a normed complex vector space. |
| ⊢ G = ( +v ‘U) & ⊢ N = (norm ‘U) ⇒ ⊢ (U ∈ NrmCVec → (X = dom N ↔ X = ran G)) | ||
| 24-Jun-2008 | hhssablt 9089 | Abelian group property of subspace addition. |
| ⊢ (H ∈ Sℋ → ( +h ↾ (H × H)) ∈ Abel) | ||
| 24-Jun-2008 | spwnex 8619 | Non-closure when the supremum doesn't exist. |
| ⊢ X = dom R & ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ ((R ∈ Poset ⋀ A ∈ W ⋀ ¬ ∃x ∈ X φ) → ¬ (R supw A) ∈ X) | ||
| 23-Jun-2008 | axhilex 8807 |
Derive axiom ax-hilex 8825 from Hilbert space under ZF set theory.
Before introducing the 18 axioms for Hilbert space, we first prove them as the conclusions of theorems axhilex 8807 through axhcompl 8824, using ZFC set theory only. These show that if we are given a known, fixed Hilbert space U = ⟨⟨ +h , ·h ⟩, normh⟩ that satisfies their hypotheses, then we can derive the Hilbert space axioms as theorems of ZFC set theory. In practice, in order to use these theorems to convert the Hilbert Space explorer to a ZFC-only subtheory, we would also have to provide definitions for the 3 (otherwise primitive) class constants +h, ·h, and ·ih before df-hnorm 8793 above. See also the comment in ax-hilex 8825. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil ⇒ ⊢ ℋ ∈ V | ||
| 23-Jun-2008 | metnei 7841 | The neighborhoods around a point P of a metric space are those subsets containing a ball around P. Definition of neighborhood in [Kreyszig] p. 19. |
| ⊢ X = dom dom D & ⊢ J = (Open ‘D) ⇒ ⊢ ((D ∈ Met ⋀ P ∈ X) → ((nei ‘J) ‘{P}) = {x∣(x ⊆ X ⋀ ∃r ∈ ℝ (0 < r ⋀ (P( ball ‘D)r) ⊆ x))}) | ||
| 22-Jun-2008 | axhcompl 8824 | Derive axiom ax-hcompl 9027 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil ⇒ ⊢ (F ∈ Cauchy → ∃x ∈ ℋ F ⇝v x) | ||
| 22-Jun-2008 | axhis4 8823 | Derive axiom ax-his4 8908 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil & ⊢ ·ih = ( ·i ‘U) ⇒ ⊢ ((A ∈ ℋ ⋀ A ≠ 0h) → 0 < (A ·ih A)) | ||
| 22-Jun-2008 | metne0 7784 | A metric space is nonempty iff its base set is nonempty. |
| ⊢ X = dom dom D ⇒ ⊢ (D ∈ Met → (D ≠ ∅ ↔ X ≠ ∅)) | ||
| 21-Jun-2008 | axhis3 8822 | Derive axiom ax-his3 8907 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil & ⊢ ·ih = ( ·i ‘U) ⇒ ⊢ ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → ((A ·h B) ·ih C) = (A · (B ·ih C))) | ||
| 21-Jun-2008 | axhis2 8821 | Derive axiom ax-his2 8906 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil & ⊢ ·ih = ( ·i ‘U) ⇒ ⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → ((A +h B) ·ih C) = ((A ·ih C) + (B ·ih C))) | ||
| 21-Jun-2008 | axhis1 8820 | Derive axiom ax-his1 8905 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil & ⊢ ·ih = ( ·i ‘U) ⇒ ⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ) → (A ·ih B) = (∗ ‘(B ·ih A))) | ||
| 21-Jun-2008 | axhfi 8819 | Derive axiom ax-hfi 8902 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil & ⊢ ·ih = ( ·i ‘U) ⇒ ⊢ ·ih :( ℋ × ℋ )–→ℂ | ||
| 21-Jun-2008 | iscnp2 7722 | The predicate "F is a continuous function from topology J to topology K at point P." |
| ⊢ X = ∪J & ⊢ Y = ∪K ⇒ ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ P ∈ X) → (F ∈ ((J CnP K) ‘P) ↔ (F:X–→Y ⋀ ∀y ∈ K ((F ‘P) ∈ y → ∃x ∈ J (P ∈ x ⋀ x ⊆ (◡F “ y)))))) | ||
| 20-Jun-2008 | dveeq1ALT 1354 | Version of dveeq1 1353 using ax-16 1209 instead of ax-17 970. |
| ⊢ (¬ ∀x x = y → (y = z → ∀x y = z)) | ||
| 19-Jun-2008 | axhvmul0 8818 | Derive axiom ax-hvmul0 8836 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil ⇒ ⊢ (A ∈ ℋ → (0 ·h A) = 0h) | ||
| 19-Jun-2008 | axhvdistr2 8817 | Derive axiom ax-hvdistr2 8835 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil ⇒ ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℋ ) → ((A + B) ·h C) = ((A ·h C) +h (B ·h C))) | ||
| 19-Jun-2008 | dveeq2ALT 1212 | Version of dveeq2 1211 using ax-16 1209 instead of ax-17 970. |
| ⊢ (¬ ∀x x = y → (z = y → ∀x z = y)) | ||
| 18-Jun-2008 | pstr 8610 | A poset is transitive. |
| ⊢ ((R ∈ Poset ⋀ ARB ⋀ BRC) → ARC) | ||
| 17-Jun-2008 | ee7.2a 10384 | Lemma for Euclid's Elements, Book 7, proposition 2. The original mentions the smaller measure being 'continually subtracted' from the larger. Many authors interpret this phrase as A mod B. Here, just one subtraction step is proved to preserve the gcd. The rec function will be used in other proofs for iterated subtraction. |
| ⊢ ((A ∈ ℕ ⋀ B ∈ ℕ) → (A < B → gcd(A, B) = gcd(A, (B − A)))) | ||
| 17-Jun-2008 | nndivlub 10381 | A factor of a natural number cannot exceed it. |
| ⊢ ((A ∈ ℕ ⋀ B ∈ ℕ) → ((A / B) ∈ ℕ → B ≤ A)) | ||
| 17-Jun-2008 | nndivsub 10380 | Please add description here. |
| ⊢ (((A ∈ ℕ ⋀ B ∈ ℕ ⋀ C ∈ ℕ) ⋀ ((A / C) ∈ ℕ ⋀ A < B)) → ((B / C) ∈ ℕ ↔ ((B − A) / C) ∈ ℕ)) | ||
| 17-Jun-2008 | nnssi3 10379 | Convert a theorem for real/complex numbers into one for natural numbers. |
| ⊢ ℕ ⊆ D & ⊢ (C ∈ ℕ → φ) & ⊢ (((A ∈ D ⋀ B ∈ D ⋀ C ∈ D) ⋀ φ) → ψ) ⇒ ⊢ ((A ∈ ℕ ⋀ B ∈ ℕ ⋀ C ∈ ℕ) → ψ) | ||
| 17-Jun-2008 | nnssi2 10378 | Convert a theorem for real/complex numbers into one for natural numbers. |
| ⊢ ℕ ⊆ D & ⊢ (B ∈ ℕ → φ) & ⊢ ((A ∈ D ⋀ B ∈ D ⋀ φ) → ψ) ⇒ ⊢ ((A ∈ ℕ ⋀ B ∈ ℕ) → ψ) | ||
| 17-Jun-2008 | gelsupvalOLD 10377 | The greatest element of a set is the supremum. Note that the converse is not true. The supremum might not be an element of the set considered. OBSOLETE - Use supmax 4572 instead. |
| ⊢ R Or A ⇒ ⊢ ((C ∈ B ⋀ (C ∈ A ⋀ ∀y ∈ B ¬ CRy)) → sup(B, A, R) = C) | ||
| 17-Jun-2008 | gelcomplOLD 10376 | A set that contains a greatest element satisfies the antecedent in supremum theorems. This allows sup(A, B, R) to be used in some situations without the completeness axiom. OBSOLETE - Use supmaxlem 4571 instead. |
| ⊢ ((x ∈ A ⋀ (∀z ∈ B ¬ xRz ⋀ x ∈ B)) → ∃x ∈ A (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) | ||
| 17-Jun-2008 | axhvdistr1 8816 | Derive axiom ax-hvdistr1 8834 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩ & ⊢ U ∈ CHil ⇒ ⊢ ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → (A ·h (B +h C)) = ((A ·h B) +h (A ·h C))) | ||
| 16-Jun-2008 | cldlp 7711 | A subset of a topological space is closed iff it contains all its limit points. Corollary 6.7 of [Munkres] p. 97. |
| ⊢ X = ∪J ⇒ ⊢ ((J ∈ Top ⋀ S ⊆ X) → (S ∈ (Clsd ‘J) ↔ ((limPt ‘J) ‘S) ⊆ S)) | ||
| 15-Jun-2008 | ntr0 7671 | The interior of the empty set. |
| ⊢ (J ∈ Top → ((int ‘J) ‘∅) = ∅) | ||
| 15-Jun-2008 | dvelimALT 1352 | Version of dvelim 1351 that doesn't use ax-10 965. (See dvelimfALT 1152 for a version that doesn't use ax-11 966.) |
| ⊢ (φ → ∀xφ) & ⊢ (z = y → (φ ↔ ψ)) ⇒ ⊢ (¬ ∀x x = y → (ψ → ∀xψ)) | ||
| 14-Jun-2008 | axhvmulass 8815 | Derive axiom ax-hvmulass 8833 from Hilbert space under ZF set theory. |
| ⊢ U = ⟨⟨ +h , ·h ⟩ | ||