English
If two boolean-valued sequences f and g on natural numbers agree at a given index n, then the auxiliary Cantor function evaluated at n yields the same value for f and g (for any fixed real parameter c).
Русский
Если две булевы последовательности f и g на множествах натуральных чисел совпадают в позиции n, то соответствующая функция Кантора, применённая к f и g в позиции n, даёт одинаковый результат (при фиксированном вещественном параметре c).
LaTeX
$$$\\forall c \\in \\mathbb{R},\\; \\forall f,g:\\\\mathbb{N} \\to \\{0,1\\},\\; \\forall n \\in \\mathbb{N},\\; f(n)=g(n)\\Rightarrow \\operatorname{cantorFunctionAux}(c,f,n)=\\operatorname{cantorFunctionAux}(c,g,n).$$$
Lean4
theorem cantorFunctionAux_eq (h : f n = g n) : cantorFunctionAux c f n = cantorFunctionAux c g n := by
simp [cantorFunctionAux, h]
