English
Let G be a topological group and K a positive compact subset. If V is any subset whose interior is nonempty, then the index of V with respect to K is strictly positive: index(K, V) > 0.
Русский
Пусть G — топологическая группа, K — положимый компакт, и V — множество таковое, что interior(V) не пусто. Тогда индекс (K, V) строго положителен: index(K, V) > 0.
LaTeX
$$$0 < \text{index}(K, V)$$$
Lean4
@[to_additive addIndex_pos]
theorem index_pos (K : PositiveCompacts G) {V : Set G} (hV : (interior V).Nonempty) : 0 < index (K : Set G) V := by
classical
rw [index, Nat.sInf_def, Nat.find_pos, mem_image]
· rintro ⟨t, h1t, h2t⟩; rw [Finset.card_eq_zero] at h2t; subst h2t
obtain ⟨g, hg⟩ := K.interior_nonempty
change g ∈ (∅ : Set G)
convert h1t (interior_subset hg); symm
simp only [Finset.notMem_empty, iUnion_of_empty, iUnion_empty]
· exact index_defined K.isCompact hV
