stdSimplex_of_subsingleton — Mathlib

English

If the index set ι is nonempty and subsingleton and the ground ring 𝕜 is subsingleton, then stdSimplex 𝕜 ι equals the singleton consisting of the constant-1 function.

Русский

Если ι непусто и является подсинглетоном, а 𝕜 — подсинглетон, тогда stdSimplex 𝕜 ι состоит из единственной функции, отвечающей f ≡ 1.

LaTeX

$$$\mathrm{stdSimplex}_{\mathbb{k}}(\iota) = \{ f: \iota \to \mathbb{k} \mid f \equiv 1 \}$$$

Lean4

@[nontriviality]
theorem stdSimplex_of_subsingleton [Subsingleton 𝕜] : stdSimplex 𝕜 ι = univ :=
  eq_univ_of_forall fun _ ↦ ⟨fun _ ↦ (Subsingleton.elim _ _).le, Subsingleton.elim _ _⟩

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