English
The right chart for the interval is defined as a map from the closed interval [x, y] to the Euclidean half-space with a specified chart; it encodes the right-hand coordinate chart for the boundary.
Русский
Правый график для интервала задаёт отображение из [x, y] в евклидову полуплоскость и задаёт правый координатный чарт для границы.
LaTeX
$$def IccRightChart (x y : Real) [h : Fact (Real.instLT.lt x y)] : OpenPartialHomeomorph (Set.Icc x y) (EuclideanHalfSpace 1)$$
Lean4
/-- The right chart for the topological space `[x, y]`, defined on `(x,y]` and sending `y` to `0` in
`EuclideanHalfSpace 1`.
-/
def IccRightChart (x y : ℝ) [h : Fact (x < y)] : OpenPartialHomeomorph (Icc x y) (EuclideanHalfSpace 1)
where
source := {z : Icc x y | x < z.val}
target := {z : EuclideanHalfSpace 1 | z.val 0 < y - x}
toFun z := ⟨fun _ => y - z.val, sub_nonneg.mpr z.property.2⟩
invFun z := ⟨max (y - z.val 0) x, by simp [z.prop, h.out.le, sub_eq_add_neg]⟩
map_source' := by simp only [imp_self, mem_setOf_eq, sub_lt_sub_iff_left, forall_true_iff]
map_target' := by
simp only [lt_max_iff, mem_setOf_eq]; intro z hz; left
linarith
left_inv' := by
rintro ⟨z, hz⟩ h'z
simp only [mem_setOf_eq, mem_Icc] at hz h'z
simp only [hz, sub_eq_add_neg, max_eq_left, add_add_neg_cancel'_right, neg_add_rev, neg_neg]
right_inv' := by
rintro ⟨z, hz⟩ h'z
rw [Subtype.mk_eq_mk]
funext i
dsimp at hz h'z
have A : x ≤ y - z 0 := by linarith
rw [Subsingleton.elim i 0]
simp only [A, sub_sub_cancel, max_eq_left]
open_source :=
haveI : IsOpen {z : ℝ | x < z} := isOpen_Ioi
this.preimage continuous_subtype_val
open_target := by
have : IsOpen {z : ℝ | z < y - x} := isOpen_Iio
have : IsOpen {z : EuclideanSpace ℝ (Fin 1) | z 0 < y - x} :=
this.preimage (@continuous_apply (Fin 1) (fun _ => ℝ) _ 0)
exact this.preimage continuous_subtype_val
continuousOn_toFun := by
apply Continuous.continuousOn
apply Continuous.subtype_mk
have : Continuous fun (z : ℝ) (_ : Fin 1) => y - z := continuous_const.sub (continuous_pi fun _ => continuous_id)
exact this.comp continuous_subtype_val
continuousOn_invFun := by
apply Continuous.continuousOn
apply Continuous.subtype_mk
have A : Continuous fun z : ℝ => max (y - z) x := (continuous_const.sub continuous_id).max continuous_const
have B : Continuous fun z : EuclideanSpace ℝ (Fin 1) => z 0 := continuous_apply 0
exact (A.comp B).comp continuous_subtype_val
