# Is a function needed here?

This question is related to my question Can we choose an element from a class?. However, I decided to create a separate question.

Let $$H$$ be a complex Hilbert space and $$H_1,\dotsc,H_n$$ be closed subspaces of $$H$$. Set $$H_0\mathrel{:=}H_1\cap H_2\cap\dotsb\cap H_n$$ and let $$P_i$$ be the orthogonal projection onto $$H_i$$, $$i=0,1,2,\dotsc,n$$. I study the functions $$f_n:[0,1]\to\mathbb{R}$$ defined by $$f_n(c)=\sup\{\lVert P_n\dotsm P_2 P_1-P_0\rVert \mathrel| c_F(H_1,\dotsc,H_n)\leqslant c\},\,c\in[0,1],$$ where the supremum is taken over all complex Hilbert spaces $$H$$ and systems of closed subspaces $$H_1,\dotsc,H_n$$ of $$H$$ for which the Friedrichs number $$c_F(H_1,\dotsc,H_n)$$ is less than or equal to $$c$$ (the Friedrichs number is a certain numerical characteristic of a system of subspaces). Note that all such systems of subspaces do not form a set. Despite this, the function $$f_n$$ is well-defined (see my Question Can we take a supremum over all Hilbert spaces?). Indeed, let $$A_{n}(c)$$ be the set of all $$a\in\mathbb{R}$$ for which there exist a complex Hilbert space $$H$$ and a system of closed subspaces $$H_1,\dotsc,H_n$$ of $$H$$ such that $$c_F(H_1,\dotsc,H_n)\leqslant c$$ and $$\lVert P_n\dotsm P_2 P_1-P_0\rVert=a$$. Then by the axiom (scheme) of separation $$A_{n}(c)$$ is a set and thus we can take its supremum.

I need to show that $$f_n(c)\leqslant g_n(c)$$ for some function $$g_n$$. I argue as follows. Consider arbitrary element $$a\in A_{n}(c)$$. Then there exist a complex Hilbert space $$H$$ and a system of closed subspaces $$H_1,\dotsc,H_n$$ of $$H$$ such that $$c_F(H_1,\dotsc,H_n)\leqslant c$$ and $$\lVert P_n\dotsm P_2 P_1-P_0\rVert=a$$. After this I work with this system of subspaces $$(H;H_1,\dotsc,H_n)$$ and show that $$\|P_n\dotsm P_2 P_1-P_0\|\leqslant g_n(c)$$. Thus $$a\leqslant g_n(c)$$. Since this inequality holds for every $$a\in A_{n}(c)$$, we conclude that $$\sup A_{n}(c)\leqslant g_n(c)$$, i.e., $$f_n(c)\leqslant g_n(c)$$.

Questions. Are all these arguments correct, say, in the axiomatic theory ZFC? Essentially, the core of my worries is the following. Unfortunately, I do not understand if the function $$A_n(c)\ni a\mapsto (H;H_1,...,H_n)$$ such that $$c_F(H_1,\dotsc,H_n)\leqslant c$$ and $$\lVert P_n\dotsm P_2 P_1-P_0\rVert=a$$, is needed in the arguments above or not. If a function is needed here, it turns out that the "Axiom of Choice for classes" is needed here, and I do not know what to do with this. On the one hand, it seems that the function is not needed here. On the other hand, we choose a system of subspaces for each $$a\in A_n(c)$$; the set $$A_n(c)$$ can be infinite and we need to consider all $$a\in A_n(c)$$. Therefore, perhaps, a function is needed here. Explain to me, please, whether a function is needed here or not?

• As in all your questions, you do not need the axiom of choice to choose one element from a non-empty class; that's what non-empty means. You only need AC to make many choices simultaneously. See, for example, mathoverflow.net/questions/387353/… . Apr 7 at 21:47
• Also, a TeX note: please do not use repeated periods to simulate dots; that's what the various \dots commands are for. Compare the spacing in $H_1 \cap H_2 \cap \dotsb \cap H_n$ H_1 \cap H_2 \cap \dotsb \cap H_n to that in $H_1 \cap H_2 \cap ... \cap H_n$ H_1 \cap H_2 \cap ... \cap H_n. I have edited accordingly. Apr 7 at 21:53
• The answers are as follows: these arguments are correct, the indicated function is not needed. Indeed, your argument might as well prove that for all H1,…,Hn, H such that c_F(H1,…,Hn)⩽c, you have ∥Pn⋯P2P1−P0∥⩽g_n(c). Quantifying over a collection of sets is perfectly legitimate even if this collection of sets forms a proper class. There is no need to mention A_n(c) at all, it only creates further confusion. Apr 7 at 22:57
• @DmitriPavlov Would you mind posting your comment as an answer to close out the question? Apr 8 at 0:25

Indeed, your argument might as well prove that for all $$H_1,\dotsc,H_n$$, and $$H$$ such that $$c_F(H_1,\dotsc,H_n)\le c$$, you have $$\lVert P_n\dotsm P_2P_1−P_0\rVert \le g_n(c)$$. Quantifying over a collection of sets is perfectly legitimate even if this collection of sets forms a proper class. There is no need to mention the set $$A_n(c)$$ at all, it only creates further confusion.
• Dear Dmitri, thank you for your answer. One thing is confusing for me. Assume that my arguments (proof of $f_n(c)\leqslant g_n(c)$) are correct. Then by "similar" arguments I can prove the Axiom of Choice. The "proof" is as follows. Let $A_i, i\in I$ be a set of mutually disjoint nonempty sets. We will construct a set that contains exactly one element in common with each of the sets as follows. Consider arbitrary $i\in I$ and fix it. Since the set $A_i$ is nonempty, $\exists x$ such that $x\in A_i$. To be continued. Apr 9 at 21:29
• Now we use the existential instantiation and write $x(i)$ for a new symbol (just a symbol) such that $x(i)\in A_i$. Consider one-element sets $\{x(i)\}$ and let $A=\bigcup_{i\in I}\{x(i)\}$. Then $A$ is a set and $A$ contains exactly one element in common with each $A_j$. Where am I wrong? Apr 9 at 21:37
• @IvanFeshchenko You go wrong as soon as you define $A$: intuitively this requires you to "unfix" your chosen element $i$. You'll see this if you sit down and try to write out your argument as a formal proof (say, in sequent calculus). Basically you have a first existential instantiation picking an $i$ and following that a second existential instantiation picking an $x$, but there isn't a logical rule letting you somehow "uniformize" this. (In fact you can think of $\mathsf{AC}$ as an additional logical rule in a precise, if technical, sense.) Apr 9 at 22:12