cast_type — Mathlib

English

Cast type compatibility: converting the index with an equality ds₁ = ds₂ preserves the value component.

Русский

Совместимость типов при преобразовании типа индекса: равенство ds₁ = ds₂ сохраняет значение.

LaTeX

$$cast_type (is : List ℕ) (eq : ds₁ = ds₂) (h : Forall₂ (· < ·) is ds₁) : (cast (congr_arg HolorIndex eq) ⟨is, h⟩).val = is$$

Lean4

theorem cast_type (is : List ℕ) (eq : ds₁ = ds₂) (h : Forall₂ (· < ·) is ds₁) :
    (cast (congr_arg HolorIndex eq) ⟨is, h⟩).val = is := by subst eq; rfl

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