aeEqSetoid — Mathlib

English

Define the almost-everywhere equality setoid on AEStronglyMeasurable functions: f ≈ g iff f =ᵐ[μ] g.

Русский

Определяем множитель-отношение почти везде равно между AEStronglyMeasurable функциями: f ≈ g тогда и только тогда, когда f =ᵐ[μ] g.

LaTeX

$$aeEqSetoid μ := ⟨(f,g) ↔ (f =ᵐ[μ] g), ...⟩$$

Lean4

/-- The equivalence relation of being almost everywhere equal for almost everywhere strongly
measurable functions. -/
def aeEqSetoid (μ : Measure α) : Setoid { f : α → β // AEStronglyMeasurable f μ } :=
  ⟨fun f g => (f : α → β) =ᵐ[μ] g, fun {f} => ae_eq_refl f.val, fun {_ _} => ae_eq_symm, fun {_ _ _} => ae_eq_trans⟩

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