English
clPrehaar(K0,U) is the closure of the set { prehaar(K0,U,K) } over K in Compacts.
Русский
clPrehaar(K0,U) равна замыканию множества prehaar(K0,U,K) по K в Compacts.
LaTeX
$$$\overline{\{\operatorname{prehaar}(K_0,U,K) : K \in \text{Compacts} \}}$$$
Lean4
/-- The closure of the collection of elements of the form `prehaar K₀ U`,
for `U` open neighbourhoods of `1`, contained in `V`. The closure is taken in the space
`compacts G → ℝ`, with the topology of pointwise convergence.
We show that the intersection of all these sets is nonempty, and the Haar measure
on compact sets is defined to be an element in the closure of this intersection. -/
@[to_additive /-- additive version of `MeasureTheory.Measure.haar.clPrehaar` -/
]
def clPrehaar (K₀ : Set G) (V : OpenNhdsOf (1 : G)) : Set (Compacts G → ℝ) :=
closure <| prehaar K₀ '' {U : Set G | U ⊆ V.1 ∧ IsOpen U ∧ (1 : G) ∈ U}
