map_eq_comap_of_inverse — Mathlib

English

If m and n are inverse to each other, then map m f equals comap n f.

Русский

Если m и n взаимно обратны, то образ m фильтра f равен обратному образу фильтра f по n.

LaTeX

$$map m f = comap n f$$

Lean4

theorem map_eq_comap_of_inverse {f : Filter α} {m : α → β} {n : β → α} (h₁ : m ∘ n = id) (h₂ : n ∘ m = id) :
    map m f = comap n f :=
  map_equiv_symm ⟨n, m, congr_fun h₁, congr_fun h₂⟩ f

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