Символ «Равно по определению» входит в подраздел «Знаки отношений» раздела «Математические операторы» и
был утвержден как часть Юникода версии 1.1 в 1993 г.
The ≜ indicates that U is being defined to be {Ux:x∈X}: we are not saying that some previously defined U is equal to the collection of these sets Ux.
the triangle-equals looks neater inline, is faster to write by hand, and is language-independent.
I am simply pointing out the difference between U≜{Ux:x∈X} which defines the symbol U, and U={Ux:x∈X} which asserts that some previously defined set U is equal to the set {Ux:,∈X}. In most contexts I would write U={Ux:x∈X} for both of those meanings, but occasionally it is useful to distinguish definitions from statements that two previously defined things are equal
Определение (≜ , равно по определению) вводит новое понятие, которого ранее не было.
Определение это некоторого рода конкретизация аксиомы, хотя аксиома не обязательно вводит новое понятие.
Используя это (и ранее введённые определения и аксиомы) можно доказывать.
Что такое определение? Утверждение.
Само равенство, видимо, задается (определяется) другим утверждением (например, через элементы множеств).
Равносильность (⇔) же показывает, что это определение можно записать и с помощью знака включения.
≣ - строго эквивалентно
≡ - идентично
≢ - не идентично
тождественно
Стрелка вправо — «достаточно». Стрелка влево — «необходимо». Стрелка туды-сюды — «необходимо и достаточно», «равносильно», «одно и то же», «тождественно», «по определению равно»… Обозначение последнего, соответственно, может быть разным.
“по определению равно” и $:=$ - это не просто равносильность. “По определению равно” вводит новый символ.
значки $\Rightarrow$, $\Leftarrow$ и $\Leftrightarrow$ являются символами операций логического вывода (по правилам той логики, которая по умолчанию принята в данном контексте рассуждений)
могут связывать значения только одного типа - булевского, и только одного значения - истина.
Знаки определения $\stackrel{\text{def}}=$ и тождественности $\equiv$ могут связывать любые объекты, отношения и операции любого типа в любой формальной системе, при этом определение подразумевает введение новой конструкции и конструктивное описание ее построения на основе базовых и ранее определенных конструкций данной системы, а тождество всегда (?) требует доказательства.
Вы намешали в одну кучу выводимость, истинность и то, что теория до определения и теория после — две разные (в первой — аксиомы $\mathcal A$, во сторой — $\mathcal A \cup{\mathrm{NewDef}}$).