ih4_neg — Mathlib

English

Symmetry properties of IH4 with respect to negation: IH4 x1 x2 y implies IH4 (-x2) (-x1) y and IH4 x1 x2 (-y).

Русский

Свойства симметрии IH4 относительно отрицания: IH4 x1 x2 y → IH4 (-x2) (-x1) y и IH4 x1 x2 (-y).

LaTeX

$$IH4 x1 x2 y → (IH4 (-x2) (-x1) y ∧ IH4 x1 x2 (-y))$$

Lean4

/-- Symmetry properties of `IH4`. -/
theorem ih4_neg : IH4 x₁ x₂ y → IH4 (-x₂) (-x₁) y ∧ IH4 x₁ x₂ (-y) :=
  by
  simp_rw [IH4, isOption_neg]
  refine fun h ↦ ⟨fun z w h' ↦ ?_, fun z w h' ↦ ?_⟩
  · convert (h h').symm using 2 <;> rw [P2_neg_left, neg_neg]
  · convert h h' using 2 <;> rw [P2_neg_right]

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