Commit 2025-08-21 17:58 35e8f57b
View on Github →refactor(MeasureTheory/RieszMarkovKakutani): Use PositiveLinearMap (#28059)
This PR refactors the unbundled {Λ : C_c(X, ℝ) →ₗ[ℝ] ℝ} (hΛ : ∀ f, 0 ≤ f → 0 ≤ Λ f) in the statement of RMK to the bundled (Λ : C_c(X, ℝ) →ₚ[ℝ] ℝ).
Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Uniqueness.20in.20Riesz.E2.80.93Markov.E2.80.93Kakutani.20representation.20theorem