prehaar_sup_le — Mathlib

English

For K1, K2 compact, and U with nonempty interior, prehaar(K0, U, K1 ⊔ K2) ≤ prehaar(K0, U, K1) + prehaar(K0, U, K2).

Русский

Для K1,K2 компактных: prehaar(K0,U,K1 ⊔ K2) ≤ prehaar(K0,U,K1) + prehaar(K0,U,K2).

LaTeX

$$$\text{prehaar}_{K_0}(U, K_1 \sqcup K_2) \le \text{prehaar}_{K_0}(U, K_1) + \text{prehaar}_{K_0}(U, K_2)$$$

Lean4

@[to_additive]
theorem prehaar_sup_le {K₀ : PositiveCompacts G} {U : Set G} (K₁ K₂ : Compacts G) (hU : (interior U).Nonempty) :
    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, div_le_div_iff_of_pos_right]
  · exact mod_cast index_union_le K₁ K₂ hU
  · exact mod_cast index_pos K₀ hU

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