setInterior_mono — Mathlib

English

If I ⊆ J, then the interior with weights in I is contained in the interior with weights in J for any simplex.

Русский

Если I ⊆ J, то множество interiors с весами из I содержится во внутреннем составе с весами из J.

LaTeX

$$$ s.\mathrm{setInterior} I\; s \subseteq s.\mathrm{setInterior} J $ when I ⊆ J$$

Lean4

theorem setInterior_mono {I J : Set k} (hij : I ⊆ J) {n : ℕ} (s : Simplex k P n) : s.setInterior I ⊆ s.setInterior J :=
  fun _ ⟨w, hw, hw01, hww⟩ ↦ ⟨w, hw, fun i ↦ hij (hw01 i), hww⟩

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