single_apply_of_ne

Mathlib.Data.PEquiv

URI: https://scilib.ai/kg/mathlib#PEquiv.single_apply_of_ne

English

If a1 ≠ a2, then the single a1 b applied to a2 yields none.

Русский

Если a1 ≠ a2, то применённая к a2 функция single возвращает none.

LaTeX

$$single a_1 b a_2 = None \quad \text{if } a_1 \neq a_2$$

Lean4

theorem single_apply_of_ne {a₁ a₂ : α} (h : a₁ ≠ a₂) (b : β) : single a₁ b a₂ = none :=
  if_neg h.symm

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

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

Разделы

Аффилиация

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