surjective

Mathlib.RingTheory.WittVector.Basic

URI: https://scilib.ai/kg/mathlib#WittVector.mapFun.surjective

← MathLib Explorer

English

The mapFun preserves zero: mapFun f (0) = 0.

Русский

Отображение mapFun сохраняет ноль: mapFun f (0) = 0.

LaTeX

$$$\\mathrm{WittVector.mapFun}\\, f\\, 0 = 0$$$

Lean4

theorem surjective (f : α → β) (hf : Surjective f) : Surjective (mapFun f : 𝕎 α → 𝕎 β) := fun x =>
  ⟨mk _ fun n => Classical.choose <| hf <| x.coeff n, by ext n;
    simp only [mapFun, coeff_mk, comp_apply, Classical.choose_spec (hf (x.coeff n))]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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