index_mono — Mathlib

English

If K is contained in K' and the interior of V is nonempty, then the index does not increase: index(K, V) ≤ index(K', V).

Русский

Если K ⊆ K' и interior(V) не пусто, то индекс не возрастает: index(K, V) ≤ index(K', V).

LaTeX

$$$\text{index}(K, V) \leq \text{index}(K', V)\quad (K \subseteq K',\, (\operatorname{int}V).\mathord{\text{Nonempty}})$$$$

Lean4

@[to_additive addIndex_mono]
theorem index_mono {K K' V : Set G} (hK' : IsCompact K') (h : K ⊆ K') (hV : (interior V).Nonempty) :
    index K V ≤ index K' V := by
  rcases index_elim hK' hV with ⟨s, h1s, h2s⟩
  apply Nat.sInf_le; rw [mem_image]; exact ⟨s, Subset.trans h h1s, h2s⟩

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