inter_ae_eq_empty_of_ae_eq_empty_right

English

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

Русский

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

LaTeX

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

Lean4

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

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