inf_ae_iff — Mathlib

English

IntegrableAtFilter f (l ⊓ ae μ) μ ↔ IntegrableAtFilter f l μ.

Русский

IntegrableAtFilter f (l ⊓ ae μ) μ ⇔ IntegrableAtFilter f l μ.

LaTeX

$$$\\operatorname{IntegrableAtFilter}(f, l \\cap ae(\\mu), \\mu) \\;\\Leftrightarrow\\; \\operatorname{IntegrableAtFilter}(f, l, \\mu).$$$

Lean4

@[simp]
theorem inf_ae_iff {l : Filter α} : IntegrableAtFilter f (l ⊓ ae μ) μ ↔ IntegrableAtFilter f l μ :=
  by
  refine ⟨?_, fun h ↦ h.filter_mono inf_le_left⟩
  rintro ⟨s, ⟨t, ht, u, hu, rfl⟩, hf⟩
  refine ⟨t, ht, hf.congr_set_ae <| eventuallyEq_set.2 ?_⟩
  filter_upwards [hu] with x hx using (and_iff_left hx).symm

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