projIcc_surjOn

Mathlib.Order.Interval.Set.ProjIcc

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

English

The map projIcc(a,b,h) is surjective from Icc(a,b) onto the ambient space.

Русский

Карта projIcc(a,b,h) сюръективна с области Icc(a,b) на всю вселенную.

LaTeX

$$$\mathrm{SurjOn}(\mathrm{projIcc}(a,b,h), \mathrm{Icc}(a,b), \mathrm{univ})$$$

Lean4

theorem projIcc_surjOn : SurjOn (projIcc a b h) (Icc a b) univ := fun x _ => ⟨x, x.2, projIcc_val h x⟩

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

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

Разделы

Аффилиация

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