interior_eq_empty — Mathlib

English

For a 0-simplex, the interior is empty.

Русский

Для 0-симплекса interior пуст.

LaTeX

$$$ s. interior = \emptyset $ for a 0-simplex$$

Lean4

@[simp]
theorem interior_eq_empty (s : Simplex k P 0) : s.interior = ∅ :=
  by
  ext p
  simp only [Simplex.interior, Simplex.setInterior, Nat.reduceAdd, univ_unique, Fin.default_eq_zero, Fin.isValue,
    sum_singleton, Set.mem_Ioo, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_exists, not_and]
  intro w h hi
  simpa [h] using hi 0

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