inter_ae_eq_right_of_ae_eq_univ — Mathlib

English

If s is almost everywhere equal to the universal set, then s ∩ t is almost everywhere equal to t.

Русский

Если s равно вселенной почти по μ, то s ∩ t равно t почти повсеместно.

LaTeX

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

Lean4

theorem inter_ae_eq_right_of_ae_eq_univ (h : s =ᵐ[μ] univ) : (s ∩ t : Set α) =ᵐ[μ] t :=
  by
  convert ae_eq_set_inter h (ae_eq_refl t)
  rw [univ_inter]

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