ih24_neg — Mathlib

English

IH24 is symmetric with respect to negation: IH24 x1 x2 y implies IH24 (-x2) (-x1) y and IH24 x1 x2 (-y).

Русский

IH24 симметрично относительно отрицания: IH24 x1 x2 y следует IH24 (-x2) (-x1) y и IH24 x1 x2 (-y).

LaTeX

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

Lean4

/-- Symmetry properties of `IH24`. -/
theorem ih24_neg : IH24 x₁ x₂ y → IH24 (-x₂) (-x₁) y ∧ IH24 x₁ x₂ (-y) :=
  by
  simp_rw [IH24, ← P24_neg_right, isOption_neg]
  refine fun h ↦ ⟨fun z ↦ ⟨?_, ?_, ?_⟩, fun z ↦ ⟨(@h z).1, (@h z).2.1, P24_neg_right.2 ∘ (@h <| -z).2.2⟩⟩
  all_goals
    rw [P24_neg_left]
    simp only [neg_neg]
    first
    | exact (@h <| -z).2.1
    | exact (@h <| -z).1
    | exact (@h z).2.2

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