coe_coe_fst

Mathlib.Topology.FiberBundle.Trivialization

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

English

An element (x,y) lies in the target of e' exactly when x lies in e'.baseSet.

Русский

Элемент $(x,y)$ принадлежит целевой области e' тогда и только тогда, когда x ∈ e'.baseSet.

LaTeX

$$$(x,y)\in e'.target\iff x\in e'.baseSet$$$

Lean4

@[mfld_simps]
theorem coe_coe_fst (hb : b ∈ e'.baseSet) : (e' y).1 = b := by simp [hb]

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

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

Разделы

Аффилиация

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