measure_union_congr_of_subset — Mathlib

English

If two families s_i, t_i satisfy s_i ⊆ t_i for all i and μ(t_i) ≤ μ(s_i) for all i, then the measure of the union of s_i equals the measure of the union of t_i.

Русский

Если для всех i выполняется s_i ⊆ t_i и μ(t_i) ≤ μ(s_i), тогда мерa объединения s_i равна мере объединения t_i.

LaTeX

$$$ \forall i, s_i \subseteq t_i \rightarrow \forall i, μ(t_i) ≤ μ(s_i) \rightarrow μ(⋃ i, s_i) = μ(⋃ i, t_i) $$$

Lean4

theorem measure_union_congr_of_subset {t₁ t₂ : Set α} (hs : s₁ ⊆ s₂) (hsμ : μ s₂ ≤ μ s₁) (ht : t₁ ⊆ t₂)
    (htμ : μ t₂ ≤ μ t₁) : μ (s₁ ∪ t₁) = μ (s₂ ∪ t₂) :=
  by
  rw [union_eq_iUnion, union_eq_iUnion]
  exact measure_iUnion_congr_of_subset (Bool.forall_bool.2 ⟨ht, hs⟩) (Bool.forall_bool.2 ⟨htμ, hsμ⟩)

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