mem_target

Mathlib.Topology.FiberBundle.Trivialization

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

English

x ∈ e.target iff its first coordinate lies in e.baseSet.

Русский

x ∈ e.target тогда и только тогда, когда первая компонента x ∈ e.baseSet.

LaTeX

$$$x \in e.target \iff x.1 \in e.baseSet$$$

Lean4

theorem mem_target {x : B × F} : x ∈ e.target ↔ x.1 ∈ e.baseSet :=
  e.toPretrivialization.mem_target

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

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

Разделы

Аффилиация

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