segment_single_subset_stdSimplex — Mathlib

English

The line segment between two canonical basis points lies inside the standard simplex: [Pi.single i 1 -[𝕜] Pi.single j 1] ⊆ stdSimplex 𝕜 ι.

Русский

Линия между двумя каноническими базисными точками находится внутри стандартного симплекса.

LaTeX

$$$\bigl( [\Pi\text{single } i\ 1 -[\mathbb{k}] \Pi\text{single } j\ 1] : \mathrm{Set}(\iota \to \mathbb{k}) \bigr) \subseteq \mathrm{stdSimplex}_{\mathbb{k}}(\iota)$$$

Lean4

/-- The edges are contained in the simplex. -/
theorem segment_single_subset_stdSimplex (i j : ι) :
    ([Pi.single i 1 -[𝕜] Pi.single j 1] : Set (ι → 𝕜)) ⊆ stdSimplex 𝕜 ι :=
  (convex_stdSimplex 𝕜 ι).segment_subset (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)

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