English
The manifold structure on the interval Icc x y is smooth, i.e., there exists a smooth atlas coming from the model with corners.
Русский
Манifold-структура на интервале Icc x y гладкая, то есть существует гладкий атлас, порождаемый моделью с углами.
LaTeX
$$IsManifold( modelWithCornersEuclideanHalfSpace 1, Set.Icc x y ).Elem$$
Lean4
theorem boundary_Icc : (𝓡∂ 1).boundary (Icc x y) = {⊥, ⊤} :=
by
ext p
rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc p.2 with (hp | hp | hp)
· have : p = ⊥ := SetCoe.ext hp
rw [this]
apply iff_of_true Icc_isBoundaryPoint_bot (mem_insert ⊥ {⊤})
· have : p = ⊤ := SetCoe.ext hp
rw [this]
apply iff_of_true Icc_isBoundaryPoint_top (mem_insert_of_mem ⊥ rfl)
· apply iff_of_false
· simpa [← mem_compl_iff, ModelWithCorners.compl_boundary] using Icc_isInteriorPoint_interior hp
· rw [mem_insert_iff, mem_singleton_iff]
push_neg
constructor <;> by_contra h <;> rw [congrArg Subtype.val h] at hp
exacts [left_mem_Ioo.mp hp, right_mem_Ioo.mp hp]
