coe_fst

Mathlib.Topology.FiberBundle.Trivialization

URI: https://scilib.ai/kg/mathlib#Trivialization.coe_fst

English

If x lies in the domain e.source, then the first coordinate of e(x) equals proj(x).

Русский

Если x ∈ e.source, то первый компонент e(x) равен proj(x).

LaTeX

$$$\text{If } x \in e.source, \ (e(x)).1 = \mathrm{proj}(x)$$$

Lean4

@[simp, mfld_simps]
theorem coe_fst (ex : x ∈ e.source) : (e x).1 = proj x :=
  e.proj_toFun x ex

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru