English
If f reverses join/meet in a suitable way, then f'' latticeClosure s = latticeClosure(f'' s).
Русский
Если f корректно обращает операции объединения и пересечения, то образ latticeClosure сохраняется через f.
LaTeX
$$$f'' \mathrm{latticeClosure}(s) = \mathrm{latticeClosure}(f'' s)$ при допущениях map_sup, map_inf$$
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
simpa only [Set.image_comp, ← Set.preimage_equiv_eq_image_symm, ← ofDual_preimage_latticeClosure] using
image_latticeClosure s (ofDual.symm ∘ f) map_sup map_inf
