English
The range of the corner-model map 𝓡∂ n is { y | y_0 ≥ 0 }.
Русский
Образ отображения модели с углами 𝓡∂ n равен { y | y_0 ≥ 0 }.
LaTeX
$$$\\mathrm{range}(\\mathcal{R}\\partial_n) = \\{ y : y_0 \\ge 0 \\}$$$
Lean4
/-- Definition of the model with corners `(EuclideanSpace ℝ (Fin n), EuclideanHalfSpace n)`, used as
a model for manifolds with boundary. In the scope `Manifold`, use the shortcut `𝓡∂ n`.
-/
def modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] :
ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n)
where
toFun := Subtype.val
invFun x := ⟨update x 0 (max (x 0) 0), by simp⟩
source := univ
target := {x | 0 ≤ x 0}
map_source' x _ := x.property
map_target' _ _ := mem_univ _
left_inv' := fun ⟨xval, xprop⟩ _ => by
rw [Subtype.mk_eq_mk, update_eq_iff]
exact ⟨max_eq_left xprop, fun i _ => rfl⟩
right_inv' _ hx := update_eq_iff.2 ⟨max_eq_left hx, fun _ _ => rfl⟩
source_eq := rfl
convex_range' := by
simp only [instIsRCLikeNormedField, ↓reduceDIte]
apply Convex.convex_isRCLikeNormedField
rw [range_euclideanHalfSpace n]
exact EuclideanHalfSpace.convex (n := n)
nonempty_interior' := by
rw [range_euclideanHalfSpace, interior_halfSpace]
refine ⟨fun i ↦ 1, by simp⟩
continuous_toFun := continuous_subtype_val
continuous_invFun := by exact (continuous_id.update 0 <| (continuous_apply 0).max continuous_const).subtype_mk _
