toGerm — Mathlib

English

An a.e.-equivalence class function f can be interpreted as a germ at the almost-everywhere filter.

Русский

Функцию в классе эквивалентности a.e. можно трактовать как га́рм на фильтре a.e.

LaTeX

$$$toGerm: (α →ₘ[μ] β) \to (ae μ)\text{ Germ } β$$$

Lean4

/-- Interpret `f : α →ₘ[μ] β` as a germ at `ae μ` forgetting that `f` is almost everywhere
strongly measurable. -/
def toGerm (f : α →ₘ[μ] β) : Germ (ae μ) β :=
  Quotient.liftOn' f (fun f => ((f : α → β) : Germ (ae μ) β)) fun _ _ H => Germ.coe_eq.2 H

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