isCovering_of_bijective_star

Mathlib.Combinatorics.Quiver.Covering

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$isCovering_of_bijective_star$$

Lean4

theorem isCovering_of_bijective_star (h : ∀ u, Bijective (φ.star u)) : φ.IsCovering :=
  ⟨h, fun u => (φ.bijective_costar_iff_bijective_star u).2 (h u)⟩

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

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

Разделы

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

Аффилиация

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