apply_coe_mem_map

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.apply_coe_mem_map

English

For a lattice homomorphism f and an element a in L, the image f a belongs to L.map f.

Русский

Пусть f — гомоморфизм решёток, а a ∈ L. Тогда f(a) принадлежит L.map f.

LaTeX

$$$f(a) \\in L.map f$$$

Lean4

theorem apply_coe_mem_map (f : LatticeHom α β) (a : L) : f a ∈ L.map f :=
  mem_map_of_mem f a.prop

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

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

Разделы

Аффилиация

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