English
If ZeroLEOneClass 𝕜 holds and ι is nonempty and subsingleton, then stdSimplex 𝕜 ι is the singleton consisting of the constant-1 function.
Русский
Если выполняются условия ZeroLEOneClass 𝕜 и ι некратно непусто и является подсинглетоном, то stdSimplex 𝕜 ι — единичный элемент, соответствующий f ≡ 1.
LaTeX
$$$\mathrm{stdSimplex}_{\mathbb{k}}(\iota) = \{ f: \iota \to \mathbb{k} \mid f \equiv 1 \}$$$
Lean4
theorem stdSimplex_unique [ZeroLEOneClass 𝕜] [Nonempty ι] [Subsingleton ι] : stdSimplex 𝕜 ι = {fun _ ↦ 1} :=
by
cases nonempty_unique ι
refine eq_singleton_iff_unique_mem.2 ⟨⟨fun _ ↦ zero_le_one, Fintype.sum_unique _⟩, ?_⟩
rintro f ⟨-, hf⟩
rw [Fintype.sum_unique] at hf
exact funext (Unique.forall_iff.2 hf)
