Icc_chartedSpaceChartAt_of_top_le

Mathlib.Geometry.Manifold.Instances.Real

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

← MathLib Explorer

English

If z.val < y, then chartAt (EuclideanHalfSpace 1) z equals 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_top_le {z : Set.Icc x y} (h : y ≤ z.val) : chartAt _ z = IccRightChart x y := by
  simp [Icc_chartedSpaceChartAt, reduceIte, not_lt.mpr h]

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

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

Разделы

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

Аффилиация

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