coe_mem_source

Mathlib.Topology.FiberBundle.Trivialization

URI: https://scilib.ai/kg/mathlib#Pretrivialization.coe_mem_source

English

For a fiber element y in E b, y considered as a point in e'.source is equivalent to b belonging to e'.baseSet.

Русский

Для элемента волокна y в E b, его членство в source эквивалентно принадлежности b базовому множеству e'.

LaTeX

$$$↑y\in e'.source\leftrightarrow b\in e'.baseSet$$$

Lean4

@[simp]
theorem coe_mem_source : ↑y ∈ e'.source ↔ b ∈ e'.baseSet :=
  e'.mem_source

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

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

Разделы

Аффилиация

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