boundary_eq_iSup — Mathlib

English

The boundary of the nth standard simplex can be expressed as the supremum of the complements of the single-vertex face inclusions, i.e., boundary(n) = ⨆_{i ∈ Fin(n+1)} stdSimplex.face{ i }^c.

Русский

Граница ∂Δ[n] выражается как верхняя грань над дополнениями грани по каждому i: boundary(n) = ⨆_{i ∈ Fin(n+1)} stdSimplex.face{ i }^c.

LaTeX

$$$ \\partial \\Delta[n] = \\bigcup_{i \\in \\mathrm{Fin}(n+1)} (\\mathrm{stdSimplex}.face\\{i\\}^{c})$$$

Lean4

theorem boundary_eq_iSup (n : ℕ) : boundary.{u} n = ⨆ (i : Fin (n + 1)), stdSimplex.face { i }ᶜ :=
  by
  ext
  simp [stdSimplex.face_obj, boundary, Function.Surjective]
  tauto

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