inf_ae_iff — Mathlib

English

If μ is finite at filter f, then it is finite at the infimum with any g: μ.FiniteAtFilter f → μ.FiniteAtFilter (f ⊓ g).

Русский

Если μ конечна на фильтре f, то она конечна и на их наименьшем (f ⊓ g).

LaTeX

$$$μ.FiniteAtFilter f → μ.FiniteAtFilter (f \inf g)$$$

Lean4

@[simp]
theorem inf_ae_iff : μ.FiniteAtFilter (f ⊓ ae μ) ↔ μ.FiniteAtFilter f :=
  by
  refine ⟨?_, fun h => h.filter_mono inf_le_left⟩
  rintro ⟨s, ⟨t, ht, u, hu, rfl⟩, hμ⟩
  suffices μ t ≤ μ (t ∩ u) from ⟨t, ht, this.trans_lt hμ⟩
  exact measure_mono_ae (mem_of_superset hu fun x hu ht => ⟨ht, hu⟩)

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