bijective_costar_iff_bijective_star

Mathlib.Combinatorics.Quiver.Covering

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

← MathLib Explorer

English

Bijectivity of φ.costar u is equivalent to bijectivity of φ.star u for each u.

Русский

Биективность φ.costar u эквивалентна биективности φ.star u для каждого u.

LaTeX

$$bijective_costar_iff_bijective_star$$

Lean4

theorem bijective_costar_iff_bijective_star (u : U) : Bijective (φ.costar u) ↔ Bijective (φ.star u) := by
  rw [Prefunctor.costar_conj_star φ, EquivLike.comp_bijective, EquivLike.bijective_comp]

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

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

Разделы

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

Аффилиация

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