mono — Mathlib

English

If f ≤ g, then μ.FiniteAtFilter g → μ.FiniteAtFilter f; similarly for measure relations.

Русский

Если f ≤ g, то конечность μ на g переносится на f; аналогично для отношений меры.

LaTeX

$$$f \le g \to μ.FiniteAtFilter g \to μ.FiniteAtFilter f$$$

Lean4

@[mono]
protected theorem mono (hf : f ≤ g) (hμ : μ ≤ ν) : ν.FiniteAtFilter g → μ.FiniteAtFilter f := fun h =>
  (h.filter_mono hf).measure_mono hμ

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