restrict_biUnion_finset_congr — Mathlib

English

If μ|_{⋃ i∈s} t_i = ν|_{⋃ i∈s} t_i for a countable s, then μ|_{t_i} = ν|_{t_i} for all i ∈ s.

Русский

Если μ ограничено на объединение по i в s равно ν ограничено на то же объединение, то для каждого i ∈ s следует μ|_{t_i} = ν|_{t_i}.

LaTeX

$$$s.Countable \implies (μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) \iff ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i))$$$

Lean4

theorem restrict_biUnion_finset_congr {s : Finset ι} {t : ι → Set α} :
    μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i) := by
  classical
    induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs =>
    simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
    rw [restrict_union_congr, ← hs]

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