eqOn

Mathlib.Topology.FiberBundle.Trivialization

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

English

x ∈ e.source if and only if proj x ∈ e.baseSet.

Русский

x ∈ e.source тогда и только тогда, когда proj(x) ∈ e.baseSet.

LaTeX

$$$x \in e.source \iff \mathrm{proj}(x) \in e.baseSet$$$

Lean4

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

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

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

Разделы

Аффилиация

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