liftCover_restrict'

Mathlib.Topology.ContinuousMap.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.liftCover_restrict'

← MathLib Explorer

English

The glued map restricted to S_i equals φ_i: (liftCover S φ hφ hS).restrict(S_i) = φ_i.

Русский

Склеенное отображение, ограниченное до S_i, равно φ_i.

LaTeX

$$$\\mathrm{restrict}\\ (S_i)\\ (\\mathrm{liftCover}\\ S\\ φ\\ hφ\\ hS) = φ_i$$$

Lean4

@[simp]
theorem liftCover_restrict' {s : Set α} {hs : s ∈ A} : (liftCover' A F hF hA).restrict s = F s hs :=
  ext <| liftCover_coe' (hF := hF) (hA := hA)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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