coe_fst'

Mathlib.Topology.FiberBundle.Trivialization

URI: https://scilib.ai/kg/mathlib#Pretrivialization.coe_fst'

English

For every x in e.source, (fst ∘ e)(x) = proj(x).

Русский

Для каждого x из e.source выполняется (fst ∘ e)(x) = proj(x).

LaTeX

$$$\forall x \in e.(source),\ (\mathrm{fst}(e(x))) = \mathrm{proj}(x)$$$

Lean4

theorem coe_fst' (ex : proj x ∈ e.baseSet) : (e x).1 = proj x :=
  e.coe_fst (e.mem_source.2 ex)

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

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

Разделы

Аффилиация

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