mem_prehaar_empty — Mathlib

English

The membership condition for haarProduct when K0 is empty collection is equivalent to 0.

Русский

Условие принадлежности для haarProduct при пустом K0 эквивалентно нулю.

LaTeX

$$$f \in \haarProduct(K_0) \iff f(K) \in Icc(0, index(K,K_0))$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_prehaar_empty {K₀ : Set G} {f : Compacts G → ℝ} :
    f ∈ haarProduct K₀ ↔ ∀ K : Compacts G, f K ∈ Icc (0 : ℝ) (index (K : Set G) K₀) := by
  simp only [haarProduct, Set.pi, forall_prop_of_true, mem_univ, mem_setOf_eq]

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