eq_stalkwise — Mathlib

English

The property SurjectiveOnStalks is equivalent to its stalk-wise formulation, i.e., surjectivity on stalk maps at every point.

Русский

Свойство SurjectiveOnStalks эквивалентно его локальному формулированию по стелам: сюръективность отображения стел на каждой точке.

LaTeX

$$SurjectiveOnStalks f ≡ stalkwise (Function.Surjective f.stalkMap)$$

Lean4

theorem eq_stalkwise : @SurjectiveOnStalks = stalkwise (Function.Surjective ·) := by ext; exact surjectiveOnStalks_iff _

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