lift_coe — Mathlib

English

The quotient lift of f along h evaluated at the coe of x is f(x) when x is a list.

Русский

Подъем по активной эквивалентности через h для x, представляющего список, равен f(x).

LaTeX

$$$$Quotient.lift f h (x : Multiset\ α) = f x$$$$

Lean4

@[simp]
theorem lift_coe {α β : Type*} (x : List α) (f : List α → β) (h : ∀ a b : List α, a ≈ b → f a = f b) :
    Quotient.lift f h (x : Multiset α) = f x :=
  Quotient.lift_mk _ _ _

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