mem_source

Mathlib.Topology.FiberBundle.Trivialization

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

English

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

Русский

x принадлежит области определения тогда и только тогда, когда proj(x) ∈ e.baseSet.

LaTeX

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

Lean4

theorem mem_source : x ∈ e.source ↔ proj x ∈ e.baseSet := by rw [e.source_eq, mem_preimage]

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

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

Разделы

Аффилиация

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