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