cofinite — Mathlib

English

The cofinites filter membership corresponds to finiteness of the complement: s ∈ μ.cofinite iff μ(s^c) < ∞.

Русский

Членство в фильтре cofinites эквивалентно тому, что комплемент имеет конечную меру: s ∈ μ.cofinite ⇔ μ(s^c) < ∞.

LaTeX

$$$ s \in \mu.cofinite \iff \mu(s^c) < \infty $$$

Lean4

/-- The filter of sets `s` such that `sᶜ` has finite measure. -/
def cofinite {m0 : MeasurableSpace α} (μ : Measure α) : Filter α :=
  comk (μ · < ∞) (by simp) (fun _ ht _ hs ↦ (measure_mono hs).trans_lt ht) fun s hs t ht ↦
    (measure_union_le s t).trans_lt <| ENNReal.add_lt_top.2 ⟨hs, ht⟩

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