chaar_nonneg — Mathlib

English

If K1 and K2 are disjoint in their carrier sets and K2 is closed, then chaar(K0, sup(K1, K2)) equals the sum chaar(K0, K1) + chaar(K0, K2).

Русский

Если носители K1 и K2 раздельны, и K2 замкнуто, то chaar(K0, sup(K1,K2)) = chaar(K0,K1) + chaar(K0,K2).

LaTeX

$$$\text{chaar}(K_0, \mathrm{max}(K_1, K_2)) = \text{chaar}(K_0, K_1) + \text{chaar}(K_0, K_2)$$$

Lean4

@[to_additive addCHaar_nonneg]
theorem chaar_nonneg (K₀ : PositiveCompacts G) (K : Compacts G) : 0 ≤ chaar K₀ K := by
  have := chaar_mem_haarProduct K₀ K (mem_univ _); rw [mem_Icc] at this; exact this.1

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