image — Mathlib

English

Let s be sup-closed in α and f: α → β a sup-homomorphism. Then the image f[s] is sup-closed in β.

Русский

Пусть s замкнуто по ⊔ в α и f: α → β — гомоморфизм по ⊔. Тогда изображение f[s] замкнуто по ⊔ в β.

LaTeX

$$$ (\\forall x \\in s)(\\forall y \\in s)\\, f(x) \\sqcup f(y) \\in f[s] \\quad \\text{(i.e. } f[x \\sqcup y] \\in f[s] \\text{)} $$$

Lean4

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

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