append1Cases — Mathlib

English

append1Cases provides a way to reduce a property on TypeVec (n+1) to a property on append1 α β: if C holds for all append1 α β, then it holds for every γ.

Русский

append1Cases позволяет сводить свойство на TypeVec (n+1) к свойству на append1 α β: если C выполняется для всех append1 α β, тогда C выполняется для каждого γ.

LaTeX

$$∃ C : TypeVec (n + 1) → Sort u, (∀ α β, C (append1 α β)) → ∀ γ, C γ$$

Lean4

/-- cases on `(n+1)-length` vectors -/
@[elab_as_elim]
def append1Cases {C : TypeVec (n + 1) → Sort u} (H : ∀ α β, C (append1 α β)) (γ) : C γ := by
  rw [← @append1_drop_last _ γ]; apply H

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