English
The Euclidean half-space is locally path-connected (for NeZero n).
Русский
Полупространство Евклида локально путь-соединённое.
LaTeX
$$$\\forall n\\in\\mathbb{N},\\ [\\mathrm{NeZero}\\ n] \\Rightarrow \\mathrm{LocPathConnectedSpace}(\\mathrm{EuclideanHalfSpace}(n))$$$
Lean4
/-- Definition of the model with corners `(EuclideanSpace ℝ (Fin n), EuclideanQuadrant n)`, used as a
model for manifolds with corners -/
def modelWithCornersEuclideanQuadrant (n : ℕ) : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanQuadrant n)
where
toFun := Subtype.val
invFun x := ⟨fun i => max (x i) 0, fun i => by simp only [le_refl, or_true, le_max_iff]⟩
source := univ
target := {x | ∀ i, 0 ≤ x i}
map_source' x _ := x.property
map_target' _ _ := mem_univ _
left_inv' x _ := by ext i; simp only [x.2 i, max_eq_left]
right_inv' x hx := by ext1 i; simp only [hx i, max_eq_left]
source_eq := rfl
convex_range' := by
simp only [instIsRCLikeNormedField, ↓reduceDIte]
apply Convex.convex_isRCLikeNormedField
rw [range_euclideanQuadrant]
exact EuclideanQuadrant.convex
nonempty_interior' := by
rw [range_euclideanQuadrant, interior_euclideanQuadrant]
exact ⟨fun i ↦ 1, by simp⟩
continuous_toFun := continuous_subtype_val
continuous_invFun :=
Continuous.subtype_mk (continuous_pi fun i => (continuous_id.max continuous_const).comp (continuous_apply i)) _
