quot_lift_mk — Mathlib

English

For any β and f with the necessary step-respecting property, Quot.lift f H (mk L) = f L.

Русский

Для любых β и f с требуемым условием совместимости шагов, Quot.lift f H (mk L) = f L.

LaTeX

$$$\forall {\beta}, \forall f:\, \mathsf{List}(\alpha \times \mathsf{Bool}) \to \beta,\ \forall H,\ (\dots) \ \Rightarrow \mathrm{Quot.lift} f H (\mathrm{mk}(L)) = f(L).$$$

Lean4

@[to_additive (attr := simp)]
theorem quot_lift_mk (β : Type v) (f : List (α × Bool) → β) (H : ∀ L₁ L₂, Red.Step L₁ L₂ → f L₁ = f L₂) :
    Quot.lift f H (mk L) = f L :=
  rfl

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