liftOn_mk — Mathlib

English

The value of liftOn on a canonical representative mk m s equals f ⟨m,s⟩.

Русский

Значение liftOn на каноническом представительстве mk m s равно f ⟨m,s⟩.

LaTeX

$$$\\text{LocalizedModule}.liftOn\\, (\\text{mk } m s)\\; f\\; wd = f(\\langle m,s \\rangle).$$$

Lean4

theorem liftOn_mk {α : Type*} {f : M × S → α} (wd : ∀ (p p' : M × S), p ≈ p' → f p = f p') (m : M) (s : S) :
    liftOn (mk m s) f wd = f ⟨m, s⟩ := by convert Quotient.liftOn_mk f wd ⟨m, s⟩

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