exists

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sieve.ofArrows.exists

Lean4

theorem «exists» : ∃ (i : I) (h : W ⟶ Y i), g = h ≫ f i :=
  by
  obtain ⟨_, h, _, ⟨i⟩, rfl⟩ := hg
  exact ⟨i, h, rfl⟩

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

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

Разделы

Аффилиация

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