isCovering_of_bijective_costar

Mathlib.Combinatorics.Quiver.Covering

URI: https://scilib.ai/kg/mathlib#Prefunctor.isCovering_of_bijective_costar

← MathLib Explorer

English

If all φ.costar u are bijective, then φ is a covering.

Русский

Если для всех u отображение φ.costar u биективно, то φ является покрывающим.

LaTeX

$$isCovering_of_bijective_costar$$

Lean4

theorem isCovering_of_bijective_costar (h : ∀ u, Bijective (φ.costar u)) : φ.IsCovering :=
  ⟨fun u => (φ.bijective_costar_iff_bijective_star u).1 (h u), h⟩

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

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

Разделы

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

Аффилиация

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