English
The one-dimensional standard simplex in 𝕜 with Fin 2 is equivalent to the closed unit interval Icc(0,1), via a natural order-preserving bijection sending the first vertex to 0 and the second to 1.
Русский
Одномерный стандартный симплекс в 𝕜 на Fin 2 эквивалентен замкнутому отрезку Icc(0,1) посредством естественного упорядоченного биекция, отправляющей первую вершину в 0, вторую — в 1.
LaTeX
$$$\mathrm{stdSimplex}_{\mathbb{k}}(\mathrm{Fin}\,2) \cong Icc(0,1)$$$
Lean4
/-- The standard one-dimensional simplex in `Fin 2 → 𝕜` is equivalent to the unit interval.
This bijection sends the zeroth vertex `Pi.single 0 1` to `0` and
the first vertex `Pi.single 1 1` to `1`. -/
@[simps -fullyApplied]
def stdSimplexEquivIcc : stdSimplex 𝕜 (Fin 2) ≃ Icc (0 : 𝕜) 1
where
toFun f := ⟨f.1 1, f.2.1 _, f.2.2 ▸ Finset.single_le_sum (fun i _ ↦ f.2.1 i) (Finset.mem_univ _)⟩
invFun x := ⟨![1 - x, x], Fin.forall_fin_two.2 ⟨sub_nonneg.2 x.2.2, x.2.1⟩, by simp⟩
left_inv
f := Subtype.eq <| funext <| Fin.forall_fin_two.2 <| by simp [← (show f.1 0 + f.1 1 = 1 by simpa using f.2.2)]
