ker_apply_mk_out

Mathlib.Data.Setoid.Basic

URI: https://scilib.ai/kg/mathlib#Setoid.ker_apply_mk_out

English

For any a ∈ α, f applied to the quotient representative mk'' a, then out equals f(a).

Русский

Для любого a: f(Quotient.mk'' a).out = f(a).

LaTeX

$$$ f(\langle a \rangle)^{\mathrm{out}} = f(a) $$$

Lean4

theorem ker_apply_mk_out {f : α → β} (a : α) : f (⟦a⟧ : Quotient (Setoid.ker f)).out = f a :=
  @Quotient.mk_out _ (Setoid.ker f) a

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

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

Разделы

Аффилиация

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