inter_ae_eq_left_of_ae_eq_univ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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