English
Let α and β be lattices and L a Sublattice of α. For a lattice homomorphism f from α to β, the image L.map f consists of all elements b in β that are the image under f of some element a in L; equivalently, b ∈ L.map f if and only if there exists a ∈ L with f(a) = b.
Русский
Пусть α и β — решётки, L — подпорешётка α. Пусть f — гомоморфизм решёток α → β. Образ L под действием f состоит из всех элементов b ∈ β, которые являются изображением некоторого a ∈ L; эквивалентно: b ∈ L.map f тогда и только тогда, когда существует a ∈ L такое, что f(a) = b.
LaTeX
$$$b \\in L.map f \\;\\iff\\; \\exists a \\in L, \\; f\,a = b$$$
Lean4
@[simp]
theorem mem_map {b : β} : b ∈ L.map f ↔ ∃ a ∈ L, f a = b :=
Iff.rfl
