prehaar_le_index — Mathlib

English

For a positive compact K0 and any open U with nonempty interior, the prehaar of U with K relative to K0 is bounded above by the index: prehaar(K0, U, K) ≤ index(K, K0).

Русский

Для K0 и любого открытого U с непустым interior: prehaar(K0, U, K) ≤ index(K, K0).

LaTeX

$$$\text{prehaar}_{K_0}(U,K) \le \text{index}(K,K_0)$$$

Lean4

@[to_additive add_prehaar_le_addIndex]
theorem prehaar_le_index (K₀ : PositiveCompacts G) {U : Set G} (K : Compacts G) (hU : (interior U).Nonempty) :
    prehaar (K₀ : Set G) U K ≤ index (K : Set G) K₀ :=
  by
  unfold prehaar; rw [div_le_iff₀] <;> norm_cast
  · apply le_index_mul K₀ K hU
  · exact index_pos K₀ hU

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