modelWithCornersSelf_boundaryless

English

The trivial model with corners has no boundary.

Русский

Тривиальная модель с углами не имеет границы.

LaTeX

$$$\partial\text{(modelWithCornersSelf)} = \emptyset$$$

Lean4

/-- The trivial model with corners has no boundary -/
instance modelWithCornersSelf_boundaryless (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] : (modelWithCornersSelf 𝕜 E).Boundaryless :=
  ⟨by simp⟩

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