ae_eq_restrict_biUnion_finset_iff

English

Equivalent form of ae_restrict_biUnion_finset_iff using alternative indexing by Finset.

Русский

Эквивалентная форма ae_restrict_biUnion_finset_iff с другой индексацией Finset.

LaTeX

$$$f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g \\iff ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g$.$$

Lean4

theorem ae_eq_restrict_biUnion_finset_iff (s : ι → Set α) (t : Finset ι) (f g : α → δ) :
    f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g :=
  ae_eq_restrict_biUnion_iff s t.countable_toSet f g

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