mem_ofSimplex_obj_iff — Mathlib

English

For x ∈ X and m, membership in ofSimplex x at m is equivalent to the existence of a map f with X.map f.op x = y.

Русский

Для x ∈ X и для m, членство y в ofSimplex x.obj m эквивалentно существованию отображения f с X.map f.op x = y.

LaTeX

$$$$ y \in (\text{ofSimplex } x).obj m \iff \exists f : m.unop \rightarrow \langle n \rangle, \; X.map f.op x = y $$$$

Lean4

theorem mem_ofSimplex_obj_iff {n : ℕ} (x : X _⦋n⦌) {m : SimplexCategoryᵒᵖ} (y : X.obj m) :
    y ∈ (ofSimplex x).obj m ↔ ∃ (f : m.unop ⟶ ⦋n⦌), X.map f.op x = y :=
  by
  dsimp [ofSimplex, Subpresheaf.ofSection]
  aesop

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