Icc_chartedSpaceChartAt_of_le_top

Mathlib.Geometry.Manifold.Instances.Real

URI: https://scilib.ai/kg/mathlib#Icc_chartedSpaceChartAt_of_le_top

← MathLib Explorer

English

If z.val < y, then chartAt (EuclideanHalfSpace 1) z = IccLeftChart x y.

Русский

Если z.val < y, то chartAt (EuclideanHalfSpace 1) z = IccLeftChart x y.

LaTeX

$$If z.\mathrm{val} < y, then chartAt(\text{EuclideanHalfSpace } 1) z = IccLeftChart(x,y).$$

Lean4

theorem Icc_chartedSpaceChartAt_of_le_top {z : Set.Icc x y} (h : z.val < y) : chartAt _ z = IccLeftChart x y := by
  simp [Icc_chartedSpaceChartAt, h]

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

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

Разделы

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

Аффилиация

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