mem_sieve₁'

Mathlib.CategoryTheory.Sites.Hypercover.One

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁'

← MathLib Explorer

English

Membership lemma for E.sieve₁' in J via pullback condition.

Русский

Лемма принадлежности для E.sieve₁' внутри J через условие вытяжки.

LaTeX

$$$ E.sieve_1' i_1 i_2 \\in J _ $$$

Lean4

theorem mem_sieve₁' {S : C} (E : J.OneHypercover S) (i₁ i₂ : E.I₀) [HasPullback (E.f i₁) (E.f i₂)] :
    E.sieve₁' i₁ i₂ ∈ J _ := by
  rw [E.sieve₁'_eq_sieve₁]
  exact mem₁ _ _ _ _ _ pullback.condition

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

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

Разделы

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

Аффилиация

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