English
For compact K1,K2 and K0, the prehaar for their supremum does not exceed the sum of prehaars for each: prehaar ≤ prehaar1 + prehaar2.
Русский
Для K1,K2 и K0: prehaar(K0, U, K1 ⊔ K2) ≤ prehaar(K0, U, K1) + prehaar(K0, U, K2).
LaTeX
$$$\text{prehaar}_{K_0}(U, \mathsf{max}(K_1,K_2)) \le \text{prehaar}_{K_0}(U, K_1) + \text{prehaar}_{K_0}(U, K_2)$$$
Lean4
@[to_additive]
theorem prehaar_sup_eq {K₀ : PositiveCompacts G} {U : Set G} {K₁ K₂ : Compacts G} (hU : (interior U).Nonempty)
(h : Disjoint (K₁.1 * U⁻¹) (K₂.1 * U⁻¹)) :
prehaar (K₀ : Set G) U (K₁ ⊔ K₂) = prehaar (K₀ : Set G) U K₁ + prehaar (K₀ : Set G) U K₂ :=
by
simp only [prehaar];
rw [← add_div]
-- Porting note: Here was `congr`, but `to_additive` failed to generate a theorem.
refine congr_arg (fun x : ℝ => x / index K₀ U) ?_
exact mod_cast index_union_eq K₁ K₂ hU h
