inter_ae_eq_empty_of_ae_eq_empty_left

English

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

Русский

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

LaTeX

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

Lean4

theorem inter_ae_eq_empty_of_ae_eq_empty_left (h : s =ᵐ[μ] (∅ : Set α)) : (s ∩ t : Set α) =ᵐ[μ] (∅ : Set α) :=
  by
  convert ae_eq_set_inter h (ae_eq_refl t)
  rw [empty_inter]

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