exists_mem_basis — Mathlib

English

If μ.FiniteAtFilter f and f HasBasis p s, there exists i with p(i) and μ(s_i) < ∞.

Русский

Если μ.FiniteAtFilter f и f имеет базис p с s, найдётся i такое, что p(i) и μ(s_i) < ∞.

LaTeX

$$∃ i, p i ∧ μ(s i) < ∞$$

Lean4

theorem exists_mem_basis {f : Filter α} (hμ : FiniteAtFilter μ f) {p : ι → Prop} {s : ι → Set α} (hf : f.HasBasis p s) :
    ∃ i, p i ∧ μ (s i) < ∞ :=
  (hf.exists_iff fun {_s _t} hst ht => (measure_mono hst).trans_lt ht).1 hμ

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