notConvergentSeq — Mathlib

English

Applying an order isomorphism to essInf preserves essInf under μ.

Русский

Преобразование по линейному порядку сохраняет essInf относительно меры μ.

LaTeX

$$$g (essInf f μ) = essInf (fun x => g (f x)) μ$$$

Lean4

/-- Given a sequence of functions `f` and a function `g`, `notConvergentSeq f g n j` is the
set of elements such that `f k x` and `g x` are separated by at least `1 / (n + 1)` for some
`k ≥ j`.

This definition is useful for Egorov's theorem. -/
def notConvergentSeq [Preorder ι] (f : ι → α → β) (g : α → β) (n : ℕ) (j : ι) : Set α :=
  ⋃ (k) (_ : j ≤ k), {x | (n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)}

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