union_ae_eq_left_of_ae_eq_empty — Mathlib

English

Let s,t ⊆ α. If t is equal to the empty set almost everywhere with respect to μ, then s ∪ t is equal to s almost everywhere with respect to μ.

Русский

Пусть s,t ⊆ α. Если t равно пустому по μ почти повсеместно, то s ∪ t равно s почти повсеместно.

LaTeX

$$$\forall s,t\subseteq\alpha,\; t =_{\mathrm{ae}}^{\mu} \emptyset \Rightarrow (s \cup t) =_{\mathrm{ae}}^{\mu} s$$$

Lean4

theorem union_ae_eq_left_of_ae_eq_empty (h : t =ᵐ[μ] (∅ : Set α)) : (s ∪ t : Set α) =ᵐ[μ] s :=
  by
  convert ae_eq_set_union (ae_eq_refl s) h
  rw [union_empty]

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