ofSimplex_le_iff — Mathlib

English

For a simplex x and subcomplex A, the inclusion of the generated subcomplex is equivalent to x belonging to A.

Русский

Для simplex x и подкомплексa A равносильно утверждение: ofSimplex x ≤ A тогда и только тогда, когда x ∈ A.obj _.

LaTeX

$$$$ \text{ofSimplex } x \le A \;\iff\; x \in A.obj _ $$$$

Lean4

theorem ofSimplex_le_iff {n : ℕ} (x : X _⦋n⦌) (A : X.Subcomplex) : ofSimplex x ≤ A ↔ x ∈ A.obj _ :=
  Subpresheaf.ofSection_le_iff _ _

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