English
There exists a charted space structure on the set Icc x y given by two charts, IccLeftChart and IccRightChart; the chart at a point z is left if z < y and right otherwise.
Русский
Существует структура чарта на множестве Icc x y задаваемая двумя чартами IccLeftChart и IccRightChart; для точки z чарт равен левому, если z < y, и правому — иначе.
LaTeX
$$$\text{chartAt}(z) = \begin{cases} IccLeftChart(x,y), & z.\mathrm{val} < y \\ IccRightChart(x,y), & \text{else} \end{cases}$$$
Lean4
/-- Charted space structure on `[x, y]`, using only two charts taking values in
`EuclideanHalfSpace 1`.
-/
instance instIccChartedSpace (x y : ℝ) [h : Fact (x < y)] : ChartedSpace (EuclideanHalfSpace 1) (Icc x y)
where
atlas := {IccLeftChart x y, IccRightChart x y}
chartAt z := if z.val < y then IccLeftChart x y else IccRightChart x y
mem_chart_source
z := by
by_cases h' : z.val < y
· simp only [h', if_true]
exact h'
· simp only [h', if_false]
apply lt_of_lt_of_le h.out
simpa only [not_lt] using h'
chart_mem_atlas z := by by_cases h' : (z : ℝ) < y <;> simp [h']
