image — Mathlib

English

If s is inf-closed and f is an inf-homomorphism, then the image f''s is inf-closed.

Русский

Если s инф-замкнуто и f инф-гомоморфизм, то образ f''s инф-замкнут.

LaTeX

$$$ \\text{InfClosed } s \\rightarrow \\text{InfClosed}(f''s) $$$

Lean4

theorem image [FunLike F α β] [InfHomClass F α β] (hs : InfClosed s) (f : F) : InfClosed (f '' s) :=
  by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
  rw [← map_inf]
  exact Set.mem_image_of_mem _ <| hs ha hb

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