isLittleOTVS_map — Mathlib

English

Post-composing both f and g with a fixed map k preserves the little-OTVS relation: f =o after map k is equivalent to f∘k =o relative to l when paired with g∘k.

Русский

Пост-композиция обеих функций f и g с фиксированным отображением k сохраняет отношение little-OTVS: f = o после map k эквивалентно f ∘ k = o по отношению к l совместно с g ∘ k.

LaTeX

$$$f =o[𝕜; map\\ k\\ l]\\ g \\iff (f \\circ k) =o[𝕜; l] (g \\circ k).$$$

Lean4

@[simp]
theorem isLittleOTVS_map {k : β → α} {l : Filter β} : f =o[𝕜; map k l] g ↔ (f ∘ k) =o[𝕜; l] (g ∘ k) := by
  simp [isLittleOTVS_iff, EventuallyLE]

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