English
Let L and M be Boolean subalgebras of α and f a bounded lattice homomorphism with f injective. Then the image of the meet L ⊓ M under f equals the meet of the images: map f (L ⊓ M) = map f L ⊓ map f M.
Русский
Пусть L и M — булевы подполья α и f — ограниченный гомоморфизм решёток с инъективностью. Тогда образ соприкасания L и M под действием f равен соприкосновению образов: map f (L ⊓ M) = map f L ⊓ map f M.
LaTeX
$$$\\operatorname{map} f (L \\cap M) = \\operatorname{map} f L \\cap \\operatorname{map} f M$$$
Lean4
theorem map_inf (L M : BooleanSubalgebra α) (f : BoundedLatticeHom α β) (hf : Injective f) :
map f (L ⊓ M) = map f L ⊓ map f M := by
rw [← SetLike.coe_set_eq]
simp [Set.image_inter hf]
