comap

Mathlib.Order.CompleteSublattice

URI: https://scilib.ai/kg/mathlib#CompleteSublattice.comap

Lean4

/-- The pull back of a complete sublattice under a complete lattice hom is a complete sublattice. -/
@[simps]
def comap (L : CompleteSublattice β) : CompleteSublattice α
    where
  carrier := f ⁻¹' L
  supClosed' := L.supClosed.preimage f
  infClosed' := L.infClosed.preimage f
  sSupClosed' s
    hs := by simpa only [mem_preimage, map_sSup, SetLike.mem_coe] using sSupClosed <| mapsTo_iff_image_subset.mp hs
  sInfClosed' s
    hs := by simpa only [mem_preimage, map_sInf, SetLike.mem_coe] using sInfClosed <| mapsTo_iff_image_subset.mp hs

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru