codRestrict_range_surjective

Mathlib.Data.Set.Restrict

URI: https://scilib.ai/kg/mathlib#Set.codRestrict_range_surjective

← MathLib Explorer

English

The codRestrict map from a restricted range is surjective onto its target.

Русский

Код Restrict отображает всё на целевой тип.

LaTeX

$$$(codRestrict f (range f) mem_range_self)\\;$.Surjective$$

Lean4

theorem codRestrict_range_surjective (f : ι → α) : ((range f).codRestrict f mem_range_self).Surjective :=
  by
  rintro ⟨b, ⟨a, rfl⟩⟩
  exact ⟨a, rfl⟩

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

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

Разделы

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

Аффилиация

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