face_le_horn — Mathlib

English

If i ≠ j, then the i-th face (complement of {i}) is contained in the j-th horn: stdSimplex.face{ i }^c ≤ horn n j.

Русский

Если i ≠ j, то i-я грань (комплемент {i}) содержится в j-ом рожке: stdSimplex.face{ i }^c ≤ horn n j.

LaTeX

$$$\\text{stdSimplex.face}_{\\{i\\}}^{c} \\le \\mathrm{horn}(n,j) \\quad\\text{при } i \\neq j$$$

Lean4

theorem face_le_horn {n : ℕ} (i j : Fin (n + 1)) (h : i ≠ j) : stdSimplex.face.{u} { i }ᶜ ≤ horn n j :=
  by
  rw [horn_eq_iSup]
  exact le_iSup (fun (k : ({ j }ᶜ : Set (Fin (n + 1)))) ↦ stdSimplex.face.{u} { k.1 }ᶜ) ⟨i, h⟩

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