vPullbackConeIsLimit — Mathlib

English

There exists a representation of any glued point as the image of some ι_i from some component U_i.

Русский

Любая точка склейки может быть получена как образ некоторого ι_i из компонента U_i.

LaTeX

$$$\\exists i, \\exists y, (\\iota_i)_{base}(y) = x$$$

Lean4

/-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.
```
Vᵢⱼ ⟶ Uᵢ
 |      |
 ↓      ↓
 Uⱼ ⟶ X
```
-/
def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) :=
  𝖣.vPullbackConeIsLimitOfMap forgetToSheafedSpace i j (D.toSheafedSpaceGlueData.vPullbackConeIsLimit _ _)

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