isEquivalent_map — Mathlib

English

The equivalence of two functions is preserved under reparameterization by a map k: α → α₂; specifically, f ~[Filter.map k l] g iff f∘k ~[l] g∘k.

Русский

Эквивалентность двух функций сохраняется при замене параметра с помощью отображения k: α → α₂; то есть f ~[Filter.map k l] g эквивалентно f∘k ~[l] g∘k.

LaTeX

$$$f ~[Filter.map k l] g \;\Leftrightarrow\; (f \circ k) ~[l] (g \circ k)$$$

Lean4

@[simp]
theorem isEquivalent_map {α₂ : Type*} {f g : α₂ → β} {k : α → α₂} : f ~[Filter.map k l] g ↔ (f ∘ k) ~[l] (g ∘ k) :=
  isLittleO_map

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