congr — Mathlib

English

If two sets are almost everywhere equal to s and t respectively, then their AEDisjoint relation is preserved.

Русский

Если две пары множеств совпадают почти повсеместно с s и t соответствующим образом, то их отношение AEDisjoint сохраняется.

LaTeX

$$AEDisjoint μ s t → s =ᵐ[μ] u → t =ᵐ[μ] v → AEDisjoint μ u v$$

Lean4

protected theorem congr (h : AEDisjoint μ s t) (hu : u =ᵐ[μ] s) (hv : v =ᵐ[μ] t) : AEDisjoint μ u v :=
  mono_ae h (Filter.EventuallyEq.le hu) (Filter.EventuallyEq.le hv)

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