English
Under a lattice-homomorphism f preserving joins and meets, the image of latticeClosure s equals latticeClosure of the image of s.
Русский
При отображении, сохраняющем объединения и пересечения, образ latticeClosure(s) равен latticeClosure образа s.
LaTeX
$$$f'' \mathrm{latticeClosure}(s) = \mathrm{latticeClosure}(f'' s)$ при соответствующих предпосылках$$
Lean4
theorem image_latticeClosure (s : Set α) (f : α → β) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
(map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) : f '' latticeClosure s = latticeClosure (f '' s) :=
by
simp only [subset_antisymm_iff, Set.image_subset_iff]
constructor <;> apply latticeClosure_sup_inf_induction
· exact fun a ha ↦ subset_latticeClosure <| Set.mem_image_of_mem _ ha
· rintro a - b - ha hb
simpa [map_sup] using isSublattice_latticeClosure.supClosed ha hb
· rintro a - b - ha hb
simpa [map_inf] using isSublattice_latticeClosure.infClosed ha hb
· exact Set.image_mono subset_latticeClosure
· rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
exact ⟨a ⊔ b, isSublattice_latticeClosure.supClosed ha hb, map_sup ..⟩
· rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
exact ⟨a ⊓ b, isSublattice_latticeClosure.infClosed ha hb, map_inf ..⟩
