sup_iff — Mathlib

English

IntegrableAtFilter f (l ⊔ l') μ ↔ (IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ).

Русский

IntegrableAtFilter f (l ⊔ l') μ эквивалентно IntegrableAtFilter f l μ и IntegrableAtFilter f l' μ.

LaTeX

$$$\\operatorname{IntegrableAtFilter}(f, l\\sqcup l', \\mu) \\iff (\\operatorname{IntegrableAtFilter}(f, l, \\mu) \\land \\operatorname{IntegrableAtFilter}(f, l', \\mu)).$$$

Lean4

theorem sup_iff [PseudoMetrizableSpace ε'] {f : α → ε'} {l l' : Filter α} :
    IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ :=
  by
  constructor
  · exact fun h => ⟨h.filter_mono le_sup_left, h.filter_mono le_sup_right⟩
  · exact fun ⟨⟨s, hsl, hs⟩, ⟨t, htl, ht⟩⟩ ↦ ⟨s ∪ t, union_mem_sup hsl htl, hs.union ht⟩

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