toTopObj_one_coe_add_coe_eq_one — Mathlib

English

In Real numbers, the two coordinates of a 1-simplex sum to 1: (f(0)) + f(1) = 1.

Русский

В вещественных числах две координаты 1-мерного простейшего складываются в единицу: (f(0)) + f(1) = 1.

LaTeX

$$$\\forall f \\in (\\langle 1 \\rangle).toTopObj,\\; (f(0) : \\mathbb{R}) + f(1) = 1$$$

Lean4

theorem toTopObj_one_coe_add_coe_eq_one (f : ⦋1⦌.toTopObj) : (f 0 : ℝ) + f 1 = 1 :=
  by
  norm_cast
  rw [toTopObj_one_add_eq_one]

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