image

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#IsSublattice.image

English

If s is a Sublattice and f is a lattice homomorphism, then the image f''s is a Sublattice.

Русский

Если s — субрешетка и f — гомоморфизм, то образ f''s является субрешеткой.

LaTeX

$$IsSublattice s → IsSublattice (Set.image (inst_2.coe f) s)$$

Lean4

theorem image [FunLike F α β] [LatticeHomClass F α β] (hs : IsSublattice s) (f : F) : IsSublattice (f '' s) :=
  ⟨hs.1.image _, hs.2.image _⟩

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

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

Разделы

Аффилиация

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