quotient_liftOn_mk

Mathlib.GroupTheory.Coset.Defs

URI: https://scilib.ai/kg/mathlib#QuotientGroup.quotient_liftOn_mk

English

If f is a function on α that is compatible with the quotient relation, then Quotient.liftOn' (QuotientGroup.mk x) f h = f x.

Русский

Если функция f согласована с эквивалентностью, то Quotient.liftOn' (mk x) f h = f x.

LaTeX

$$QuotientGroup.quotient_liftOn_mk$$

Lean4

@[to_additive (attr := simp)]
theorem quotient_liftOn_mk {β} (f : α → β) (h) (x : α) : Quotient.liftOn' (x : α ⧸ s) f h = f x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru