Символ «Равно по определению» входит в подраздел «Знаки отношений» раздела «Математические операторы» и
был утвержден как часть Юникода версии 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
Определение (≜ , равно по определению) вводит новое понятие, которого ранее не было.
Определение это некоторого рода конкретизация аксиомы, хотя аксиома не обязательно вводит новое понятие.
Используя это (и ранее введённые определения и аксиомы) можно доказывать.
Что такое определение? Утверждение.
Само равенство, видимо, задается (определяется) другим утверждением (например, через элементы множеств).
Равносильность (⇔) же показывает, что это определение можно записать и с помощью знака включения.


:=
А что если двоеточие тут означает изменение контекста? Или что-то с контекстами связанное? Хорошо бы было двоеточие над знаком равно разместить, а не левее.
I was referring to when ≜ is used to mean “is equal, by a previously made definition”, just like one would write =(23) meaning that “is equal, by virtue of formula (23)”. Such usage of ≜ is a reference to a previously made definition and would be a verbatim copy of it or a very trivial specialisation, e.g. UX:={Ux:x∈X} and then UY≜{Ux:x∈Y}, where ≜ is to emphasise that the equality is a trivial consequence of a definition and that no new definition has been made.
It is the eject button.