symmDiff_right_inj

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#symmDiff_right_inj

English

The map x ↦ a Δ x is injective; i.e., equality of outputs implies equal inputs.

Русский

Отображение x ↦ a Δ x инъективно; равенство выходов значит равенство входов.

LaTeX

$$$ \forall x\forall y\, (a \\Delta x = a \\Delta y \\Rightarrow x = y)$$$

Lean4

@[simp]
theorem symmDiff_right_inj : a ∆ b = a ∆ c ↔ b = c :=
  (symmDiff_right_injective _).eq_iff

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru