stdSimplex_of_isEmpty_index — Mathlib

English

If the index set ι is empty, then stdSimplex 𝕜 ι is empty.

Русский

Если множество индексов ι пусто, то стандартный симплекс пуст.

LaTeX

$$$\mathrm{stdSimplex}_{\mathbb{k}}(\iota) = \varnothing$$$

Lean4

/-- The standard simplex in the zero-dimensional space is empty. -/
theorem stdSimplex_of_isEmpty_index [IsEmpty ι] [Nontrivial 𝕜] : stdSimplex 𝕜 ι = ∅ :=
  eq_empty_of_forall_notMem <| by rintro f ⟨-, hf⟩; simp at hf

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