lift_def — Mathlib

English

The lift construction is the universal map from RingQuot r to T with the property that it sends the class of x to f x.

Русский

Конструкция lift — это универсальное отображение RingQuot r → T, которое переводит эквивалентный класс x в значение f x.

LaTeX

$$$\\operatorname{lift}(\langle f, w\\rangle) \\;:\\; \\operatorname{RingQuot} r \\to\\+* T\\text{ satisfies } \\operatorname{lift}(\\langle f, w\\rangle) (mkRingHom r\\ x) = f\\ x$$$

Lean4

theorem lift_def : eta_helper Eq✝ @lift.{} @(delta% @definition✝) :=
  by
  intros
  delta lift
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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