FiniteAtFilter — Mathlib

English

If μ.FiniteAtFilter f and f has a basis {s_i}, there exists i with μ(s_i) < ∞.

Русский

Если μ имеет конечную меру на фильтре f и f имеет базис {s_i}, существует i такой что μ(s_i) < ∞.

LaTeX

$$$\exists i, p(i) \land μ(s_i) < ∞$$$

Lean4

/-- A measure is called finite at filter `f` if it is finite at some set `s ∈ f`.
Equivalently, it is eventually finite at `s` in `f.small_sets`. -/
def FiniteAtFilter {_m0 : MeasurableSpace α} (μ : Measure α) (f : Filter α) : Prop :=
  ∃ s ∈ f, μ s < ∞

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