projIci_surjective

Mathlib.Order.Interval.Set.ProjIcc

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

English

Surjectivity of projIci: every element of the ambient space is attained as projIci(a) of some input.

Русский

Сюръективность projIci: каждый элемент пространства является образом некоторого элемента.

LaTeX

$$$\mathrm{Surjective}(\mathrm{projIci}(a))$$$

Lean4

theorem projIci_surjective : Surjective (projIci a) := fun x => ⟨x, projIci_coe x⟩

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

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

Разделы

Аффилиация

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