map — Mathlib

English

For any φ in a fibre, the mapping under p.map φ yields a HomLift instance for the base projection.

Русский

Для любого φ в волокне отображение p.map φ порождает зависимое поднятие над базовым отображением.

LaTeX

$$$p.IsHomLift (p.map φ) φ$$$

Lean4

/-- For any arrow `φ : a ⟶ b` in `𝒳`, `φ` lifts the arrow `p.map φ` in the base `𝒮`. -/
@[simp]
instance map {a b : 𝒳} (φ : a ⟶ b) : p.IsHomLift (p.map φ) φ where cond := by constructor

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