Icc_chartedSpaceChartAt — Mathlib

English

For any z in Set.Icc x y, the chartAt is equal to IccLeftChart x y if z.val < y, and to IccRightChart x y otherwise.

Русский

Для любого z ∈ Set.Icc x y отображение chartAt равно IccLeftChart x y, если z.val < y, и IccRightChart x y иначе.

LaTeX

$$$chartAt\left(EuclideanHalfSpace\ 1\right)\; z = \begin{cases} IccLeftChart(x,y), & z.\mathrm{val} < y \\ IccRightChart(x,y), & \text{иначе} \end{cases}$$$

Lean4

@[simp]
theorem Icc_chartedSpaceChartAt {z : Set.Icc x y} :
    chartAt _ z = if z.val < y then IccLeftChart x y else IccRightChart x y :=
  rfl

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