ih1_neg_left

Mathlib.SetTheory.Surreal.Multiplication

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

English

If IH1 holds for x and y, then IH1 also 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_left : IH1 x y → IH1 (-x) y := fun h x₁ x₂ y' h₁ h₂ hy ↦
  by
  rw [isOption_neg] at h₁ h₂
  exact P24_neg_left.2 (h h₂ h₁ hy)

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

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

Разделы

Аффилиация

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