mk_mem_target

Mathlib.Topology.FiberBundle.Trivialization

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

English

Alternative expression for the source of the composite symmetry as the intersection of base sets.

Русский

Альтернативная форма источника композиции симметрии — пересечение базовых множеств.

LaTeX

$$$\text{source} (f^{-1}\circ e) = (e.baseSet\cap f.baseSet)\times\univ$$$

Lean4

theorem mk_mem_target {x : B} {y : F} : (x, y) ∈ e'.target ↔ x ∈ e'.baseSet :=
  e'.mem_target

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

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

Разделы

Аффилиация

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