eqOn

Mathlib.Topology.FiberBundle.Trivialization

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

English

If proj(x) ∈ e.baseSet, then the first component of e(x) equals proj(x).

Русский

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

LaTeX

$$$(e\,x)_{1} = \mathrm{proj}(x) \quad \text{если } \mathrm{proj}(x) \in e.baseSet$$$

Lean4

protected theorem eqOn : EqOn (Prod.fst ∘ e) proj e.source := fun _ hx => e.coe_fst hx

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

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

Разделы

Аффилиация

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