W_of_isLocallyBijective

Mathlib.CategoryTheory.Sites.LocallyBijective

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.W_of_isLocallyBijective

← MathLib Explorer

English

If f is locally bijective, then W f holds.

Русский

Если f локально биективен, то выполняется W f.

LaTeX

$$[Presheaf.IsLocallyInjective J f] [Presheaf.IsLocallySurjective J f] : J.W f$$

Lean4

theorem W_of_isLocallyBijective [Presheaf.IsLocallyInjective J f] [Presheaf.IsLocallySurjective J f] : J.W f :=
  by
  rw [W_iff_isLocallyBijective]
  constructor <;> infer_instance

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

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

Разделы

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

Аффилиация

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