map_equiv_eq_comap_symm — Mathlib

English

For an isomorphism e, mapping by e.symm is the comap along e.

Русский

Для изоморфизма e отображение по e.symm эквивалентно взятию обратного образа вдоль e.

LaTeX

$$$L.map\, e^{-1} = L\;\text{comap}\, e$$$

Lean4

theorem map_equiv_eq_comap_symm (f : α ≃o β) (L : BooleanSubalgebra α) :
    L.map f = L.comap (f.symm : BoundedLatticeHom β α) :=
  SetLike.coe_injective <| f.toEquiv.image_eq_preimage L

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