insertNthOrderIso_last — Mathlib

English

Equality between insertNthOrderIso and snocOrderIso at the last position.

Русский

Равенство между insertNthOrderIso и snocOrderIso в позиции last.

LaTeX

$$$\operatorname{insertNthOrderIso}(\_, \text{last } n) = \operatorname{snocOrderIso}(\_)$$$

Lean4

/-- Note this lemma can only be written about non-dependent tuples as `insertNth (last n) = snoc` is
not a definitional equality. -/
@[simp]
theorem insertNthOrderIso_last (n : ℕ) (α : Type*) [LE α] :
    insertNthOrderIso (fun _ ↦ α) (last n) = snocOrderIso (fun _ ↦ α) := by ext; simp

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