map_equiv_eq_comap_symm — Mathlib

English

For an order isomorphism f: β ≃o α, the map of L under f.symm equals the comap of L under f, establishing a duality between map and comap.

Русский

Для порядка изоморфизма f: β ≃o α отображение L через f.symm эквивалентно обратному образу L под f, демонстрируя двойственность между map и comap.

LaTeX

$$L.map f = L.comap (f.symm : LatticeHom β α)$$

Lean4

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

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