horn_eq_iSup — Mathlib

English

Λ[n,i] equals the supremum over j in ({i}^c) of stdSimplex.face(j)^c.

Русский

Λ[n,i] равняется супремуму по j в ({i}^c) из stdSimplex.face(j)^c.

LaTeX

$$\\mathrm{horn}(n,i) = \\bigvee_{j \\in ({i}^c)} \\mathrm{stdSimplex.face}(j)^c$$

Lean4

theorem horn_eq_iSup (n : ℕ) (i : Fin (n + 1)) :
    horn.{u} n i = ⨆ (j : ({ i }ᶜ : Set (Fin (n + 1)))), stdSimplex.face { j.1 }ᶜ :=
  by
  ext m j
  simp [stdSimplex.face_obj, horn, Set.eq_univ_iff_forall]
  rfl

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