ih1_neg_right

Mathlib.SetTheory.Surreal.Multiplication

URI: https://scilib.ai/kg/mathlib#Surreal.Multiplication.ih1_neg_right

English

If IH1 holds for x and y, then IH1 holds for x and -y.

Русский

Если IH1 справедливо для x и y, то IH1 справедливо для x и -y.

LaTeX

$$$\forall x\forall y\ (IH1(x,y) \rightarrow IH1(x,-y))$$$

Lean4

theorem ih1_neg_right : IH1 x y → IH1 x (-y) := fun h x₁ x₂ y' ↦
  by
  rw [← neg_eq_iff_eq_neg, isOption_neg, P24_neg_right]
  apply h

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

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

Разделы

Аффилиация

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