instIsManifoldIcc — Mathlib

English

For any z in Icc x y with z.val < y, chartAt equals IccLeftChart x y.

Русский

Для любого z ∈ Icc x y с z.val < y график chartAt совпадает с IccLeftChart x y.

LaTeX

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

Lean4

/-- The manifold structure on `[x, y]` is smooth. -/
instance instIsManifoldIcc (x y : ℝ) [Fact (x < y)] {n : WithTop ℕ∞} : IsManifold (𝓡∂ 1) n (Icc x y) :=
  by
  have M : ContDiff ℝ n (show EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) from fun z i => -z i + (y - x)) :=
    contDiff_id.neg.add contDiff_const
  apply isManifold_of_contDiffOn
  intro e e' he he'
  simp only [atlas] at he he'
  rcases he with (rfl | rfl) <;> rcases he' with (rfl | rfl)
  · -- `e = left chart`, `e' = left chart`
    exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _)).1
  · -- `e = left chart`, `e' = right chart`

    apply M.contDiffOn.congr
    rintro _ ⟨⟨hz₁, hz₂⟩, ⟨⟨z, hz₀⟩, rfl⟩⟩
    simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, update_self, max_eq_left, hz₀,
      lt_sub_iff_add_lt, mfld_simps] at hz₁ hz₂
    rw [min_eq_left hz₁.le, lt_add_iff_pos_left] at hz₂
    ext i
    rw [Subsingleton.elim i 0]
    simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, *, max_eq_left, min_eq_left hz₁.le,
      update_self, mfld_simps]
    abel
  · -- `e = right chart`, `e' = left chart`

    apply M.contDiffOn.congr
    rintro _ ⟨⟨hz₁, hz₂⟩, ⟨z, hz₀⟩, rfl⟩
    simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, max_lt_iff, update_self,
      max_eq_left hz₀, mfld_simps] at hz₁ hz₂
    rw [lt_sub_comm] at hz₁
    ext i
    rw [Subsingleton.elim i 0]
    simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, update_self, max_eq_left, hz₀, hz₁.le,
      mfld_simps]
    abel
  · -- `e = right chart`, `e' = right chart`
    exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _)).1

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