projIci_surjOn

Mathlib.Order.Interval.Set.ProjIcc

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

English

The map projIci(a) is surjective from Ici(a) onto the ambient space.

Русский

Карта projIci(a) сюръективна с области Ici(a) на всю вселенную.

LaTeX

$$$\mathrm{SurjOn}(\mathrm{projIci}(a), \mathrm{Ici}(a), \mathrm{univ})$$$

Lean4

theorem projIci_surjOn : SurjOn (projIci a) (Ici a) univ := fun x _ => ⟨x, x.2, projIci_coe x⟩

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

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

Разделы

Аффилиация

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