ih₂₁ — Mathlib

English

IH2-1 provides the swapped-indices version of IH1, aligning the two halves of the 24-argument inductive structure.

Русский

IH2-1 задаёт зеркальную версию IH1 для перестановки индексов, согласуя две половины 24-аргументной структуры индукции.

LaTeX

$$$IH2\\!\\!1\\ x_1 x_2 y := IH1\\!\\! x_2 x_1 y$$$

Lean4

theorem ih₂₁ (ih' : ∀ a, ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH24 x₂ x₁ y :=
  ih₁₂ <| by
    simp_rw [ArgsRel, InvImage, Args.toMultiset, Multiset.pair_comm] at ih' ⊢
    suffices { x₁, y, x₂ } = { x₂, y, x₁ } by rwa [← this]
    dsimp only [Multiset.insert_eq_cons, ← Multiset.singleton_add] at ih' ⊢
    abel

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