projIcc_surjective

Mathlib.Order.Interval.Set.ProjIcc

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

English

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

Русский

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

LaTeX

$$$\mathrm{Surjective}(\mathrm{projIcc}(a,b,h))$$$

Lean4

theorem projIcc_surjective : Surjective (projIcc a b h) := fun x => ⟨x, projIcc_val h x⟩

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

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

Разделы

Аффилиация

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