Чему эквивалентна запись A, где B.

[nebachiv]

Чему эквивалентна эта запись?
A, где B.
A$\Rightarrow$B или B$\Rightarrow$A или A$\Leftrightarrow$B ?
Или чему-то другому?

[Someone]

Никогда не встречал такой записи. А можно привести более-менее обширную цитату, где бы это встречалось?

[Mikhail_K]

Обычно в таких конструкциях $B$ просто является разъяснением обозначений, использованных в $A$...

[VAL]

Mikhail_K в сообщении #1253849 писал(а):

Обычно в таких конструкциях $B$ просто является разъяснением обозначений, использованных в $A$...

т.е., по сути, эквивалентна таки $B\Rightarrow A$

[Mysterious Light]

VAL в сообщении #1253854 писал(а):

Mikhail_K в сообщении #1253849 писал(а):

Обычно в таких конструкциях $B$ просто является разъяснением обозначений, использованных в $A$...

т.е., по сути, эквивалентна таки $B\Rightarrow A$

с квантором всеобщности по всем свободным буквам в $B$, не входящим при этом в контекст.

ср.:

Цитата:

Пусть $f: R\to R^2$, $t\in R$
...
$z=x+iy$, где $(x, y) = f(t)$

Цитата:

Пусть $f: R\to R^2$, $t\in R$
...
$\forall x\forall y((x, y) = f(t) \Rightarrow z=x+iy)$

[george66]

Ни тому, ни другому. Подстановке. Допустим "$x^2$, где $x=y+1$" означает $x^2[y+1/x]$ (подстановка $y+1$ вместо $x$ в выражение $x^2$)

[arseniiv]

george66
А как следующее переформулируете?

$C_n = A_n + B_n$, где $A_n = A_{n-1} + B_{n-1}$, $B_n = A_{n-1} - B_{n-1}$, $A_0 = a, B_0 = b$.

(А на самом деле…)

Вообще представляю решение, но интересно, какое предложите.

[Mysterious Light]

george66, разве $x^2$ является суждением? Иначе выражения вроде $A\Rightarrow B$, приведённые ТС, теряют смысл.

arseniiv, пока справа от «где» находится система равенств вида буква=выражение, формализуемо. Если к тому же индексы монотонно убывают, как у Вас, то даже без неподвижной точки можно.

Однажды было обсуждение, которое, однако, не могу найти.
Оно было о выражениях «$F[x]$, где $P[x]$» с буквой $x$ и функциональным и предикатным контекстами $F[]$ и $P[]$, которые записывались через $F[\iota x. P[x]]$.
Насколько я помню, кто-то доказывал, что нельзя дать каноничное определение этой конструкции, не похерив ряд удобных теорем для работы с выражениями и предикатами.
Увы, не могу найти эту тему.

[george66]

arseniiv в сообщении #1254010 писал(а):

george66
А как следующее переформулируете?

$C_n = A_n + B_n$, где $A_n = A_{n-1} + B_{n-1}$, $B_n = A_{n-1} - B_{n-1}$, $A_0 = a, B_0 = b$.

(А на самом деле…)

Вообще представляю решение, но интересно, какое предложите.

$C_n = A(n) + B(n)$, где $A,B=$ две функции, определённые рекурсией (можно записать с помощью оператора рекурсии)

Дело в том, что обычно мы не пишем подстановку явно, поэтому её не замечаем (как воздух). Но, вообще, это вещь не совсем простая.

-- 08.10.2017, 06:06 --

Mysterious Light в сообщении #1254015 писал(а):

george66, разве $x^2$ является суждением? Иначе выражения вроде $A\Rightarrow B$, приведённые ТС, теряют смысл.

Конечно, я и говорю "ни то, ни другое". Подставлять можно терм в формулу или один терм в другой вместо переменной.

-- 08.10.2017, 06:09 --

Хотя, если так "$x^2$, где $x>1$", тогда сложнее.

-- 08.10.2017, 06:39 --

Допустим
$y=x^2$ где $x>1$
означает
$y=x^2\wedge x>1$
или, возможно
$\exists x(y=x^2\wedge x>1)$

[grizzly]

arseniiv в сообщении #1254010 писал(а):

А как следующее переформулируете?

А можно увидеть авторское решение? Просто любопытно, будет ли в нём видно исчезновение $a$ после нескольких первых итераций.

[arseniiv]

Я предполагал сначала переход к функции со значениями-парами $AB_n = \ldots(AB_{n-1}), AB_0 = (a, b)$, потом к её определению в виде $AB = \ldots$, и потом уже как выше.