English
For the two-point index set Fin 2, the standard simplex equals the line segment between the two vertex points Pi.single 0 1 and Pi.single 1 1.
Русский
Для множества индексов Fin 2 стандартный симплекс равен отрезку между вершинами Pi.single 0 1 и Pi.single 1 1.
LaTeX
$$$\mathrm{stdSimplex}_{\mathbb{k}}(\mathrm{Fin}\,2) = \mathrm{segment}_{\mathbb{k}}(\mathrm{Pi.single}\ 0\ 1, \mathrm{Pi.single}\ 1\ 1)$$$
Lean4
theorem stdSimplex_fin_two : stdSimplex 𝕜 (Fin 2) = ([Pi.single 0 1 -[𝕜] Pi.single 1 1] : Set (Fin 2 → 𝕜)) :=
by
refine Subset.antisymm ?_ (segment_single_subset_stdSimplex 𝕜 (0 : Fin 2) 1)
rintro f ⟨hf₀, hf₁⟩
rw [Fin.sum_univ_two] at hf₁
refine ⟨f 0, f 1, hf₀ 0, hf₀ 1, hf₁, funext <| Fin.forall_fin_two.2 ?_⟩
simp
