English
For K1 and K2 compact subsets of G, and V with nonempty interior, the index of their union is at most the sum of the individual indices: index(K1 ∪ K2, V) ≤ index(K1, V) + index(K2, V).
Русский
Для K1 и K2 — компактных подмножеств G и V с непустымInterior выполняется: index(K1 ∪ K2, V) ≤ index(K1, V) + index(K2, V).
LaTeX
$$$\text{index}(K_1 \cup K_2, V) \le \text{index}(K_1, V) + \text{index}(K_2, V)$$$
Lean4
@[to_additive addIndex_union_le]
theorem index_union_le (K₁ K₂ : Compacts G) {V : Set G} (hV : (interior V).Nonempty) :
index (K₁.1 ∪ K₂.1) V ≤ index K₁.1 V + index K₂.1 V := by
classical
rcases index_elim K₁.2 hV with ⟨s, h1s, h2s⟩
rcases index_elim K₂.2 hV with ⟨t, h1t, h2t⟩
rw [← h2s, ← h2t]
refine le_trans (Nat.sInf_le ⟨_, ?_, rfl⟩) (Finset.card_union_le _ _)
rw [mem_setOf_eq, Finset.set_biUnion_union]
gcongr
