prehaar_nonneg

Mathlib.MeasureTheory.Measure.Haar.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.haar.prehaar_nonneg

← MathLib Explorer

English

For any K0, U and K, prehaar(K0,U,K) is nonnegative.

Русский

Для любых K0,U,K выражение prehaar неотрицательно.

LaTeX

$$$0 \le \operatorname{prehaar}(K_0,U,K)$$$

Lean4

@[to_additive]
theorem prehaar_nonneg (K₀ : PositiveCompacts G) {U : Set G} (K : Compacts G) : 0 ≤ prehaar (K₀ : Set G) U K := by
  apply div_nonneg <;> norm_cast <;> apply zero_le

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru