liftOnWellOrder_type — Mathlib

English

A special case of lifting on well-orders: the lift of typeLT γ with data f and coherence c equals f applied to γ.

Русский

Особый случай подъёма по хорошо упорядоченным типам: подъем типа LT γ равен значению f(γ).

LaTeX

$$$\mathrm{liftOnWellOrder}(\operatorname{typeLT}\gamma)\; f\; c = f(\gamma).$$$

Lean4

@[simp]
theorem liftOnWellOrder_type {δ : Sort v} (f : ∀ (α) [LinearOrder α] [WellFoundedLT α], δ)
    (c : ∀ (α) [LinearOrder α] [WellFoundedLT α] (β) [LinearOrder β] [WellFoundedLT β], typeLT α = typeLT β → f α = f β)
    {γ} [LinearOrder γ] [WellFoundedLT γ] : liftOnWellOrder (typeLT γ) f c = f γ :=
  by
  change Quotient.liftOn' ⟦_⟧ _ _ = _
  rw [Quotient.liftOn'_mk]
  congr
  exact LinearOrder.ext_lt fun _ _ ↦ Iff.rfl

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